English
The conditional distribution of Y given Y is the identity kernel a.e.
Русский
Условное распределение Y при условии Y равно ядру идентичности почти наверняка.
LaTeX
$$$$ \\mathrm{condDistrib}(Y,Y,μ) =_{a.e.} \\mathrm{Kernel.id}. $$$$
Lean4
theorem condDistrib_map {γ : Type*} {mγ : MeasurableSpace γ} {ν : Measure γ} [IsFiniteMeasure ν] {f : γ → α}
(hX : AEMeasurable X (ν.map f)) (hY : AEMeasurable Y (ν.map f)) (hf : AEMeasurable f ν) :
condDistrib Y X (ν.map f) =ᵐ[ν.map (X ∘ f)] condDistrib (Y ∘ f) (X ∘ f) ν :=
by
rw [← AEMeasurable.map_map_of_aemeasurable hX hf]
refine condDistrib_ae_eq_of_measure_eq_compProd (μ := ν.map f) X hY ?_
rw [AEMeasurable.map_map_of_aemeasurable hX hf, compProd_map_condDistrib (by fun_prop),
AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]
rfl
