integral — Mathlib

English

The Bochner integral of simple real-valued functions is given by a finite sum over their range with weights μ.restrict f.

Русский

Бохнеров интеграл простых функций вещественного значения равен конечной сумме по их диапазону со взвешиванием μ.restrict.

LaTeX

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

Lean4

/-- Bochner integral of simple functions whose codomain is a real `NormedSpace`.
This is equal to `∑ x ∈ f.range, μ.real (f ⁻¹' {x}) • x` (see `integral_eq`). -/
def integral {_ : MeasurableSpace α} (μ : Measure α) (f : α →ₛ F) : F :=
  f.setToSimpleFunc (weightedSMul μ)

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