setIntegral_dirac — Mathlib

English

Same as setDirac restriction: the integral over a restricted to a yields either f(a) or 0 depending on membership.

Русский

То же самое, что и ограниченный интеграл по Dirac: интеграл по a в s равен либо f(a), либо 0, в зависимости от принадлежности.

LaTeX

$$$$\int x in s, f x \partial(\mathrm{dirac} a) = (\text{if } a\in s\text{ then } f a\text{ else }0).$$$$

Lean4

theorem setIntegral_dirac [MeasurableSpace α] [MeasurableSingletonClass α] (f : α → E) (a : α) (s : Set α)
    [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 integral_dirac _ _
  · exact integral_zero_measure _

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