Reduction of Compact Bounds to the Regular Class

Proved

FunctionalInequalities.KLS.LogConcave.Suspension.letwinCompactBound_of_regularClass_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This formalizes the reduction in Lemma A.1 and Theorem 1.2 of Letwin (arXiv:2607.24164v1).

Assume that for every $n>0$ , every compact convex $K\subseteq\mathbb R^n$ with nonempty interior, every $C^\infty$ function $W$ , every $κ>0$ for which $W-(κ/2)\|\cdot\|^2$ is convex, and every isotropic probability measure $μ$ satisfying

μ=\operatorname{volume}.\operatorname{withDensity}\!\left(1_K(x)\,\operatorname{ENNReal.ofReal}(e^{-W(x)})\right),

the predicate LetwinQuadraticBound μ holds. Then LetwinCompactBound holds for every compactly supported isotropic log-concave probability measure in every positive dimension.

This is an implication between bound predicates: it does not itself state a universal KLS estimate.

Original Lean declaration header

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

theorem letwinCompactBound_of_regularClass
    (h : ∀ (n : ℕ), 0 < n → ∀ (K : Set (EuclideanSpace ℝ (Fin n))) (W : EuclideanSpace ℝ (Fin n) → ℝ)
      (κ : ℝ), 0 < κ → IsCompact K → Convex ℝ K → (interior K).Nonempty → ContDiff ℝ ∞ W →
      ConvexOn ℝ univ (fun y => W y - (κ / 2) * ‖y‖ ^ 2) →
      ∀ μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)),
        (μ : Measure (EuclideanSpace ℝ (Fin n))) =
          (volume : Measure (EuclideanSpace ℝ (Fin n))).withDensity
            (K.indicator fun p => ENNReal.ofReal (Real.exp (-W p))) →
        KLS.Isotropic μ → LetwinQuadraticBound (μ : Measure (EuclideanSpace ℝ (Fin n)))) :
    LetwinCompactBound

Module navigation

Module: KLS/BKL/LetwinApproximation.

Definition modules: KLS/Isotropic, KLS/BKL/CompactReduction, Analysis/BakryEmery/Cumulant/Basic.

Supporting theorems: letwinQuadraticBound_of_tendsto_moments, exists_integrable_exp_norm, exists_regularClass_seq_of_compact, logConcave_of_eq_regularClass.

Source excerpt, lines 30–39 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_LetwinApproximation

open MeasureTheory Set Metric Filter
open scoped RealInnerProductSpace ContDiff Topology
open FunctionalInequalities.Analysis.BakryEmery

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.Suspension.letwinCompactBound_of_regularClass_readable
    (h : ∀ (n : ℕ), 0 < n → ∀ (K : Set (EuclideanSpace ℝ (Fin n))) (W : EuclideanSpace ℝ (Fin n) → ℝ)
      (κ : ℝ), 0 < κ → IsCompact K → Convex ℝ K → (interior K).Nonempty → ContDiff ℝ ∞ W →
      ConvexOn ℝ univ (fun y => W y - (κ / 2) * ‖y‖ ^ 2) →
      ∀ μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)),
        (μ : Measure (EuclideanSpace ℝ (Fin n))) =
          (volume : Measure (EuclideanSpace ℝ (Fin n))).withDensity
            (K.indicator fun p => ENNReal.ofReal (Real.exp (-W p))) →
        KLS.Isotropic μ → LetwinQuadraticBound (μ : Measure (EuclideanSpace ℝ (Fin n)))) :
    LetwinCompactBound := by sorry

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Theorem 1.2; Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Lemma A.1. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/LetwinApproximation.lean#L27-L53 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.LetwinApproximation`, declaration `FunctionalInequalities.KLS.LogConcave.Suspension.letwinCompactBound_of_regularClass`; the repository is private at upload time).

View graph