Prove2Me

An L^p-Cauchy family indexed by ε → 0⁺ converges in L^p

Proved
DbarRegularity.exists_memLp_tendsto_eLpNorm_sub

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

functional-analysislp-spacesmeasure-theory

Let (α,μ)(\alpha,\mu) be a measure space, EE a Banach space and 1≤p≤∞1\le p\le\infty. Let (uε)ε>0(u_\varepsilon)_{\varepsilon>0} be functions α→E\alpha\to E with uε∈Lp(μ)u_\varepsilon\in L^p(\mu) for every ε>0\varepsilon>0, and suppose that for every δ>0\delta>0 there is η0>0\eta_0>0 with ∥uε−uη∥p≤δ\|u_\varepsilon-u_\eta\|_p\le\delta whenever 0<ε,η<η00<\varepsilon,\eta<\eta_0. Then there is g∈Lp(μ)g\in L^p(\mu) with

∥uε−g∥p→0(ε→0+).\|u_\varepsilon-g\|_p\to0\qquad(\varepsilon\to0^+).

This is completeness of LpL^p for families indexed by ε→0+\varepsilon\to0^+.

Formalization Note. pp is in ℝ≥0∞ with [Fact (1 ≤ p)]; the family is u : ℝ → α → E and its values at ε≤0\varepsilon\le0 are ignored. The limit is along 𝓝[>] 0, stated as Tendsto (fun ε => eLpNorm (u ε - g) p μ) (𝓝[>] 0) (𝓝 0); the Cauchy condition is eLpNorm (u ε - u η) p μ ≤ ENNReal.ofReal δ.

Preamble
import Mathlib.MeasureTheory.Function.LpSpace.Complete
import Mathlib.Topology.MetricSpace.Cauchy
Formal statement
namespace DbarRegularity

open MeasureTheory Filter Topology Set
open scoped ENNReal

/-- Completeness of `L^p` along `ε → 0⁺`: a family `u ε ∈ L^p` (`ε > 0`) which is Cauchy in
`L^p` as `ε → 0⁺` converges in `L^p` to some `g ∈ L^p`. -/
theorem exists_memLp_tendsto_eLpNorm_sub {α E : Type*} [MeasurableSpace α] {μ : Measure α}
    [NormedAddCommGroup E] [CompleteSpace E] {p : ℝ≥0∞} [Fact (1 ≤ p)] (u : ℝ → α → E)
    (hu : ∀ ε : ℝ, 0 < ε → MemLp (u ε) p μ)
    (hc : ∀ δ : ℝ, 0 < δ → ∃ η₀ : ℝ, 0 < η₀ ∧ ∀ ε η : ℝ, 0 < ε → ε < η₀ → 0 < η → η < η₀ →
      eLpNorm (u ε - u η) p μ ≤ ENNReal.ofReal δ) :
    ∃ g : α → E, MemLp g p μ ∧
      Tendsto (fun ε : ℝ => eLpNorm (u ε - g) p μ) (𝓝[>] 0) (𝓝 0) := by sorry

end DbarRegularity
Source
E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton Mathematical Series 30, Princeton University Press (1970), Chapter II, § 3.2, p. 35

View graph