setLIntegral_dirac — Mathlib

English

For a fixed a, function f, a set s, with measurability and decidable membership, the integral over s of f with respect to dirac a equals f(a) if a∈s and 0 otherwise.

Русский

Для фиксированного a и функции f, по множеству s с условием измеримости и решаемости принадлежности, интеграл по dirac a равен f(a) если a∈s и 0 иначе.

LaTeX

$$$$\\int_{a\\in s} f(a) \\, d(\\mathrm{Dirac}_a) = \\begin{cases} f(a), & a\\in s \\\\ 0, & a\\notin s \\end{cases}.$$$$

Lean4

theorem setLIntegral_dirac {a : α} (f : α → ℝ≥0∞) (s : Set α) [MeasurableSingletonClass α] [Decidable (a ∈ s)] :
    ∫⁻ x in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0 :=
  by
  rw [restrict_dirac]
  split_ifs
  · exact lintegral_dirac _ _
  · exact lintegral_zero_measure _

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