Covariance-normalized KLS conjecture

Definition

KLSModular_FunctionalInequalities_KLS_Statement

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

functional-inequalitiesklskls-conjecturekls-modularletwin2026log-concavemodule-context

KLS.Conjecture is the proposition that there exists one finite NNReal constant C such that, for every natural dimension n and every probability measure μ on EuclideanSpace ℝ (Fin n), log-concavity and L² integrability of the identity imply that the intrinsic local-slope Poincaré constant is at most C times the ENNReal norm of the covariance operator. The quantification includes dimension zero and does not require full-dimensionality or isotropy. This declaration defines a conjecture only; it contains no proof or assertion that the bound holds.

Original module imports

import FunctionalInequalities.Probability.LogConcave
import FunctionalInequalities.Poincare.LocalSlope.Basic
import FunctionalInequalities.Probability.Covariance.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2

Original declaration excerpt

Shown in the original module context.

def Conjecture : Prop :=
  ∃ C : NNReal, ∀ (n : ℕ) (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))),
    LogConcave μ → MemLp id 2 (μ : Measure (EuclideanSpace ℝ (Fin n))) →
      Poincare.LocalSlope.Intrinsic.constant μ ≤ (C : ENNReal) *
        ENNReal.ofReal ‖Covariance.operator (μ : Measure (EuclideanSpace ℝ (Fin n)))‖

Module navigation

Direct project imports: Probability/LogConcave, Poincare/LocalSlope/Basic, Probability/Covariance/Basic.

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.Statement · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_LogConcave
import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_LocalSlope_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Covariance_Basic
import Mathlib.Analysis.InnerProductSpace.PiL2

noncomputable section
open MeasureTheory
namespace FunctionalInequalities
namespace KLS
/-- A dimension-independent covariance-normalized bound for log-concave probability laws. -/
def Conjecture : Prop :=
  ∃ C : NNReal, ∀ (n : ℕ) (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))),
    LogConcave μ → MemLp id 2 (μ : Measure (EuclideanSpace ℝ (Fin n))) →
      Poincare.LocalSlope.Intrinsic.constant μ ≤ (C : ENNReal) *
        ENNReal.ofReal ‖Covariance.operator (μ : Measure (EuclideanSpace ℝ (Fin n)))‖
end KLS
end FunctionalInequalities

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), item CONJ. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/Statement.lean#L27-L32 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.Statement`, definition bundle `KLSModular_FunctionalInequalities_KLS_Statement`; the repository is private at upload time).

View graph