English
If a sequence of Lp-functions is almost everywhere Cauchy in eLpNorm', then almost everywhere there exists a limit function in E.
Русский
Если последовательность функций Lp является ae-Cauchy в eLpNorm', то почти везде существует предел.
LaTeX
$$$\forall\; \text{ae.ae}, \exists l: E, \; f_n(x) \to l\;\text{a.e.}$$$
Lean4
theorem ae_tendsto_of_cauchy_eLpNorm' [CompleteSpace E] {f : ℕ → α → E} {p : ℝ} (hf : ∀ n, AEStronglyMeasurable (f n) μ)
(hp1 : 1 ≤ p) {B : ℕ → ℝ≥0∞} (hB : ∑' i, B i ≠ ∞)
(h_cau : ∀ N n m : ℕ, N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N) :
∀ᵐ x ∂μ, ∃ l : E, atTop.Tendsto (fun n => f n x) (𝓝 l) :=
by
have h_summable : ∀ᵐ x ∂μ, Summable fun i : ℕ => f (i + 1) x - f i x :=
by
have h1 : ∀ n, eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' i, B i :=
eLpNorm'_sum_norm_sub_le_tsum_of_cauchy_eLpNorm' hf hp1 h_cau
have h2 n : ∫⁻ a, (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' i, B i) ^ p :=
lintegral_rpow_sum_enorm_sub_le_rpow_tsum hp1 n (h1 n)
have h3 : (∫⁻ a, (∑' i, ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' i, B i :=
lintegral_rpow_tsum_coe_enorm_sub_le_tsum hf hp1 h2
have h4 : ∀ᵐ x ∂μ, ∑' i, ‖f (i + 1) x - f i x‖ₑ < ∞ := tsum_enorm_sub_ae_lt_top hf hp1 hB h3
exact h4.mono fun x hx => .of_nnnorm <| ENNReal.tsum_coe_ne_top_iff_summable.mp hx.ne
have h : ∀ᵐ x ∂μ, ∃ l : E, atTop.Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) (𝓝 l) :=
by
refine h_summable.mono fun x hx => ?_
let hx_sum := hx.hasSum.tendsto_sum_nat
exact ⟨∑' i, (f (i + 1) x - f i x), hx_sum⟩
refine h.mono fun x hx => ?_
obtain ⟨l, hx⟩ := hx
have h_rw_sum : (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) = fun n => f n x - f 0 x :=
by
ext1 n
change (∑ i ∈ Finset.range n, ((fun m => f m x) (i + 1) - (fun m => f m x) i)) = f n x - f 0 x
rw [Finset.sum_range_sub (fun m => f m x)]
rw [h_rw_sum] at hx
have hf_rw : (fun n => f n x) = fun n => f n x - f 0 x + f 0 x :=
by
ext1 n
abel
rw [hf_rw]
exact ⟨l + f 0 x, Tendsto.add_const _ hx⟩
