norm_toL1_eq_lintegral_norm — Mathlib

English

For an integrable f with μ, the L1-norm of its L1-image equals the real part of the EN-real of the integral of the norm of f, i.e., the real EN-norm of toL1 equals the real part of the lintegral of the ENReal of ‖f‖.

Русский

Для интегрируемой функции f по μ нормa L1 образа равна вещественной части линтеграла от ENReal-образы ‖f‖; то есть ‖toL1 f‖ = ENNReal.toReal(∫ ENNReal.ofReal‖f‖ dμ).

LaTeX

$$$ \\| \\mathrm{toL1}(f) \\| = \\mathrm{ENNReal.toReal}\\left( \\int^- a \\; \\mathrm{ENNReal.ofReal}\\big( \\|f(a)\\| \\big) \\, d\\mu \\right) $$$

Lean4

theorem norm_toL1_eq_lintegral_norm (f : α → β) (hf : Integrable f μ) :
    ‖hf.toL1 f‖ = ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) := by rw [norm_toL1, lintegral_norm_eq_lintegral_edist]

Похожие утверждения