English
If f is almost everywhere measurable, then f and a measurable version of f have the same identDistrib with itself and itself.
Русский
Если функция почти всюду измерима, то она и её измеримая версия имеют одинаковое распределение по отношению к самой себе.
LaTeX
$$$\text{MeasureTheory.AEMeasurable.identDistrib_mk }(hf):\ IdentDistrib\ f\ (AEMeasurable.mk f hf)\ μ\ μ$$$
Lean4
protected theorem comp_of_aemeasurable {u : γ → δ} (h : IdentDistrib f g μ ν) (hu : AEMeasurable u (Measure.map f μ)) :
IdentDistrib (u ∘ f) (u ∘ g) μ ν :=
{ aemeasurable_fst := hu.comp_aemeasurable h.aemeasurable_fst
aemeasurable_snd := by rw [h.map_eq] at hu; exact hu.comp_aemeasurable h.aemeasurable_snd
map_eq :=
by
rw [← AEMeasurable.map_map_of_aemeasurable hu h.aemeasurable_fst, ←
AEMeasurable.map_map_of_aemeasurable _ h.aemeasurable_snd, h.map_eq]
rwa [← h.map_eq] }
