Prove2Me

Existence Of A Suitable Number Of Copies

Proved
FunctionalInequalities.KLS.LogConcave.Suspension.exists_copies_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement formalizes the numerical choice of the number of copies in the suspension construction.

Let a,β,M∈Ra,\beta,M\in\mathbb R satisfy

a>0,β≥0,M≥0.a>0,\qquad \beta\ge0,\qquad M\ge0.

Then there exists an integer N>0N>0 such that

βNM≤a.\frac{\beta}{\sqrt N}M\le a.

The result guarantees a positive finite copy number for any positive curvature parameter and finite nonnegative Hessian bound. It is the numerical existence component of the suspension convexity condition.

Formalization Note. The square root uses the real coercion of NN; the conclusion does not specify a particular choice of NN.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave.Suspension. Shown in its original module context. Proof omitted.

theorem exists_copies {a beta M : ℝ} (ha : 0 < a) (hbeta : 0 ≤ beta) (hM : 0 ≤ M) :
    ∃ N : ℕ, 0 < N ∧ beta / Real.sqrt N * M ≤ a

Module navigation

Module: KLS/BKL/Suspension/Basic.

Previous: convexOn_potential.

Source excerpt, lines 108–109 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Suspension_Basic
Formal statement

theorem FunctionalInequalities.KLS.LogConcave.Suspension.exists_copies_readable {a beta M : ℝ} (ha : 0 < a) (hbeta : 0 ≤ beta) (hM : 0 ≤ M) :
    ∃ N : ℕ, 0 < N ∧ beta / Real.sqrt N * M ≤ a := by sorry
Source
Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Proposition 7.1, p. 28. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Suspension/Basic.lean#L106-L123 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Suspension.Basic`, declaration `FunctionalInequalities.KLS.LogConcave.Suspension.exists_copies`; the repository is private at upload time).

View graph