English
If f: α → ℝ is integrable and f ≥ 0 almost everywhere, then ENNReal.ofReal(∫ f dμ) equals the Lintegral of ENNReal.ofReal(f): ENNReal.ofReal(∫ f dμ) = ∫⁻ ENNReal.ofReal(f) dμ.
Русский
Пусть f: α → ℝ интегрируема и она неотрицательна почти всюду. Тогда ENNReal.ofReal(интеграл f) равен линтегралу ENNReal.ofReal(f).
LaTeX
$$$\\\\mathrm{ENNReal}.ofReal\\\\left(\\\\int a \\, f(a) \\, d\\\\mu\\\\right) \\\\;=\\\\; \\\\int^\\\\ell a \\, \\\\mathrm{ENNReal}.ofReal\\\\left(f(a)\\\\right) \\, d\\\\mu$$$
Lean4
theorem ofReal_integral_eq_lintegral_ofReal {f : α → ℝ} (hfi : Integrable f μ) (f_nn : 0 ≤ᵐ[μ] f) :
ENNReal.ofReal (∫ x, f x ∂μ) = ∫⁻ x, ENNReal.ofReal (f x) ∂μ :=
by
have : f =ᵐ[μ] (‖f ·‖) := f_nn.mono fun _x hx ↦ (abs_of_nonneg hx).symm
simp_rw [integral_congr_ae this, ofReal_integral_norm_eq_lintegral_enorm hfi, ← ofReal_norm_eq_enorm]
exact lintegral_congr_ae (this.symm.fun_comp ENNReal.ofReal)
