Poincaré Constants Under Isometric Energy Equivalence

This is an invariance principle for optimal extended-energy Poincaré constants.

Let $\mu$ and $\mu'$ be probability measures on measurable spaces $\alpha$ and $\beta$. Let energy and energy' be extended-valued energy functionals on the corresponding real $L^2$ spaces, and let $e:L^2(\mu')\simeq L^2(\mu)$ be a real linear isometric equivalence. Assume that for every $f$, variance is preserved:

and that the energies intertwine:

Then their optimal Poincaré constants are equal:

The functionals may take the value $\infty$; the statement compares exactly the finite-energy domains and does not assume closedness, quadraticity, or a Markov property.

Original Lean declaration header

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

theorem constant_eq_of_linearIsometryEquiv {β : Type*} [MeasurableSpace β]
    (μ : ProbabilityMeasure α) (μ' : ProbabilityMeasure β)
    (energy : Energy.Functional (Lp ℝ 2 (μ : Measure α)))
    (energy' : Energy.Functional (Lp ℝ 2 (μ' : Measure β)))
    (e : Lp ℝ 2 (μ' : Measure β) ≃ₗᵢ[ℝ] Lp ℝ 2 (μ : Measure α))
    (hvar : ∀ f, L2.variance μ (e f) = L2.variance μ' f)
    (henergy : ∀ f, energy' f = energy (e f)) :
    constant μ' energy' = constant μ energy

Module navigation

Module: Poincare/L2/Energy.

Definition modules: Energy/Form/Functional, L2/MeanVariance.

Source excerpt, lines 89–96 · Frozen source 408915f.