Weak-Limit Passage for a Fixed Compactly Supported Smooth Test

This is a fixed-test weak-limit transfer statement associated with Bizeul–Klartag–Lehec (arXiv:2610.05474v1), Section 2, (12), p. 5 (unnumbered), and its regular-approximation reduction.

Let $E$ be a complete real inner product space with its Borel measurable structure. Assume:

1. Probability measures $\mu_j$ converge weakly to a probability measure $\mu$ as $j\in\mathbb N$ tends to infinity.
2. Real numbers $C_j$ converge to $C\in\mathbb R$.
3. $f:E\to\mathbb R$ is $C^\infty$ with compact support.
4. For every $j$, $\operatorname{Var}_{\mu_j}(f)\le C_j\int\|\nabla f\|^2\,d\mu_j$.

Then

This transfers the inequality for the specified test, rather than asserting a bound for all tests at once.

Formalization Note The energy is Poincare.SmoothTest.energy, and variance is ProbabilityTheory.variance. No finite-dimensionality, log-concavity, or nonnegativity assumption on $C_j$ or $C$ is present.

Original Lean declaration header

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

theorem variance_le_mul_energy_of_tendsto {μs : ℕ → ProbabilityMeasure E} {μ : ProbabilityMeasure E}
    (hlim : Tendsto μs atTop (𝓝 μ)) {Cseq : ℕ → ℝ} {C : ℝ} (hC : Tendsto Cseq atTop (𝓝 C))
    {f : E → ℝ} (hf : ContDiff ℝ ∞ f) (hc : HasCompactSupport f)
    (h : ∀ j, variance f (μs j : Measure E) ≤ Cseq j * energy (μs j : Measure E) f) :
    variance f (μ : Measure E) ≤ C * energy (μ : Measure E) f

Module navigation

Module: Poincare/SmoothTest/WeakLimit.

Definition modules: Poincare/SmoothTest/Basic.

Next: Admissible.of_contDiff_hasCompactSupport.

Source excerpt, lines 31–35 · Frozen source 408915f.