integral_dirac' — Mathlib

English

The Bochner integral of a strongly measurable function against a Dirac measure at a equals f(a).

Русский

Интеграл Боchnerа по мере Дирака в точке равен значению функции в этой точке: ∫ f dDirac a = f(a).

LaTeX

$$$$\int x, f(x) \partial\mathrm{Measure.dirac}\, a = f(a).$$$$

Lean4

@[simp]
theorem integral_dirac' [MeasurableSpace α] (f : α → E) (a : α) (hfm : StronglyMeasurable f) :
    ∫ x, f x ∂Measure.dirac a = f a := by
  borelize E
  calc
    ∫ x, f x ∂Measure.dirac a = ∫ _, f a ∂Measure.dirac a := integral_congr_ae <| ae_eq_dirac' hfm.measurable
    _ = f a := by simp

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