Compact continuous pairings respect Lp convergence

Proved

MeasureTheory.tendsto_integral_mul_of_eLpNorm

by Mazecto · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

convergenceintegrationlp-spacesmeasure-theory

Let $\mu$ be a locally finite Borel measure on $\mathbb R^n$ , $1\le p<\infty$ , and $u_j,v\in L^p(\mu)$ . If $\|u_j-v\|_p\to0$ , then for every continuous compactly supported $\psi$ ,

\int u_j\psi\,d\mu\longrightarrow\int v\psi\,d\mu.

The compact support has finite measure and the conjugate exponent estimate controls the integral difference; at $p=1$ use the supremum norm of $\psi$ . The formulation covers restricted volume and boundary volume, including dimension zero.

Preamble

import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
open MeasureTheory Filter
open scoped ENNReal Topology
set_option autoImplicit false

Formal statement

theorem MeasureTheory.tendsto_integral_mul_of_eLpNorm {n : ℕ} {p : ℝ≥0∞}
    (hp : 1 ≤ p) (hp' : p ≠ ∞)
    (μ : Measure (EuclideanSpace ℝ (Fin n))) [IsLocallyFiniteMeasure μ]
    (u : ℕ → EuclideanSpace ℝ (Fin n) → ℝ) (v : EuclideanSpace ℝ (Fin n) → ℝ)
    (hu : ∀ j, MemLp (u j) p μ) (hv : MemLp v p μ)
    (hlim : Tendsto (fun j => eLpNorm (u j - v) p μ) atTop (𝓝 0))
    (ψ : EuclideanSpace ℝ (Fin n) → ℝ) (hψ : Continuous ψ) (hc : HasCompactSupport ψ) :
    Tendsto (fun j => ∫ x, u j x * ψ x ∂μ) atTop (𝓝 (∫ x, v x * ψ x ∂μ)) := by sorry

Source

Mathlib 0df444a360eaa60ab8c11dca51a86af692955474, Mathlib/MeasureTheory/Integral/Bochner/Basic.lean, tendsto_integral_of_L1, and the Holder inequality for conjugate Lp exponents in Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean. Standard compact-test consequence used in Hunter, Notes on PDEs, https://www.math.ucdavis.edu/~hunter/pdes/ch3.pdf, Theorems 3.42–3.44, printed pp. 72–73.

View graph