English
The limit inferior of Lp-norms controls the norm of the limit in Lp.
Русский
Границы лимина в Lp управляют нормой предела в Lp.
LaTeX
$$$eLpNorm( f_{lim}) \le \liminf_{n} eLpNorm(f_n)$$$
Lean4
theorem eLpNorm_lim_le_liminf_eLpNorm {f : ℕ → α → E} (hf : ∀ n, AEStronglyMeasurable (f n) μ) (f_lim : α → E)
(h_lim : ∀ᵐ x : α ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))) :
eLpNorm f_lim p μ ≤ atTop.liminf fun n => eLpNorm (f n) p μ :=
by
obtain rfl | hp0 := eq_or_ne p 0
· simp
by_cases hp_top : p = ∞
· simp_rw [hp_top]
exact eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top h_lim
simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
exact eLpNorm'_lim_le_liminf_eLpNorm' hp_pos hf h_lim