integral_finset — Mathlib

English

For a finite set s, the integral over s of f equals the finite sum of μ.real{ x } f(x) over x in s, provided integrability on s.

Русский

Для конечного множества s интеграл по s равен конечной сумме μ.real{ x } f(x) по x∈s.

LaTeX

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

Lean4

theorem integral_finset [MeasurableSingletonClass α] (s : Finset α) (f : α → E) (hf : IntegrableOn f s μ) :
    ∫ x in s, f x ∂μ = ∑ x ∈ s, μ.real { x } • f x := by
  rw [integral_countable _ s.countable_toSet hf, ← Finset.tsum_subtype']

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