English
Alternative expression for condDistrib_snd_prod using fst map and prod structure.
Русский
Альтернативное выражение condDistrib_snd_prod через fst-map и prod-структуру.
LaTeX
$$$$ \\mathrm{condDistrib}_{\\mathrm{snd}}(Y,X,μ) =_{a.e.} \\mathrm{condDistrib}(Y,X,μ) \\text{ по соответствующей проекции }. $$$$
Lean4
theorem condDistrib_fst_prod {γ : Type*} {mγ : MeasurableSpace γ} (X : α → β) (hY : AEMeasurable Y μ) (ν : Measure γ)
[IsProbabilityMeasure ν] : condDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.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.fst (α := α) (β := γ)) (ν := μ.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_fst_prod, measure_univ, one_smul] at h_map
exact h_map.symm
