dirac_prod — Mathlib

English

As a corollary, prod_dirac can be expressed via map with a pairing function.

Русский

Как следствие, prod_dirac выражается через отображение с пары.

LaTeX

$$$\\text{dirac_prod_dirac}$$$

Lean4

theorem dirac_prod (x : α) : (dirac x).prod ν = map (Prod.mk x) ν := by
  classical
  rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prodMk_left.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_left (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if, dirac_apply' _ hs, ←
    indicator_mul_left _ _ fun _ => sfiniteSeq ν i t, Pi.one_apply, one_mul]

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