English
When p = ∞, eLpNorm_exponent_top_lim_eq_essSup_liminf gives eLpNorm top as essSup of liminf of norms.
Русский
При p = ∞ eLpNorm_exponent_top_lim_eq_essSup_liminf выражает норму как essSup liminf норм.
LaTeX
$$$eLpNorm_{\infty}(f_{lim}) = \operatorname{essSup}_{x} \;\big(\liminf_{n} \|f_n(x)\|\big)$$$
Lean4
theorem eLpNorm'_lim_le_liminf_eLpNorm' {f : ℕ → α → E} {p : ℝ} (hp_pos : 0 < p)
(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
rw [eLpNorm'_lim_eq_lintegral_liminf h_lim]
rw [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv]
refine (lintegral_liminf_le' fun m => (hf m).enorm.pow_const _).trans_eq ?_
have h_pow_liminf : atTop.liminf (fun n ↦ eLpNorm' (f n) p μ) ^ p = atTop.liminf fun n ↦ eLpNorm' (f n) p μ ^ p :=
by
have h_rpow_mono := ENNReal.strictMono_rpow_of_pos hp_pos
have h_rpow_surj := (ENNReal.rpow_left_bijective hp_pos.ne.symm).2
refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
all_goals isBoundedDefault
rw [h_pow_liminf]
simp_rw [eLpNorm'_eq_lintegral_enorm, ← ENNReal.rpow_mul, one_div, inv_mul_cancel₀ hp_pos.ne.symm, ENNReal.rpow_one]
