English
If μ ≤ ν and f is almost everywhere measurable with respect to ν, then μ.map f ≤ ν.map f.
Русский
Если μ ≤ ν и f а.е.-измерима относительно ν, то μ.map f ≤ ν.map f.
LaTeX
$$$\mu \le ν \;\rightarrow\; AEMeasurable f \nu \rightarrow (\mu.map f) \le (\nu.map f)$$$
Lean4
theorem restrict_map_of_aemeasurable {f : α → δ} (hf : AEMeasurable f μ) {s : Set δ} (hs : MeasurableSet s) :
(μ.map f).restrict s = (μ.restrict <| f ⁻¹' s).map f :=
calc
(μ.map f).restrict s = (μ.map (hf.mk f)).restrict s :=
by
congr 1
apply Measure.map_congr hf.ae_eq_mk
_ = (μ.restrict <| hf.mk f ⁻¹' s).map (hf.mk f) := (Measure.restrict_map hf.measurable_mk hs)
_ = (μ.restrict <| hf.mk f ⁻¹' s).map f := (Measure.map_congr (ae_restrict_of_ae hf.ae_eq_mk.symm))
_ = (μ.restrict <| f ⁻¹' s).map f := by
apply congr_arg
ext1 t ht
simp only [ht, Measure.restrict_apply]
apply measure_congr
apply (EventuallyEq.refl _ _).inter (hf.ae_eq_mk.symm.preimage s)
