English
For a MeasurableEmbedding f, the pushforward measure satisfies μ.map f (s) = μ(f^{-1}(s)) for any set s.
Русский
Для измеримого вложения f верно μ.map f (s) = μ(f^{-1}(s)) для любого множества s.
LaTeX
$$$$\\forall f:\\alpha \\to \\beta,\\; \\mathrm{MeasurableEmbedding}(f) \\rightarrow \\forall \\mu:\\mathrm{Measure}\\,\\alpha,\\forall s:\\mathrm Set_{\\beta},\\; \\mu.map f\\,s = \\mu\\,(f^{-1}\\\\,s).$$$$
Lean4
nonrec theorem map_apply (hf : MeasurableEmbedding f) (μ : Measure α) (s : Set β) : μ.map f s = μ (f ⁻¹' s) :=
by
refine le_antisymm ?_ (le_map_apply hf.measurable.aemeasurable s)
set t := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
have htm : MeasurableSet t :=
(hf.measurableSet_image.2 <| measurableSet_toMeasurable _ _).union hf.measurableSet_range.compl
have hst : s ⊆ t := by
rw [subset_union_compl_iff_inter_subset, ← image_preimage_eq_inter_range]
exact image_mono (subset_toMeasurable _ _)
have hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s) := by
rw [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty, hf.injective.preimage_image]
calc
μ.map f s ≤ μ.map f t := by gcongr
_ = μ (f ⁻¹' s) := by rw [map_apply hf.measurable htm, hft, measure_toMeasurable]
