bind_dirac_eq_map — Mathlib

English

For a measurable map f: α → β and a measure m on α, the Dirac-pushed image yields the pushforward: m.bind (x ↦ dirac (f x)) = m.map f.

Русский

Для измеримого отображения f: α → β и меры m на α имеем: m.bind (x ↦ dirac (f x)) = m.map f.

LaTeX

$$$m \\bind (x \\mapsto \\mathrm{dirac}(f(x))) = m \\map f$$$

Lean4

@[simp]
theorem bind_dirac_eq_map (m : Measure α) {f : α → β} (hf : Measurable f) :
    m.bind (fun x ↦ Measure.dirac (f x)) = m.map f :=
  by
  rw [← bind_dirac (m := m.map f), bind, bind, map_map, Function.comp_def]
  exacts [measurable_dirac, hf]

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