English
For a limiting function f_lim, eLpNorm' equals the liminf integral expression: eLpNorm' f_lim p μ = (∫⁻ a)^{1/p}.
Русский
Для предела функции f_lim нормa eLp' равна выражению по liminf интеграла.
LaTeX
$$$eLpNorm' f_{\lim} \; p \; \mu = \left(\int^\!\!_- a \; (\liminf)\right)^{1/p}$$$
Lean4
theorem eLpNorm'_lim_eq_lintegral_liminf {ι} [Nonempty ι] [LinearOrder ι] {f : ι → α → E} {p : ℝ} {f_lim : α → E}
(h_lim : ∀ᵐ x : α ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))) :
eLpNorm' f_lim p μ = (∫⁻ a, atTop.liminf (‖f · a‖ₑ ^ p) ∂μ) ^ (1 / p) :=
by
suffices h_no_pow : (∫⁻ a, ‖f_lim a‖ₑ ^ p ∂μ) = ∫⁻ a, atTop.liminf fun m => ‖f m a‖ₑ ^ p ∂μ by
rw [eLpNorm'_eq_lintegral_enorm, h_no_pow]
refine lintegral_congr_ae (h_lim.mono fun a ha => ?_)
dsimp only
rw [Tendsto.liminf_eq]
refine (ENNReal.continuous_rpow_const.tendsto ‖f_lim a‖₊).comp ?_
exact (continuous_enorm.tendsto (f_lim a)).comp ha
