English
Given hf: AEStronglyMeasurable f μ, the pair f and (hf.mk f) are identDistrib with μ and μ.
Русский
Пусть hf: AEStronglyMeasurable f μ, тогда пара f и (hf.mk f) идентично распределена относительно μ и μ.
LaTeX
$$$hf : AEStronglyMeasurable f μ \Rightarrow IdentDistrib f (hf.mk f) μ μ$$$
Lean4
theorem ae_snd (h : IdentDistrib f g μ ν) {p : γ → Prop} (pmeas : MeasurableSet {x | p x}) (hp : ∀ᵐ x ∂μ, p (f x)) :
∀ᵐ x ∂ν, p (g x) := by
apply (ae_map_iff h.aemeasurable_snd pmeas).1
rw [← h.map_eq]
exact (ae_map_iff h.aemeasurable_fst pmeas).2 hp