Transfer of Poincaré Bounds Through Energy Comparison

This is a comparison rule for extended-valued $L^2$ energies.

Let $\mu$ be a probability measure, let source and target be energy functionals on $L^2(\mu)$, and let $C,\kappa\in\mathbb{NNReal}$. Assume:

1. the source Poincaré inequality holds with constant $C$;
2. on every finite-energy target test $f$, the source energy is bounded by $\kappa$ times the target energy:

Then the target Poincaré inequality holds with constant $\kappa C$:

The energies and their finite values are ENNReal-valued, so the comparison explicitly handles finite-energy domains, zero constants, and the possibility of infinite optimal constants.

Original Lean declaration header

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

theorem Holds.of_energy_le_mul {μ : ProbabilityMeasure α}
    {source target : Energy.Functional (Lp ℝ 2 (μ : Measure α))} {C κ : NNReal}
    (hC : Holds μ source C)
    (henergy : ∀ f : target.domain,
      source f.1 ≤ (κ : ENNReal) * target f.1) :
    Holds μ target (κ * C)

Module navigation

Module: Poincare/L2/Comparison.

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

Source excerpt, lines 44–49 · Frozen source 408915f.