Convergence Of Haar Pairings For Vector Fields

This theorem transfers $L^2(\nu;V)$ convergence of vector fields to convergence of localized Haar pairings.

Let $V$ be a finite-dimensional real inner-product space, 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:V\to V$ are all in $L^2(\nu;V)$ and their MemLp.toLp classes converge to $F\in L^2(\nu;V)$. If $\psi:V\to\mathbb R$ is continuous and compactly supported, then for every direction $w\in V$,

The result is useful when passing from graph approximations in $L^2(\nu;V)$ to weak identities written with respect to the Haar measure. The compact support of $\psi$ supplies the required local integrability.

Original Lean declaration header

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

theorem tendsto_integral_mul_inner_of_tendsto (hνU : (ν : Measure V) = m.tilted (-U))
    (hU : Continuous U) {G : ℕ → V → V} (hG : ∀ n, MemLp (G n) 2 (ν : Measure V))
    {F : Lp V 2 (ν : Measure V)} (hlim : Tendsto (fun n => (hG n).toLp (G n)) atTop (𝓝 F))
    {ψ : V → ℝ} (hψ : Continuous ψ) (hψc : HasCompactSupport ψ) (w : V) :
    Tendsto (fun n => ∫ x, ψ x * ⟪G n x, w⟫ ∂m) atTop (𝓝 (∫ x, ψ x * ⟪F x, w⟫ ∂m))

Module navigation

Module: KLS/LogConcave/WeightedGradient/Kernel.

Supporting theorems: integral_eq_integral_mul_exp.

Previous: tendsto_integral_mul_of_tendsto · Next: integral_mul_fderiv_eq_neg_integral_mul_inner.

Source excerpt, lines 234–238 · Frozen source 408915f.