Smooth-Test Bounds Equivalent to Smooth Pre-Energy Test-Family Bounds

This statement identifies two fixed-constant formulations of the smooth-gradient Poincaré inequality.

Let $E$ be a finite-dimensional complete real inner product space with its Borel measurable structure and a second-countable topology. Let $\mu$ be any probability measure on $E$ and $C\in[0,\infty)$. Let $\mathcal T_\mu$ be the test family Poincare.TestFamily.ofPreEnergy μ (Energy.SmoothGradient.preEnergy μ).

Then

The left side is Poincare.SmoothTest.Holds: variance is at most $C\int\|\nabla f\|^2\,d\mu$ for every $C^\infty$ function $f\in L^2(\mu)$ with integrable squared gradient. The right side is the corresponding inequality on the concrete pre-energy test family.

This equivalence connects the concrete smooth-test formulation to the test-family interface, without asserting an identification with a relaxed or literature constant.

Formalization Note $C$ is NNReal and is coerced to $\mathbb R$ on the left. No moment, log-concavity, density, or positive-dimension assumption is imposed on $\mu$.

Original Lean declaration header

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

theorem holds_iff_preEnergy (C : NNReal) :
    Holds (μ : Measure E) (C : ℝ) ↔
      (TestFamily.ofPreEnergy μ (Energy.SmoothGradient.preEnergy μ)).Holds C

Module navigation

Module: Poincare/SmoothTest/Comparison.

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

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