condDistrib_comp_map — Mathlib

English

The conditional distribution composed with the pushforward by X equals the pushforward by Y; more precisely condDistrib Y X μ ∘_m (μ.map X) = μ.map Y.

Русский

Условное распределение, композиция с отображением X, равно распределению Y; точнее condDistrib Y X μ ∘_m (μ.map X) = μ.map Y.

LaTeX

$$$$\\mathrm{condDistrib}(Y,X,μ) \\circ_{m} (μ.map X) = μ.map Y.$$$$

Lean4

theorem condDistrib_comp_map (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) :
    condDistrib Y X μ ∘ₘ (μ.map X) = μ.map Y := by
  rw [← Measure.snd_compProd, compProd_map_condDistrib hY, Measure.snd_map_prodMk₀ hX]

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