English
For nonnegative simple functions f, the Bochner integral equals the real part of the lintegral of f considered as a real-valued function.
Русский
Для ненегативной простой функции f интеграл Бо́хнера равен действительной части линтеинтеграла от f как функции в ℝ.
LaTeX
$$$$ f_{\\\\text{integral}} μ = \\mathrm{toReal}\\left( \\int^- a \\, \\mathrm{ofReal}(f(a)) \\, dμ \\right) $$$$
Lean4
/-- `SimpleFunc.integral` and `SimpleFunc.lintegral` agree when the integrand has type
`α →ₛ ℝ≥0∞`. But since `ℝ≥0∞` is not a `NormedSpace`, we need some form of coercion. -/
theorem integral_eq_lintegral {f : α →ₛ ℝ} (hf : Integrable f μ) (h_pos : 0 ≤ᵐ[μ] f) :
f.integral μ = ENNReal.toReal (∫⁻ a, ENNReal.ofReal (f a) ∂μ) :=
by
have : f =ᵐ[μ] f.map (ENNReal.toReal ∘ ENNReal.ofReal) := h_pos.mono fun a h => (ENNReal.toReal_ofReal h).symm
rw [← integral_eq_lintegral' hf]
exacts [integral_congr hf this, ENNReal.ofReal_zero, fun b => ENNReal.ofReal_ne_top]
