setLIntegral_dirac' — Mathlib

English

For a fixed a, measurable f, measurable set s and decidable membership, the restricted Dirac integral over s equals f(a) if a∈s, else 0.

Русский

Для фиксированного a, измеримой функции f и измеримого множества s, интеграл Dirac по s равен 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∞} (hf : Measurable f) {s : Set α} (hs : MeasurableSet s)
    [Decidable (a ∈ s)] : ∫⁻ x in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0 :=
  by
  rw [restrict_dirac' hs]
  split_ifs
  · exact lintegral_dirac' _ hf
  · exact lintegral_zero_measure _

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