Isotropic probability law

Definition

KLSModular_FunctionalInequalities_KLS_Isotropic

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

functional-inequalitiesguedonmilman2011jambulapatileevempala2022klartaglehec2022klskls-conjecturekls-modularletwin2026log-concavemodule-context

FunctionalInequalities.KLS.Isotropic μ is a proposition for a probability measure $\mu$ on a complete real inner-product space requiring three fields: memLp_two says that the identity map has finite second moment, mean_zero says $\int x\,d\mu=0$ , and covariance_identity says the centered covariance operator Covariance.operator is the identity continuous linear map. The structure is only a definition of isotropy and includes no whitening or equivalence theorem.

Original module imports

import FunctionalInequalities.Probability.Covariance.Basic
import FunctionalInequalities.Probability.Basic
import Mathlib.MeasureTheory.Function.LpSpace.Basic
import Mathlib.Analysis.Calculus.Gradient.Basic
import FunctionalInequalities.Analysis.BakryEmery.IntegrationByParts.Basic
import FunctionalInequalities.Analysis.BakryEmery.IntegrationByParts.ConvexHessian
import FunctionalInequalities.Analysis.Matrix.Sign
import Mathlib.Probability.Moments.CovarianceBilin
import Mathlib.Analysis.CStarAlgebra.Matrix

Original declaration excerpt

Shown in the original module context.

structure Isotropic (μ : ProbabilityMeasure E) : Prop where
  memLp_two : MemLp id 2 (μ : Measure E)
  mean_zero : ∫ x, x ∂(μ : Measure E) = 0
  covariance_identity : Covariance.operator (μ : Measure E) = ContinuousLinearMap.id ℝ E

Module navigation

Direct project imports: Probability/Covariance/Basic, Probability/Basic, Analysis/BakryEmery/IntegrationByParts/Basic, Analysis/BakryEmery/IntegrationByParts/ConvexHessian, Analysis/Matrix/Sign.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Covariance_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Basic
import Mathlib.MeasureTheory.Function.LpSpace.Basic
import Mathlib.Analysis.Calculus.Gradient.Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_ConvexHessian
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Sign
import Mathlib.Probability.Moments.CovarianceBilin
import Mathlib.Analysis.CStarAlgebra.Matrix

noncomputable section
open MeasureTheory
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace KLS
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
variable [MeasurableSpace E] [BorelSpace E]
/-- A probability law with finite second moment, mean zero, and identity centered covariance.
The moment field prevents the totalized integral/covariance from encoding integrability. -/
structure Isotropic (μ : ProbabilityMeasure E) : Prop where
  memLp_two : MemLp id 2 (μ : Measure E)
  mean_zero : ∫ x, x ∂(μ : Measure E) = 0
  covariance_identity : Covariance.operator (μ : Measure E) = ContinuousLinearMap.id ℝ E
end KLS
end FunctionalInequalities

Source

Source: Guédon–Milman, Interpolating thin-shell and sharp large-deviation estimates for isotropic log-concave measures (arXiv:1011.0943v3), item DISO; Jambulapati–Lee–Vempala, A slightly improved bound for the KLS constant (arXiv:2208.11644v2), item D3; Klartag–Lehec, Bourgain’s slicing problem and KLS isoperimetry up to polylog (arXiv:2203.15551v2), item D3; Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), item DISO. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/Isotropic.lean#L30-L35 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.Isotropic`, definition bundle `KLSModular_FunctionalInequalities_KLS_Isotropic`; the repository is private at upload time).

View graph