lintegral_insert — Mathlib

English

If a ∉ s, then the lintegral over insert a s equals the sum of the singleton contribution for a plus the lintegral over s.

Русский

Если a не принадлежит s, то интеграл по insert a s равен сумме вклада элемента a и линтеграла по s.

LaTeX

$$$\int_{\mathrm{insert}\,a\,s} f(x) \, d\mu = f(a) \mu\{a\} + \int_{s} f(x) \, d\mu$$$

Lean4

theorem lintegral_insert [MeasurableSingletonClass α] {a : α} {s : Set α} (h : a ∉ s) (f : α → ℝ≥0∞) :
    ∫⁻ x in insert a s, f x ∂μ = f a * μ { a } + ∫⁻ x in s, f x ∂μ :=
  by
  rw [← union_singleton, lintegral_union (measurableSet_singleton a), lintegral_singleton, add_comm]
  rwa [disjoint_singleton_right]

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