Compact-support cumulant and Letwin hypotheses

Definition

KLSModular_FunctionalInequalities_KLS_BKL_CompactReduction

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

CumulantBoundCompact d b is the universal statement that every compactly supported isotropic log-concave probability measure in every dimension satisfies the order- $d+1$ coordinate cumulant-square bound with constant $b$ . LetwinCompactBound is the universal positive-dimensional statement that every compactly supported isotropic log-concave probability measure satisfies LetwinQuadraticBound. Both are hypotheses encoded as propositions; this bundle does not prove either bound or the associated compact approximation mentioned in the module documentation.

Original module imports

import FunctionalInequalities.KLS.BKL.LocalThirdCumulant
import FunctionalInequalities.Analysis.BakryEmery.Cumulant.Truncation
import FunctionalInequalities.KLS.LogConcave.Transport
import FunctionalInequalities.KLS.LogConcave.Isotropic
import FunctionalInequalities.Analysis.Operator.InverseSqrt
import FunctionalInequalities.Probability.Transport
import FunctionalInequalities.Probability.Conditioning

Original declaration excerpt

Shown in the original module context.

def CumulantBoundCompact (d : ℕ) (b : ℝ) : Prop :=
  ∀ (m : ℕ) (ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin m))),
    KLS.Isotropic ν → _root_.FunctionalInequalities.KLS.LogConcave ν →
      IsCompact (ν : Measure (EuclideanSpace ℝ (Fin m))).support →
      ∀ u : EuclideanSpace ℝ (Fin m),
      ∑ J : Fin d → Fin m, cumulant (ν : Measure (EuclideanSpace ℝ (Fin m))) (d + 1)
        (Fin.cons u fun k => EuclideanSpace.basisFun (Fin m) ℝ (J k)) ^ 2 ≤ b * ‖u‖ ^ 2

Module navigation

Direct project imports: KLS/BKL/LocalThirdCumulant, Analysis/BakryEmery/Cumulant/Truncation, KLS/LogConcave/Transport, KLS/LogConcave/Isotropic, Analysis/Operator/InverseSqrt, Probability/Transport, Probability/Conditioning.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.BKL.CompactReduction · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_LocalThirdCumulant
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Truncation
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Transport
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Isotropic
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Operator_InverseSqrt
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Transport
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Conditioning

noncomputable section
open MeasureTheory
open FunctionalInequalities.Analysis.BakryEmery
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
namespace Suspension
/-- `CumulantBound d b` restricted to compactly supported laws: `R^ν_{d+1} ≤ b Id` for every compactly
supported isotropic log-concave probability measure in every dimension (BKL arXiv:2610.05474v1, p. 19:
Theorem 4.1 is proved for compactly supported laws first). This names the hypothesis. -/
def CumulantBoundCompact (d : ℕ) (b : ℝ) : Prop :=
  ∀ (m : ℕ) (ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin m))),
    KLS.Isotropic ν → _root_.FunctionalInequalities.KLS.LogConcave ν →
      IsCompact (ν : Measure (EuclideanSpace ℝ (Fin m))).support →
      ∀ u : EuclideanSpace ℝ (Fin m),
      ∑ J : Fin d → Fin m, cumulant (ν : Measure (EuclideanSpace ℝ (Fin m))) (d + 1)
        (Fin.cons u fun k => EuclideanSpace.basisFun (Fin m) ℝ (J k)) ^ 2 ≤ b * ‖u‖ ^ 2
/-- Letwin's quadratic-form bound (arXiv:2607.24164v1, Theorem 1.2) for compactly supported isotropic
log-concave laws in positive dimension: the input of BKL Lemma 4.2 used by the localization argument.
This names the hypothesis; it is the interface between the Letwin and the Theorem 4.1 streams. -/
def LetwinCompactBound : Prop :=
  ∀ (n : ℕ), 0 < n → ∀ μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)),
    _root_.FunctionalInequalities.KLS.LogConcave μ → KLS.Isotropic μ →
      IsCompact (μ : Measure (EuclideanSpace ℝ (Fin n))).support →
      LetwinQuadraticBound (μ : Measure (EuclideanSpace ℝ (Fin n)))
end Suspension
end LogConcave
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/CompactReduction.lean#L31-L49 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.CompactReduction`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_CompactReduction`; the repository is private at upload time).

View graph