prod_sum_right — Mathlib

English

A symmetric version: the product distributes over a sum of β-measures indexed by a countable set.

Русский

Симметричная версия: произведение распределяется по сумме мер β, индексационной счётностей.

LaTeX

$$ (Measure.sum m).prod (Measure.sum m') = Measure.sum (fun p => (m p.1).prod (m' p.2))$$

Lean4

theorem prod_sum_right {ι' : Type*} [Countable ι'] (m : Measure α) (m' : ι' → Measure β) [∀ n, SFinite (m' n)] :
    m.prod (Measure.sum m') = Measure.sum (fun p ↦ m.prod (m' p)) :=
  by
  ext s hs
  simp only [prod_apply hs, hs, sum_apply]
  have M : ∀ x, MeasurableSet (Prod.mk x ⁻¹' s) := fun x => measurable_prodMk_left hs
  simp_rw [Measure.sum_apply _ (M _)]
  rw [lintegral_tsum (fun i ↦ (measurable_measure_prodMk_left hs).aemeasurable)]

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