Poincaré constants for extended energies on real L²

Definition

KLSModular_FunctionalInequalities_Poincare_L2_Energy

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a probability measure μ on a measurable space and an extended energy functional on real L²(μ), TestFamily.ofL2Energy uses exactly the finite-energy domain as its test type. Each test has intrinsic L² variance L2.variance μ f.1 and the finite energy value certified by the domain subtype. L2Energy.constant is the resulting extended optimal Poincaré constant, while L2Energy.Holds states that a finite NNReal constant is valid for every finite-energy test. No closedness, quadraticity, or Markov property is assumed.

Original module imports

import FunctionalInequalities.Energy.Form.Functional
import FunctionalInequalities.L2.MeanVariance
import FunctionalInequalities.Poincare.SmoothTest.Optimal

Original declaration excerpt

Shown in the original module context.

def ofL2Energy (μ : ProbabilityMeasure α)
    (energy : Energy.Functional (Lp ℝ 2 (μ : Measure α))) : TestFamily where
  Test := energy.domain
  variance f := L2.variance μ f.1
  energy f := energy.finiteValue f

Module navigation

Direct project imports: Energy/Form/Functional, L2/MeanVariance, Poincare/SmoothTest/Optimal.

Theorems in source order:

constant_eq_of_linearIsometryEquiv

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Poincare.L2.Energy · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Form_Functional
import Definitions.Def_KLSModular_FunctionalInequalities_L2_MeanVariance
import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_SmoothTest_Optimal

noncomputable section
open MeasureTheory
namespace FunctionalInequalities
namespace Poincare
universe u
variable {α : Type u} [MeasurableSpace α]
namespace TestFamily
/-- The finite-energy domain of an extended functional on real `L²(μ)`, equipped with
intrinsic `L²` variance and the functional's finite value. -/
def ofL2Energy (μ : ProbabilityMeasure α)
    (energy : Energy.Functional (Lp ℝ 2 (μ : Measure α))) : TestFamily where
  Test := energy.domain
  variance f := L2.variance μ f.1
  energy f := energy.finiteValue f
/-- Variance in the induced test family is intrinsic `L²` variance. -/
@[simp]
theorem ofL2Energy_variance (μ : ProbabilityMeasure α)
    (energy : Energy.Functional (Lp ℝ 2 (μ : Measure α)))
    (f : energy.domain) :
    (ofL2Energy μ energy).variance f = L2.variance μ f.1 :=
  rfl
/-- Energy in the induced test family is the finite value certified by the domain subtype. -/
@[simp]
theorem ofL2Energy_energy (μ : ProbabilityMeasure α)
    (energy : Energy.Functional (Lp ℝ 2 (μ : Measure α)))
    (f : energy.domain) :
    (ofL2Energy μ energy).energy f = energy.finiteValue f :=
  rfl
end TestFamily
namespace L2Energy
/-- The optimal extended Poincaré constant of an energy on real `L²(μ)`. -/
def constant (μ : ProbabilityMeasure α)
    (energy : Energy.Functional (Lp ℝ 2 (μ : Measure α))) : ENNReal :=
  (TestFamily.ofL2Energy μ energy).constant
/-- A finite Poincaré constant is valid on every finite-energy `L²` test. -/
def Holds (μ : ProbabilityMeasure α)
    (energy : Energy.Functional (Lp ℝ 2 (μ : Measure α))) (C : NNReal) : Prop :=
  (TestFamily.ofL2Energy μ energy).Holds C
end L2Energy
end Poincare
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Poincare/L2/Energy.lean#L27-L63 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Poincare.L2.Energy`, definition bundle `KLSModular_FunctionalInequalities_Poincare_L2_Energy`; the repository is private at upload time).

View graph