integral_countable' — Mathlib

English

If α is countable and f: α → E is integrable, then the Bochner integral over α equals the sum of point masses μ.real{a} times f(a) over all a.

Русский

Пусть α счётно, функция f: α → E интегрируема; then интеграл Бо́хнер по α равен сумме по всем a из α массы μ.real{a} на f(a).

LaTeX

$$$\\displaystyle \\int_{\\alpha} f(a) \\, d\\mu = \\sum_{a \\in \\alpha} \\mu_{\\mathbb{R}}(\\{a\\}) \\cdot f(a)$$$

Lean4

theorem integral_countable' [Countable α] [MeasurableSingletonClass α] {μ : Measure α} {f : α → E}
    (hf : Integrable f μ) : ∫ a, f a ∂μ = ∑' a, μ.real { a } • f a :=
  by
  rw [← Measure.sum_smul_dirac μ] at hf
  rw [← Measure.sum_smul_dirac μ, integral_sum_measure hf]
  congr 1 with a : 1
  rw [integral_smul_measure, integral_dirac, Measure.sum_smul_dirac, measureReal_def]

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