tprod_tprod — Mathlib

English

For a list l and family of sets s_i, the product measure over the tprod equals the product of μ_i(s_i).

Русский

Для списка l и множества s_i произведение мер по координатам равно произведению μ_i(s_i).

LaTeX

$$Measure.tprod l μ (Set.tprod l s) = (l.map (fun i => μ_i(s_i))).prod$$

Lean4

theorem tprod_tprod (l : List δ) (μ : ∀ i, Measure (X i)) [∀ i, SigmaFinite (μ i)] (s : ∀ i, Set (X i)) :
    Measure.tprod l μ (Set.tprod l s) = (l.map fun i => (μ i) (s i)).prod := by
  induction l with
  | nil => simp
  | cons a l ih =>
    rw [tprod_cons, Set.tprod]
    dsimp only [foldr_cons, map_cons, prod_cons]
    rw [prod_prod, ih]

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