English
For a Bochner integrable function f: α → P, the integral of its norm equals the real part of the lintegral of the ENNReal norm, i.e., ∫ ‖f‖ dμ = toReal( ∫⁻ ‖f‖ₑ dμ ).
Русский
Для интегрируемой по Бо́хнеру функции f: α → P выполняется ∫ ‖f‖ dμ = toReal( ∫⁻ ‖f‖ₑ dμ ).
LaTeX
$$$\\int a, \\|f(a)\\|\\,d\\mu = \\operatorname{toReal}\\left(\\int^- a, \\lVert f(a)\\rVert_e\\,d\\mu\\right)$$$
Lean4
theorem integral_eq_lintegral_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfm : AEStronglyMeasurable f μ) :
∫ a, f a ∂μ = ENNReal.toReal (∫⁻ a, ENNReal.ofReal (f a) ∂μ) :=
by
by_cases hfi : Integrable f μ
· rw [integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi]
have h_min : ∫⁻ a, ENNReal.ofReal (-f a) ∂μ = 0 :=
by
rw [lintegral_eq_zero_iff']
· refine hf.mono ?_
simp only [Pi.zero_apply]
intro a h
simp only [h, neg_nonpos, ofReal_eq_zero]
· exact measurable_ofReal.comp_aemeasurable hfm.aemeasurable.neg
rw [h_min, toReal_zero, _root_.sub_zero]
· rw [integral_undef hfi]
simp_rw [Integrable, hfm, hasFiniteIntegral_iff_norm, lt_top_iff_ne_top, Ne, true_and, Classical.not_not] at hfi
have : ∫⁻ a : α, ENNReal.ofReal (f a) ∂μ = ∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ :=
by
refine lintegral_congr_ae (hf.mono fun a h => ?_)
dsimp only
rw [Real.norm_eq_abs, abs_of_nonneg h]
rw [this, hfi, toReal_top]
