English
When restricting a simple function to a measurable set s, the lintegral equals the sum over its range of r times μ(f^{-1}({r}) ∩ s).
Русский
При ограничении простой функции f на измеримое множество s линеграль равен сумме по значениям: ∑_{r∈range(f)} r · μ(f^{-1}({r}) ∩ s).
LaTeX
$$$(\\restrict f s).lintegral μ = ∑_{r \\in f.range} r \\cdot μ\\big(f^{-1} \\{r\\} \\cap s\\big)$$$
Lean4
theorem restrict_lintegral (f : α →ₛ ℝ≥0∞) {s : Set α} (hs : MeasurableSet s) :
(restrict f s).lintegral μ = ∑ r ∈ f.range, r * μ (f ⁻¹' { r } ∩ s) :=
calc
(restrict f s).lintegral μ = ∑ r ∈ f.range, r * μ (restrict f s ⁻¹' { r }) :=
lintegral_eq_of_subset _ fun x hx =>
if hxs : x ∈ s then fun _ => by simp only [f.restrict_apply hs, indicator_of_mem hxs, mem_range_self]
else False.elim <| hx <| by simp [*]
_ = ∑ r ∈ f.range, r * μ (f ⁻¹' { r } ∩ s) :=
Finset.sum_congr rfl <|
forall_mem_range.2 fun b =>
if hb : f b = 0 then by simp only [hb, zero_mul] else by rw [restrict_preimage_singleton _ hs hb, inter_comm]
