English
Let f: α → ℝ≥0 be nonnegative and μ-integrable. Then the nonnegative Lintegral of f equals ENNReal.ofReal applied to the ordinary integral of f: ∫⁻ f dμ = ENNReal.ofReal(∫ f dμ).
Русский
Пусть f: α → ℝ≥0 неотрицательная и интегрируема по μ. Тогда линтеграл f по μ равен ENNReal.ofReal(интеграл f по μ).
LaTeX
$$$\\\\int^\\\\ell a, f(a) \\, d\\\\mu \\\\;=\\\\; \\\\mathrm{ENNReal}.ofReal\\\\left(\\\\int a \\, f(a) \\, d\\\\mu\\\\right)$$$
Lean4
theorem lintegral_coe_eq_integral (f : α → ℝ≥0) (hfi : Integrable (fun x => (f x : ℝ)) μ) :
∫⁻ a, f a ∂μ = ENNReal.ofReal (∫ a, f a ∂μ) :=
by
simp_rw [integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun x => (f x).coe_nonneg) hfi.aestronglyMeasurable,
← ENNReal.coe_nnreal_eq]
rw [ENNReal.ofReal_toReal]
simpa [← lt_top_iff_ne_top, hasFiniteIntegral_iff_enorm, NNReal.enorm_eq] using hfi.hasFiniteIntegral
