English
If f is integrable and g is a function with g(0)=0, then the integral of f mapped by g equals the weighted sum of g(x) over x in the range of f, with weights given by μ.real(preimage of x).
Русский
Если f интегрируема и g(0)=0, то интеграл f, приведённый через g, равен сумме по значениям x из диапазона f: μ.real(f^{-1}({x}))·g(x).
LaTeX
$$$$ (f.map \\\\; g)_{\\text{integral}} = \\sum_{x \\in \\mathrm{range}(f)} μ_{\\mathbb{R}}\\bigl(f^{-1}(\\{x\\})\\bigr) \\cdot g(x) $$$$
Lean4
/-- Calculate the integral of `g ∘ f : α →ₛ F`, where `f` is an integrable function from `α` to `E`
and `g` is a function from `E` to `F`. We require `g 0 = 0` so that `g ∘ f` is integrable. -/
theorem map_integral (f : α →ₛ E) (g : E → F) (hf : Integrable f μ) (hg : g 0 = 0) :
(f.map g).integral μ = ∑ x ∈ f.range, (μ.real (f ⁻¹' { x })) • g x :=
map_setToSimpleFunc _ weightedSMul_union hf hg
