English
The second-coordinate projection conditional distribution equals condDistrib on the second component with X projected and Y adjusted by the second coordinate; i.e., condDistrib (fun ω => Y ω.2) (fun ω => X ω.2) (ν.prod μ) = condDistrib Y X μ a.e.
Русский
Условное распределение по второй координате равно condDistrib со второй компонентой Y и X, по мере ν.prod μ.
LaTeX
$$$$ \\mathrm{condDistrib}(Y^{(2)},X^{(2)},ν.prod μ) =_{a.e.} \\mathrm{condDistrib}(Y,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_of_measurable (hX : Measurable X) (hY : Measurable Y) {κ : Kernel β Ω}
[IsFiniteKernel κ] (hκ : μ.map (fun x => (X x, Y x)) = μ.map X ⊗ₘ κ) : condDistrib Y X μ =ᵐ[μ.map X] κ :=
by
have heq : μ.map X = (μ.map (fun x ↦ (X x, Y x))).fst :=
by
ext s hs
rw [Measure.map_apply hX hs, Measure.fst_apply hs, Measure.map_apply]
exacts [rfl, Measurable.prod hX hY, measurable_fst hs]
rw [heq, condDistrib]
symm
refine eq_condKernel_of_measure_eq_compProd _ ?_
convert hκ
exact heq.symm
