English
A version of ae_tendsto for eLpNorm with standard hypotheses; almost everywhere convergence of f_n to a limit function occurs.
Русский
Версия ae_tendsto для eLpNorm с обычными условиями; почти везде сходится к пределу.
LaTeX
$$$\forall\; f_n,\;\text{ae } f_n \Rightarrow \text{exists } f: f_n \to f\; \text{ae}.$$$
Lean4
theorem ae_tendsto_of_cauchy_eLpNorm [CompleteSpace E] {f : ℕ → α → E} (hf : ∀ n, AEStronglyMeasurable (f n) μ)
(hp : 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
by_cases hp_top : p = ∞
· simp_rw [hp_top] at *
have h_cau_ae : ∀ᵐ x ∂μ, ∀ N n m, N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N :=
by
simp_rw [ae_all_iff]
exact fun N n m hnN hmN => ae_lt_of_essSup_lt (h_cau N n m hnN hmN)
simp_rw [eLpNorm_exponent_top, eLpNormEssSup] at h_cau
refine h_cau_ae.mono fun x hx => cauchySeq_tendsto_of_complete ?_
refine cauchySeq_of_le_tendsto_0 (fun n => (B n).toReal) ?_ ?_
· intro n m N hnN hmN
specialize hx N n m hnN hmN
rw [_root_.dist_eq_norm, ← ENNReal.ofReal_le_iff_le_toReal (ENNReal.ne_top_of_tsum_ne_top hB N),
ofReal_norm_eq_enorm]
exact hx.le
· rw [← ENNReal.toReal_zero]
exact
Tendsto.comp (g := ENNReal.toReal) (ENNReal.tendsto_toReal ENNReal.zero_ne_top)
(ENNReal.tendsto_atTop_zero_of_tsum_ne_top hB)
have hp1 : 1 ≤ p.toReal :=
by
rw [← ENNReal.ofReal_le_iff_le_toReal hp_top, ENNReal.ofReal_one]
exact hp
have h_cau' : ∀ N n m : ℕ, N ≤ n → N ≤ m → eLpNorm' (f n - f m) p.toReal μ < B N :=
by
intro N n m hn hm
specialize h_cau N n m hn hm
rwa [eLpNorm_eq_eLpNorm' (zero_lt_one.trans_le hp).ne.symm hp_top] at h_cau
exact ae_tendsto_of_cauchy_eLpNorm' hf hp1 hB h_cau'
