English
Let f be a simple function, and g: E → ℝ≥0∞ with g(0)=0 and g(b) ≠ ∞ for all b. Then the Bochner integral of f mapped by ENNReal.toReal∘g equals the real part of the lintegral of g∘f.
Русский
Пусть f — простая функция, g: E → ℝ≥0∞ удовлетворяет g(0)=0 и g(b)≠∞. Тогда интеграл Бо́хнера от f, применённого к g, равен действительной части линтеинтеграла от g∘f.
LaTeX
$$$$ (f.map (\\\\mathrm{ENNReal.toReal} \\, \\circ \\, g))_{\\\\text{integral}} = \\mathrm{toReal}\\left( \\int^- a \\, g(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.
See `integral_eq_lintegral` for a simpler version. -/
theorem integral_eq_lintegral' {f : α →ₛ E} {g : E → ℝ≥0∞} (hf : Integrable f μ) (hg0 : g 0 = 0) (ht : ∀ b, g b ≠ ∞) :
(f.map (ENNReal.toReal ∘ g)).integral μ = ENNReal.toReal (∫⁻ a, g (f a) ∂μ) :=
by
have hf' : f.FinMeasSupp μ := integrable_iff_finMeasSupp.1 hf
simp only [← map_apply g f, lintegral_eq_lintegral]
rw [map_integral f _ hf, map_lintegral, ENNReal.toReal_sum]
· refine Finset.sum_congr rfl fun b _ => ?_
rw [smul_eq_mul, toReal_mul, mul_comm, Function.comp_apply, measureReal_def]
· rintro a -
by_cases a0 : a = 0
· rw [a0, hg0, zero_mul]; exact WithTop.zero_ne_top
· apply mul_ne_top (ht a) (hf'.meas_preimage_singleton_ne_zero a0).ne
· simp [hg0]
