Literature Poincaré Bound at a Log-Concave Weak Limit

This formalizes the weak-limit transfer step of the regular-approximation reduction associated with 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 and a second-countable topology. Assume:

1. Probability measures $\mu_j$ converge weakly to a log-concave probability measure $\mu$ (KLS.LogConcave).
2. $C_j,C\in[0,\infty)$ and $C_j\to C$.
3. Each $\mu_j$ satisfies Poincare.SmoothTest.Holds with real constant $C_j$: every admissible smooth test satisfies $\operatorname{Var}_{\mu_j}(f)\le C_j\int\|\nabla f\|^2\,d\mu_j$. Admissibility requires $f\in C^\infty\cap L^2(\mu_j)$ and integrable squared gradient.

Then the intrinsic literature local-slope constant satisfies

This transfers supplied smooth-test bounds to the literature constant of the limit; the approximating laws need not be log-concave.

Formalization Note $C_P^{\mathrm{lit}}$ is Poincare.LocalSlope.Intrinsic.constant, valued in ENNReal. The constants are NNReal, coerced to reals in the hypotheses and to ENNReal in the conclusion.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave. Shown in its original module context. Proof omitted.

theorem localSlope_constant_le_of_tendsto (μs : ℕ → ProbabilityMeasure E)
    (μ : ProbabilityMeasure E) (hμ : LogConcave μ) (Cseq : ℕ → NNReal) (C : NNReal)
    (hlim : Tendsto μs atTop (𝓝 μ)) (hClim : Tendsto Cseq atTop (𝓝 C))
    (hbound : ∀ j, Poincare.SmoothTest.Holds (μs j : Measure E) (Cseq j : ℝ)) :
    Poincare.LocalSlope.Intrinsic.constant μ ≤ (C : ENNReal)

Module navigation

Module: KLS/LogConcave/WeakLimit.

Definition modules: Probability/LogConcave, Poincare/LocalSlope/Basic, Poincare/SmoothTest/Basic.

Selected supporting theorems: exists_ambient_extension, Admissible.of_contDiff_hasCompactSupport, Holds.of_compactSupport, holds_iff_localSlope, variance_le_mul_energy_of_tendsto.

Source excerpt, lines 28–32 · Frozen source 408915f.