Extension of Compactly Supported Smooth-Test Poincaré Bounds

This is the compact-support extension step associated with the regular-approximation reduction in Bizeul–Klartag–Lehec (arXiv:2610.05474v1), Section 2, (12), p. 5 (unnumbered).

Let $E$ be a finite-dimensional complete real inner product space with its Borel measurable structure, let $\mu$ be a probability measure, and let $C\in\mathbb R$. Assume:

1. $C\ge0$.
2. Every compactly supported admissible $f:E\to\mathbb R$ satisfies $\operatorname{Var}_\mu(f)\le C\mathcal E_\mu(f)$.

Here admissibility (Poincare.SmoothTest.Admissible) means $C^\infty$ smoothness, membership in $L^2(\mu)$, and integrability of $\|\nabla f\|^2$; $\mathcal E_\mu(f)=\int\|\nabla f\|^2\,d\mu$ is Poincare.SmoothTest.energy.

Then Poincare.SmoothTest.Holds μ C holds, namely

This removes the compact-support restriction on the tests. It does not assume log-concavity or establish the paper's regular-density conditions.

Original Lean declaration header

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

theorem Holds.of_compactSupport {μ : Measure E} [IsProbabilityMeasure μ] {C : ℝ} (hC : 0 ≤ C)
    (h : ∀ f : E → ℝ, Admissible μ f → HasCompactSupport f → variance f μ ≤ C * energy μ f) :
    Holds μ C

Module navigation

Module: Poincare/SmoothTest/WeakLimit.

Definition modules: Poincare/SmoothTest/Basic.

Supporting theorems: Admissible.of_contDiff_hasCompactSupport, tendsto_energy_scaled_mul, tendsto_integral_scaled_mul.

Previous: tendsto_energy_scaled_mul.

Source excerpt, lines 532–534 · Frozen source 408915f.