Poincaré test family from a finite pre-energy
DefinitionKLSModular_FunctionalInequalities_Poincare_RelaxationPoincare.TestFamily.ofPreEnergy builds a test family from a pre-energy on real L²(μ), assigning each concrete test the variance of its ambient L² realization and its original finite energy. The bundle contains only this family definition; it does not itself state density, quadraticity, or a comparison between the pre-energy and its sequential relaxation. The associated framework permits empty test types and extended optimal constants, including ⊤.
Original module imports
import FunctionalInequalities.Energy.Relaxation.Recovery
import FunctionalInequalities.Poincare.L2.Energy
Original declaration excerpt
Shown in the original module context.
def ofPreEnergy : TestFamily where
Test := P.Test
variance f := L2.variance μ (P.toAmbient f)
energy := P.energy
Module navigation
Direct project imports: Energy/Relaxation/Recovery, Poincare/L2/Energy.
Theorems in source order:
Project result: The KLS conjecture.
Original module · FunctionalInequalities.Poincare.Relaxation · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Relaxation_Recovery
import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_L2_Energy
noncomputable section
open MeasureTheory Filter Topology
namespace FunctionalInequalities
namespace Poincare
namespace TestFamily
universe u
variable {α : Type u} [MeasurableSpace α] (μ : ProbabilityMeasure α)
(P : Energy.PreEnergy (Lp ℝ 2 (μ : Measure α)))
/-- Concrete tests with the variance of their `L²` realizations and their raw finite energy. -/
def ofPreEnergy : TestFamily where
Test := P.Test
variance f := L2.variance μ (P.toAmbient f)
energy := P.energy
end TestFamily
end Poincare
end FunctionalInequalities