English
For a measurable set s, integrating a function over the subtype equals integrating over s with the original measure.
Русский
Для измеримого множества s интеграл по подтипу x∈s равен интегралу по s с исходной мерой.
LaTeX
$$$$\int x : s, f x \partial(Measure.comap Subtype.val \mu) = \int x \in s, f x \partial\mu.$$$$
Lean4
theorem _root_.MeasurableEmbedding.integral_map {β} {_ : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f)
(g : β → G) : ∫ y, g y ∂Measure.map f μ = ∫ x, g (f x) ∂μ :=
by
by_cases hgm : AEStronglyMeasurable g (Measure.map f μ)
· exact MeasureTheory.integral_map hf.measurable.aemeasurable hgm
· rw [integral_non_aestronglyMeasurable hgm, integral_non_aestronglyMeasurable]
exact fun hgf => hgm (hf.aestronglyMeasurable_map_iff.2 hgf)
