setIntegral_dirac' — Mathlib

English

For a strongly measurable f and any a, s, the integral over dirac a restricted to s equals f(a) if a∈s and 0 otherwise.

Русский

Для строгой измеримости f и множества s интеграл по Dirac a, ограниченный на s, равен f(a) если a∈s и 0 иначе.

LaTeX

$$$$\int x in s, f x \partial\mathrm{dirac}\, a = \mathrm{ite}(a\in s) (f(a)) (0).$$$$

Lean4

theorem setIntegral_dirac' {mα : MeasurableSpace α} {f : α → E} (hf : StronglyMeasurable f) (a : α) {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 integral_dirac' _ _ hf
  · exact integral_zero_measure _

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