English
A general tendsto convergence result: from convergent eLpNorm to pointwise tendsto to a limit.
Русский
Общее условие перехода: сходящееся по eLpNorm ведет к точечному пределу.
LaTeX
$$$\text{cauchy_tendsto_of_tendsto}(f, h_cau, h_lim) \Rightarrow \text{tendsto } eLpNorm(f_n - f) \to 0$$$
Lean4
theorem cauchy_tendsto_of_tendsto {f : ℕ → α → E} (hf : ∀ n, AEStronglyMeasurable (f n) μ) (f_lim : α → E)
{B : ℕ → ℝ≥0∞} (hB : ∑' i, B i ≠ ∞) (h_cau : ∀ N n m : ℕ, N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N)
(h_lim : ∀ᵐ x : α ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))) :
atTop.Tendsto (fun n => eLpNorm (f n - f_lim) p μ) (𝓝 0) :=
by
rw [ENNReal.tendsto_atTop_zero]
intro ε hε
have h_B : ∃ N : ℕ, B N ≤ ε :=
by
suffices h_tendsto_zero : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → B n ≤ ε from
⟨h_tendsto_zero.choose, h_tendsto_zero.choose_spec _ le_rfl⟩
exact (ENNReal.tendsto_atTop_zero.mp (ENNReal.tendsto_atTop_zero_of_tsum_ne_top hB)) ε hε
obtain ⟨N, h_B⟩ := h_B
refine ⟨N, fun n hn => ?_⟩
have h_sub : eLpNorm (f n - f_lim) p μ ≤ atTop.liminf fun m => eLpNorm (f n - f m) p μ :=
by
refine eLpNorm_lim_le_liminf_eLpNorm (fun m => (hf n).sub (hf m)) (f n - f_lim) ?_
refine h_lim.mono fun x hx => ?_
simp_rw [sub_eq_add_neg]
exact Tendsto.add tendsto_const_nhds (Tendsto.neg hx)
refine h_sub.trans ?_
refine liminf_le_of_frequently_le' (frequently_atTop.mpr ?_)
refine fun N1 => ⟨max N N1, le_max_right _ _, ?_⟩
exact (h_cau N n (max N N1) hn (le_max_left _ _)).le.trans h_B
