Concrete Tests and Sequential Relaxation Equivalence

Proved

FunctionalInequalities.Poincare.TestFamily.holds_ofPreEnergy_iff_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the abstract relaxation bridge for a pre-energy.

Let $\mu$ be a probability measure on a measurable space, let $P$ be a pre-energy on the real $L^2(\mu)$ space, and let $C\in\mathbb{NNReal}$ . Then the finite constant $C$ works on the concrete test family generated by $P$ if and only if it works on the finite domain of the sequential relaxation of $P$ :

\mathrm{Holds}_{\mathrm{ofPreEnergy}(\mu,P)}(C) \iff \mathrm{Holds}_{\mathrm{L2Energy}(\mu,\,P.\mathrm{sequentialRelaxation})}(C).

The statement is an abstract comparison result and allows empty test types and infinite optimal constants.

Original Lean declaration header

Within namespace FunctionalInequalities.Poincare.TestFamily. Shown in its original module context. Proof omitted.

theorem holds_ofPreEnergy_iff (C : NNReal) :
    (ofPreEnergy μ P).Holds C ↔ L2Energy.Holds μ P.sequentialRelaxation C

Module navigation

Module: Poincare/Relaxation.

Definition modules: Poincare/SmoothTest/Optimal, Poincare/L2/Energy, Energy/Relaxation/Basic.

Supporting theorems: hasRecoverySequenceAt_sequentialRelaxation_of_finiteAt.

Source excerpt, lines 38–39 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_Relaxation

universe u
variable {α : Type u} [MeasurableSpace α] (μ : MeasureTheory.ProbabilityMeasure α)
  (P : FunctionalInequalities.Energy.PreEnergy (MeasureTheory.Lp ℝ 2 (μ : MeasureTheory.Measure α)))

Formal statement


theorem FunctionalInequalities.Poincare.TestFamily.holds_ofPreEnergy_iff_readable (C : NNReal) :
    (ofPreEnergy μ P).Holds C ↔ L2Energy.Holds μ P.sequentialRelaxation C := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Poincare/Relaxation.lean#L36-L57 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Poincare.Relaxation`, declaration `FunctionalInequalities.Poincare.TestFamily.holds_ofPreEnergy_iff`; the repository is private at upload time).

View graph