English
For a measurable set s and functions f,g, with decidable membership, the integral of the piecewise function equals the sum of the integrals of f on s and g on s^c.
Русский
Для измеримого множества s и функций f,g, с разрешённым членством, интеграл по функции piecewise равен сумме интегралов по f на s и по g на s^c.
LaTeX
$$$$\\int_{\\alpha} s\\text{.piecewise} f g \\; d\\mu = \\int_{a\\in s} f(a) \\, d\\mu + \\int_{a\\in s^{c}} g(a) \\, d\\mu.$$$$
Lean4
theorem lintegral_piecewise (hs : MeasurableSet s) (f g : α → ℝ≥0∞) [∀ j, Decidable (j ∈ s)] :
∫⁻ a, s.piecewise f g a ∂μ = ∫⁻ a in s, f a ∂μ + ∫⁻ a in sᶜ, g a ∂μ :=
by
rw [← lintegral_add_compl _ hs]
congr 1
· exact setLIntegral_congr_fun hs <| fun _ ↦ Set.piecewise_eq_of_mem _ _ _
· exact setLIntegral_congr_fun hs.compl <| fun _ ↦ Set.piecewise_eq_of_notMem _ _ _
