map_snd_prod — Mathlib

English

The first marginal of the product measure equals the second univ mass times the first measure: (μ.prod ν).map Prod.fst = ν univ • μ.

Русский

Первая маргинальная мера произведения равна ν(univ) помноженному на μ: (μ.prod ν).map Prod.fst = ν univ • μ.

LaTeX

$$$ (\mu \mathrm{prod} \nu) \mathrm{map} \mathrm{Prod.fst} = \nu(\mathrm{univ}) \; \mu $$$

Lean4

/-- The second marginal of a product probability measure is the second probability measure. -/
@[simp]
theorem map_snd_prod : (μ.prod ν).map measurable_snd.aemeasurable = ν :=
  by
  apply Subtype.ext
  simp only [val_eq_to_measure, toMeasure_map, toMeasure_prod, Measure.map_snd_prod, measure_univ, one_smul]

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