Intrinsic affine covariance-gradient Poincaré constant

Definition

KLSModular_FunctionalInequalities_Poincare_CovarianceGradient_Intrinsic

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a finite-dimensional real Hilbert space E and a probability measure μ on E, Poincare.CovarianceGradient.Intrinsic.constant applies the generic real-L² optimizer L2Energy.constant to the intrinsic law of μ and the intrinsic covariance-gradient energy. The corresponding Holds predicate records validity of a finite NNReal constant on the finite-energy domain of that relaxation. The definitions make no finiteness, log-concavity, closability, isotropy, or KLS assertion.

Original module imports

import FunctionalInequalities.Energy.CovarianceGradient.Basic
import FunctionalInequalities.Poincare.L2.Energy

Original declaration excerpt

Shown in the original module context.

def constant (μ : ProbabilityMeasure E) : ENNReal :=
  L2Energy.constant (Probability.intrinsicMeasure μ) (Energy.CovarianceGradient.Intrinsic.energy μ)

Module navigation

Direct project imports: Energy/CovarianceGradient/Basic, Poincare/L2/Energy.

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Poincare.CovarianceGradient.Intrinsic · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_CovarianceGradient_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_L2_Energy

noncomputable section
open MeasureTheory
namespace FunctionalInequalities
namespace Poincare
namespace CovarianceGradient
namespace Intrinsic
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
  [FiniteDimensional ℝ E]
/-- The affine covariance Poincaré constant `C_P^aff(μ)`: the optimal extended constant of the
affine covariance relaxation on the intrinsic law. -/
def constant (μ : ProbabilityMeasure E) : ENNReal :=
  L2Energy.constant (Probability.intrinsicMeasure μ) (Energy.CovarianceGradient.Intrinsic.energy μ)
/-- Validity of a finite constant on the finite-energy domain of the affine covariance
relaxation of the intrinsic law. -/
def Holds (μ : ProbabilityMeasure E) (C : NNReal) : Prop :=
  L2Energy.Holds (Probability.intrinsicMeasure μ) (Energy.CovarianceGradient.Intrinsic.energy μ) C
end Intrinsic
end CovarianceGradient
end Poincare
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Poincare/CovarianceGradient/Intrinsic.lean#L40-L48 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Poincare.CovarianceGradient.Intrinsic`, definition bundle `KLSModular_FunctionalInequalities_Poincare_CovarianceGradient_Intrinsic`; the repository is private at upload time).

View graph