lintegral_countable — Mathlib

English

Let f be a function and s a countable subset. Then the lintegral of f over s equals the sum over a∈s of f(a)μ({a}).

Русский

Пусть f — произвольная функция, а s — счётное подмножество. Тогда линтеграл по s равен сумме по a∈s f(a)μ({a}).

LaTeX

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

Lean4

theorem lintegral_countable [MeasurableSingletonClass α] (f : α → ℝ≥0∞) {s : Set α} (hs : s.Countable) :
    ∫⁻ a in s, f a ∂μ = ∑' a : s, f a * μ {(a : α)} :=
  calc
    ∫⁻ a in s, f a ∂μ = ∫⁻ a in ⋃ x ∈ s, { x }, f a ∂μ := by rw [biUnion_of_singleton]
    _ = ∑' a : s, ∫⁻ x in {(a : α)}, f x ∂μ :=
      (lintegral_biUnion hs (fun _ _ => measurableSet_singleton _) (pairwiseDisjoint_fiber id s) _)
    _ = ∑' a : s, f a * μ {(a : α)} := by simp only [lintegral_singleton]

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