lintegral_countable' — Mathlib

English

If α is countable, then for any measure μ and function f: α → ℝ≥0∞, the lintegral over α equals the sum over α of f(a) times μ({a}).

Русский

Если α счётно, то интеграл Лебега по α равен сумме по a∈α функции f(a) умноженной на μ({a}).

LaTeX

$$$\int_{\alpha} f(a) \, d\mu = \sum_{a \in \alpha} f(a) \mu\{a\}$$$

Lean4

theorem lintegral_countable' [Countable α] [MeasurableSingletonClass α] (f : α → ℝ≥0∞) :
    ∫⁻ a, f a ∂μ = ∑' a, f a * μ { a } :=
  by
  conv_lhs => rw [← sum_smul_dirac μ, lintegral_sum_measure]
  congr 1 with a : 1
  simp [mul_comm]

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