Convergence Of Haar Pairings For Scalar Functions

This theorem transfers scalar $L^2(\nu)$ convergence to convergence of Haar integrals against compactly supported weights.

Let $V$ be a finite-dimensional real vector space with the stated Borel and topological structures, let $m$ be an additive Haar measure, let $\nu$ be a probability measure, and let $U:V\to\mathbb R$ be continuous with $\nu=m.\operatorname{tilted}(-U)$. Suppose $g_n\in L^2(\nu)$ and the classes of $g_n$ converge to $f\in L^2(\nu)$. For every continuous compactly supported $\psi:V\to\mathbb R$,

This is a technical localization lemma used to pass $L^2(\nu)$ limits through Haar integrals. No global integrability of the functions with respect to $m$ is required beyond what follows from the tilted-law and compact-support hypotheses.

Original Lean declaration header

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

theorem tendsto_integral_mul_of_tendsto (hνU : (ν : Measure V) = m.tilted (-U))
    (hU : Continuous U) {g : ℕ → V → ℝ} (hg : ∀ n, MemLp (g n) 2 (ν : Measure V))
    {f : Lp ℝ 2 (ν : Measure V)} (hlim : Tendsto (fun n => (hg n).toLp (g n)) atTop (𝓝 f))
    {ψ : V → ℝ} (hψ : Continuous ψ) (hψc : HasCompactSupport ψ) :
    Tendsto (fun n => ∫ x, g n x * ψ x ∂m) atTop (𝓝 (∫ x, f x * ψ x ∂m))

Module navigation

Module: KLS/LogConcave/WeightedGradient/Kernel.

Supporting theorems: integrable_exp_neg_of_eq_tilted, integral_eq_integral_mul_exp.

Previous: restrict_le_smul_of_eq_tilted · Next: tendsto_integral_mul_inner_of_tendsto.

Source excerpt, lines 148–152 · Frozen source 408915f.