map_prod_map — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem map_prod_map {α' : Type*} [MeasurableSpace α'] {β' : Type*} [MeasurableSpace β'] {f : α → α'} {g : β → β'}
    (f_mble : Measurable f) (g_mble : Measurable g) :
    (μ.map f_mble.aemeasurable).prod (ν.map g_mble.aemeasurable) =
      (μ.prod ν).map (f_mble.prodMap g_mble).aemeasurable :=
  by
  apply Subtype.ext
  simp only [val_eq_to_measure, toMeasure_prod, toMeasure_map]
  rw [Measure.map_prod_map _ _ f_mble g_mble]

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