prod_swap

Mathlib.MeasureTheory.Measure.FiniteMeasureProd

URI: https://scilib.ai/kg/mathlib#MeasureTheory.ProbabilityMeasure.prod_swap

English

If f and g are measurable, then (μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g).

Русский

Если f и g измеримы, то (μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g).

LaTeX

$$$ (\mu.map f) \mathrm{prod} (\nu.map g) = (\mu \mathrm{prod} \nu).\mathrm{map} (\mathrm{Prod.map} f g) $$$

Lean4

theorem prod_swap : (μ.prod ν).map measurable_swap.aemeasurable = ν.prod μ :=
  by
  apply Subtype.ext
  simp [Measure.prod_swap]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru