integral_eq_sum — Mathlib

English

For a simple function f: α → E, integrable, the integral equals the finite sum over its range of real weights times the value in the range.

Русский

Для простой функции f: α → E, интегрируемой, интеграл равен конечной сумме по диапазону значений f.

LaTeX

$$$\\int f\,d\\mu = \\sum_{x\\in \\mathrm{range}(f)} \\mu( f^{-1}(\\{x\\}) ) \\cdot x$.$$

Lean4

theorem integral_eq_sum (f : α →ₛ E) (hfi : Integrable f μ) : ∫ x, f x ∂μ = ∑ x ∈ f.range, μ.real (f ⁻¹' { x }) • x :=
  by rw [← f.integral_eq_integral hfi, SimpleFunc.integral, ← SimpleFunc.integral_eq]; rfl

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