Intrinsic smooth-gradient Poincaré constant

Definition

KLSModular_FunctionalInequalities_Poincare_SmoothGradient_Intrinsic

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

Poincare.SmoothGradient.Intrinsic.constant μ applies the generic real-L² Poincaré optimizer to the intrinsic-affine smooth-gradient relaxation Energy.SmoothGradient.Intrinsic.energy μ. The variance is the intrinsic L²(μ) variance of the original probability law, while the energy is evaluated through the intrinsic-coordinate presentation. The definition does not assert a Cheeger, spectral, or KLS identification.

Original module imports

import FunctionalInequalities.Energy.SmoothGradient.Intrinsic.Closed
import FunctionalInequalities.Poincare.L2.Energy

Original declaration excerpt

Shown in the original module context.

def constant (μ : ProbabilityMeasure E) : ENNReal :=
  L2Energy.constant μ
    (Energy.SmoothGradient.Intrinsic.energy μ)

Module navigation

Direct project imports: Energy/SmoothGradient/Intrinsic/Closed, Poincare/L2/Energy.

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_SmoothGradient_Intrinsic_Closed
import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_L2_Energy

noncomputable section
open MeasureTheory
namespace FunctionalInequalities
namespace Poincare
namespace SmoothGradient
namespace Intrinsic
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
  [FiniteDimensional ℝ E]
/-- The optimal Poincaré constant of the intrinsic-affine smooth-gradient relaxation. -/
def constant (μ : ProbabilityMeasure E) : ENNReal :=
  L2Energy.constant μ
    (Energy.SmoothGradient.Intrinsic.energy μ)
end Intrinsic
end SmoothGradient
end Poincare
end FunctionalInequalities

Source

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

View graph