English
The integral of an indicator times a function equals the integral over the set of the function.
Русский
Интеграл от индикатора множества на функцию равен интегралу от функции по этому множеству.
LaTeX
$$$\\int \\! f \\,d\\mu = \\int_{x\\in S} f(x) \\,d\\mu$$$
Lean4
/-- For a function `f` and a measurable set `s`, the integral of `indicator s f`
over the whole space is equal to `∫ x in s, f x ∂μ` defined as `∫ x, f x ∂(μ.restrict s)`. -/
theorem integral_indicator (hs : MeasurableSet s) : ∫ x, indicator s f x ∂μ = ∫ x in s, f x ∂μ :=
by
by_cases hfi : IntegrableOn f s μ; swap
· rw [integral_undef hfi, integral_undef]
rwa [integrable_indicator_iff hs]
calc
∫ x, indicator s f x ∂μ = ∫ x in s, indicator s f x ∂μ + ∫ x in sᶜ, indicator s f x ∂μ :=
(integral_add_compl hs (hfi.integrable_indicator hs)).symm
_ = ∫ x in s, f x ∂μ + ∫ x in sᶜ, 0 ∂μ :=
(congr_arg₂ (· + ·) (integral_congr_ae (indicator_ae_eq_restrict hs))
(integral_congr_ae (indicator_ae_eq_restrict_compl hs)))
_ = ∫ x in s, f x ∂μ := by simp
