English
If μ.map X equals (μ.map X) ∘ Prod κ where κ is a finite kernel, then condDistrib Y X μ equals a.e. κ.
Русский
Если μ.map X равна (μ.map X) ∘ Prod κ, где κ — конечное ядро, тогда condDistrib Y X μ равно κ почти наверняка.
LaTeX
$$$$ (\\mathrm{condDistrib}(Y,X,μ) =_{a.e.} κ) \\iff μ.map (X) = μ.map X ⊗ κ $$$$
Lean4
/-- `condDistrib` is a.e. uniquely defined as the kernel satisfying the defining property of
`condKernel`. -/
theorem condDistrib_ae_eq_of_measure_eq_compProd (X : α → β) (hY : AEMeasurable Y μ) {κ : Kernel β Ω} [IsFiniteKernel κ]
(hκ : μ.map (fun x => (X x, Y x)) = μ.map X ⊗ₘ κ) : condDistrib Y X μ =ᵐ[μ.map X] κ :=
by
by_cases hX : AEMeasurable X μ
swap; · simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq]
suffices condDistrib (hY.mk Y) (hX.mk X) μ =ᵐ[μ.map (hX.mk X)] κ by
rwa [Measure.map_congr hX.ae_eq_mk, condDistrib_congr hY.ae_eq_mk hX.ae_eq_mk]
refine
condDistrib_ae_eq_of_measure_eq_compProd_of_measurable (μ := μ) hX.measurable_mk hY.measurable_mk
((Eq.trans ?_ hκ).trans ?_)
· refine Measure.map_congr ?_
filter_upwards [hX.ae_eq_mk, hY.ae_eq_mk] with a haX haY using by rw [haX, haY]
· rw [Measure.map_congr hX.ae_eq_mk]
