instIsProbabilityMeasureForallInfinitePi

English

Mapping the infinite product after a measurable map f preserves product structure: infinitePi μ mapped by f equals infinitePi of the mapped measures.

Русский

Образ бесконечного произведения меры через измеримое отображение сохраняет произведение: infinitePi μ после отображения f равно infinitePi μ∘f.

LaTeX

$$$$\mathrm{infinitePi}_{i} \bigl(\cdot\bigr) \;\xrightarrow{\;f\;} \; \mathrm{infinitePi}_{i} (\mu_i \circ f_i).$$$$

Lean4

instance : IsProbabilityMeasure (infinitePi μ) := by
  constructor
  rw [← cylinder_univ ∅, cylinder, ← map_apply (measurable_restrict _) .univ, infinitePi_map_restrict, measure_univ]

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