lintegral_count — Mathlib

English

Let α be a type equipped with the counting measure. For any function f: α → ℝ≥0∞, the Lebesgue integral of f with respect to the counting measure equals the (possibly infinite) sum of the values f(a) over all a ∈ α.

Русский

Пусть α — множество с счетной мерой. Для любой функции f: α → ℝ≥0∞ интеграл Лебега по счетной мере равен (возможно бесконечной) сумме значений f(a) по всем a ∈ α.

LaTeX

$$$\int_{\alpha} f(x) \, d\mathrm{count} = \sum_{a \in \alpha} f(a)$$$

Lean4

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

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