English
Same as condDistrib_snd_prod but with Y as second component; a.e. equality with snd projection.
Русский
То же самое, что и condDistrib_snd_prod, но с Y как второй компонентой; эквивалентность почти наверняка по второй координате.
LaTeX
$$$$ \\mathrm{condDistrib}(\\mathrm{snd}(Y), \\mathrm{snd}(X), (ν.prod μ)) =_{a.e.} \\mathrm{condDistrib}(Y,X,μ). $$$$
Lean4
theorem condDistrib_snd_prod {γ : Type*} {mγ : MeasurableSpace γ} (X : α → β) (hY : AEMeasurable Y μ) (ν : Measure γ)
[IsProbabilityMeasure ν] : condDistrib (fun ω ↦ Y ω.2) (fun ω ↦ X ω.2) (ν.prod μ) =ᵐ[μ.map X] condDistrib Y X μ :=
by
by_cases hX : AEMeasurable X μ
swap; · simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq]
have : μ = (μ.prod ν).map (fun ω ↦ ω.1) := by simp [Measure.map_fst_prod]
have h_map :=
condDistrib_map (X := X) (Y := Y) (f := Prod.snd (β := α) (α := γ)) (ν := ν.prod μ) (mα := inferInstance) (mβ :=
inferInstance) (by simpa) (by simpa) (by fun_prop)
rw [← AEMeasurable.map_map_of_aemeasurable (by simpa) (by fun_prop)] at h_map
simp only [Measure.map_snd_prod, measure_univ, one_smul] at h_map
exact h_map.symm
