map_dirac — Mathlib

English

If f is a measurable map, the pushforward of the Dirac measure δ_a by f is the Dirac measure at f(a).

Русский

Если f — измеримая отображение, то образящаяся по δ_a мера под действием f является мерой Дирака в точке f(a).

LaTeX

$$$ (dirac a).map f = dirac (f a) $$$

Lean4

theorem map_dirac {f : α → β} (hf : Measurable f) (a : α) : (dirac a).map f = dirac (f a) := by
  classical exact ext fun s hs => by simp [hs, map_apply hf hs, hf hs, indicator_apply]

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