English
Let p ≥ 1 and let (f_n) be a sequence of functions with each f_n ∈ Lp(μ; E). If the sequence is Cauchy with respect to the eLp-norm (i.e., for some summable bound B, the eLp-norm of f_n − f_m is eventually smaller than B_N for N ≤ n, m), then there exists a limit function f_lim ∈ Lp(μ; E) such that f_n converges to f_lim in the eLp-norm: eLpNorm(f_n − f_lim) → 0 as n → ∞. This proves that Lp(μ; E) is complete for 1 ≤ p.
Русский
Пусть p ≥ 1 и пусть (f_n) — последовательность функций; каждая f_n принадлежит Lp(μ; E). Если последовательность является голомາ в eLp-норме (существует B с ∑ B_i < ∞ так, что для всех N ≤ n, m выполняется eLpNorm(f_n − f_m) < B_N), тогда существует f_lim ∈ Lp(μ; E), такое что f_n сходится к f_lim по eLp-норме: eLpNorm(f_n − f_lim) → 0 при n → ∞.
LaTeX
$$$\\text{Let } p \\ge 1. \\text{ Suppose } f_n: \\mathbb{N} \\to \\alpha \\to E \\text{ with } f_n \\in \\mathrm{MemLp}(f_n,p,\\mu). \\text{ If there exists } B: \\mathbb{N} \\to \\mathbb{R}_{\\ge 0}^{\\infty} \\text{ with } \\sum_{i=0}^{\\infty} B_i \\neq \\infty \\text{ and } \\forall N,n,m: \\ N \\le n, N \\le m \\Rightarrow eLpNorm(f_n - f_m)_{p,\\mu} < B_N, \\ \\text{then } \\exists f_{\\lim}: \\alpha \\to E, \\ memLp(f_{\\lim},p,\\mu) \\wedge \\ \\text{atTop}.Tendsto\\Bigl(n \\mapsto eLpNorm(f_n - f_{\\lim})_{p,\\mu}\\Bigr)\\left(\\mathcal{N}_0\\right).$$$
Lean4
theorem cauchy_complete_eLpNorm [CompleteSpace E] (hp : 1 ≤ p) {f : ℕ → α → E} (hf : ∀ n, MemLp (f n) p μ)
{B : ℕ → ℝ≥0∞} (hB : ∑' i, B i ≠ ∞) (h_cau : ∀ N n m : ℕ, N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) :
∃ (f_lim : α → E), MemLp f_lim p μ ∧ atTop.Tendsto (fun n => eLpNorm (f n - f_lim) p μ) (𝓝 0) :=
by
obtain ⟨f_lim, h_f_lim_meas, h_lim⟩ :
∃ f_lim : α → E, StronglyMeasurable f_lim ∧ ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x)) :=
exists_stronglyMeasurable_limit_of_tendsto_ae (fun n => (hf n).1)
(ae_tendsto_of_cauchy_eLpNorm (fun n => (hf n).1) hp hB h_cau)
have h_tendsto' : atTop.Tendsto (fun n => eLpNorm (f n - f_lim) p μ) (𝓝 0) :=
cauchy_tendsto_of_tendsto (fun m => (hf m).1) f_lim hB h_cau h_lim
have h_ℒp_lim : MemLp f_lim p μ := memLp_of_cauchy_tendsto hp hf f_lim h_f_lim_meas.aestronglyMeasurable h_tendsto'
exact ⟨f_lim, h_ℒp_lim, h_tendsto'⟩
