Isotropic, covariance, and affine KLS bounds

Definition

KLSModular_FunctionalInequalities_KLS_LogConcave_Isotropic

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

KLS.IsotropicBound K states that every log-concave probability measure on every finite-dimensional space in universe u that is isotropic has intrinsic local-slope Poincaré constant at most the nonnegative constant $K$ . KLS.CovarianceBound K instead bounds the intrinsic constant for every log-concave probability measure by $K$ times ENNReal.ofReal ‖Covariance.operator μ‖, while KLS.AffineBound K bounds the intrinsic covariance-gradient constant by $K$ ; all three are definitions of propositions and do not themselves assert that any such $K$ exists.

Original module imports

import FunctionalInequalities.Energy.CovarianceGradient.LinearEquiv
import FunctionalInequalities.KLS.Isotropic
import FunctionalInequalities.KLS.LogConcave.Translation
import FunctionalInequalities.KLS.LogConcave.Density.BorellRepresentation.Moments
import FunctionalInequalities.KLS.LogConcave.WeightedGradient.Basic
import FunctionalInequalities.KLS.Statement
import FunctionalInequalities.Poincare.LipschitzGradient.Comparison
import FunctionalInequalities.Poincare.L2.Comparison
import FunctionalInequalities.KLS.LogConcave.Poincare
import FunctionalInequalities.Probability.Covariance.Whitening
import FunctionalInequalities.Probability.Covariance.Intrinsic

Original declaration excerpt

Shown in the original module context.

def IsotropicBound (K : NNReal) : Prop :=
  ∀ (V : Type u) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
    [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
    (ν : ProbabilityMeasure V), LogConcave ν → Isotropic ν → Poincare.LocalSlope.Intrinsic.constant ν ≤ (K : ENNReal)

Module navigation

Direct project imports: Energy/CovarianceGradient/LinearEquiv, KLS/Isotropic, KLS/LogConcave/Translation, KLS/LogConcave/Density/BorellRepresentation/Moments, KLS/LogConcave/WeightedGradient/Basic, KLS/Statement, Poincare/LipschitzGradient/Comparison, Poincare/L2/Comparison, KLS/LogConcave/Poincare, Probability/Covariance/Whitening, Probability/Covariance/Intrinsic.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.LogConcave.Isotropic · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_CovarianceGradient_LinearEquiv
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_Isotropic
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Translation
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_BorellRepresentation_Moments
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_WeightedGradient_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_Statement
import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_LipschitzGradient_Comparison
import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_L2_Comparison
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Poincare
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Covariance_Whitening
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Covariance_Intrinsic

noncomputable section
open MeasureTheory Filter Topology InnerProductSpace
namespace FunctionalInequalities
open Energy Energy.Euclidean Probability
section Statements
universe u
namespace KLS
/-- Item (1): every isotropic log-concave law on every finite-dimensional Euclidean space of the
universe `u` has literature constant at most `K`. -/
def IsotropicBound (K : NNReal) : Prop :=
  ∀ (V : Type u) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
    [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
    (ν : ProbabilityMeasure V), LogConcave ν → Isotropic ν → Poincare.LocalSlope.Intrinsic.constant ν ≤ (K : ENNReal)
/-- Item (2): every log-concave law on every finite-dimensional Euclidean space of the universe `u`
has literature constant at most `K` times the operator norm of its covariance. -/
def CovarianceBound (K : NNReal) : Prop :=
  ∀ (E : Type u) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E]
    (μ : ProbabilityMeasure E), LogConcave μ →
      Poincare.LocalSlope.Intrinsic.constant μ ≤ (K : ENNReal) * ENNReal.ofReal ‖Covariance.operator (μ : Measure E)‖
/-- Item (3): every log-concave law on every finite-dimensional Euclidean space of the universe `u`
has affine covariance Poincaré constant at most `K`. -/
def AffineBound (K : NNReal) : Prop :=
  ∀ (E : Type u) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E]
    (μ : ProbabilityMeasure E), LogConcave μ → Poincare.CovarianceGradient.Intrinsic.constant μ ≤ (K : ENNReal)
end KLS
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E]
end Statements
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/Isotropic.lean#L165-L185 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.Isotropic`, definition bundle `KLSModular_FunctionalInequalities_KLS_LogConcave_Isotropic`; the repository is private at upload time).

View graph