English
Equality for eLpNorm in terms of ENNReal and real integrals: eLpNorm f p μ = ENNReal.ofReal((∫ ‖f‖^p)^(1/p)).
Русский
Эквивалентность eLpNorm через ENNReal и реальный интеграл: eLpNorm f p μ = ENNReal.ofReal((∫ ‖f‖^p)^(1/p)).
LaTeX
$$$\\\\|f\\\\|_{eLp} = \\\\mathrm{ENNReal}.ofReal\\\\left((\\\\int a \\, \|f(a)\\\\|^{p} \\, d\\\\mu)^{1/p}\\\\right)$$$
Lean4
theorem eLpNorm_eq_integral_rpow_norm {f : α → H} {p : ℝ≥0∞} (hp1 : p ≠ 0) (hp2 : p ≠ ∞) (hf : MemLp f p μ) :
eLpNorm f p μ = ENNReal.ofReal ((∫ a, ‖f a‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹) :=
by
have A : ∫⁻ a : α, ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ a : α, ‖f a‖ₑ ^ p.toReal ∂μ := by
simp_rw [← ofReal_rpow_of_nonneg (norm_nonneg _) toReal_nonneg, ofReal_norm_eq_enorm]
simp only [eLpNorm_eq_lintegral_rpow_enorm hp1 hp2, one_div]
rw [integral_eq_lintegral_of_nonneg_ae]; rotate_left
· exact ae_of_all _ fun x => by positivity
· exact (hf.aestronglyMeasurable.norm.aemeasurable.pow_const _).aestronglyMeasurable
rw [A, ← ofReal_rpow_of_nonneg toReal_nonneg (inv_nonneg.2 toReal_nonneg), ofReal_toReal]
exact (lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp1 hp2 hf.2).ne
