lintegral_count' — Mathlib

English

For a measurable f, the lintegral with respect to the counting measure equals the sum over the index set of f.

Русский

Для измеримой функции f линегральный интеграл по счетной мере равен сумме f по каждому индексу.

LaTeX

$$$$\\int f \\, d\\text{count} = \\sum_{a} f(a).$$$$

Lean4

theorem lintegral_count' {f : α → ℝ≥0∞} (hf : Measurable f) : ∫⁻ a, f a ∂count = ∑' a, f a :=
  by
  rw [count, lintegral_sum_measure]
  congr
  exact funext fun a => lintegral_dirac' a hf

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