integral_fintype — Mathlib

English

If α is finite, then the integral of f over α equals the finite sum over all elements of α of μ.real{a} f(a).

Русский

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

LaTeX

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

Lean4

theorem integral_fintype [MeasurableSingletonClass α] [Fintype α] (f : α → E) (hf : Integrable f μ) :
    ∫ x, f x ∂μ = ∑ x, μ.real { x } • f x := by
  -- NB: Integrable f does not follow from Fintype, because the measure itself could be non-finite

  rw [← integral_finset .univ, Finset.coe_univ, Measure.restrict_univ]
  simp [Finset.coe_univ, hf]

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