English
If f and g are integrable on a measurable set s and its complement, the integral of the piecewise function on the whole space equals the sum of the integrals on s and on its complement.
Русский
Если f интегрируемо на s и g интегрируемо на s^c, то интеграл по всёму пространству от функции piecewise f g равен сумме интегралов по s и по s^c.
LaTeX
$$$$ \int f \;\text{pcw} \;g \, d\mu = \int_{x \in s} f(x) \, d\mu + \int_{x \in s^c} g(x) \, d\mu $$$$
Lean4
theorem integral_piecewise [DecidablePred (· ∈ s)] (hs : MeasurableSet s) (hf : IntegrableOn f s μ)
(hg : IntegrableOn g sᶜ μ) : ∫ x, s.piecewise f g x ∂μ = ∫ x in s, f x ∂μ + ∫ x in sᶜ, g x ∂μ := by
rw [← Set.indicator_add_compl_eq_piecewise,
integral_add' (hf.integrable_indicator hs) (hg.integrable_indicator hs.compl), integral_indicator hs,
integral_indicator hs.compl]
