compProd_map_condDistrib — Mathlib

English

The joint distribution μ.map X ⊗ condDistrib Y X μ equals μ.map (a ↦ (X a, Y a)).

Русский

Смешанная (совместная) распределение μ.map X ⊗ condDistrib Y X μ равно μ.map (a ↦ (X a, Y a)).

LaTeX

$$$$ (\\mu\\text{.map } X) \\otimes \\mathrm{condDistrib}(Y,X,μ) = μ.map( a \\mapsto (X(a), Y(a)) ). $$$$

Lean4

theorem compProd_map_condDistrib (hY : AEMeasurable Y μ) : (μ.map X) ⊗ₘ condDistrib Y X μ = μ.map fun a ↦ (X a, Y a) :=
  by rw [condDistrib, ← Measure.fst_map_prodMk₀ hY, Measure.disintegrate]

Похожие утверждения