5.1. Simple Functions🔗

Definition.

Let X be a measurable space. A function f : X \to [0,\infty] is called simple if

for any a \in [0,\infty], the fiber f^{-1}\{a\} is measurable, and
the image \operatorname{Im}f is finite.

Lean code

/-- A simple function is an `ℝ≥0∞`-valued measurable function with finite range. -/
structure SimpleFunc (X : Type*) [MeasurableSpace X] where
  /-- The underlying function. -/
  toFun : X → ℝ≥0∞
  measurableSet_fiber' : ∀ x, MeasurableSet (toFun ⁻¹' {x})
  finite_range' : (Set.range toFun).Finite

Definition.

Let f : X \to [0,\infty] be a simple function, and let \mu be a measure on X. Its integral is defined by \Simp \int_{x \in X} f(x)\,d\mu \coloneqq \sum_{y \in \operatorname{Im} f} y \cdot \mu(f^{-1}\{y\}).

Lean code

/-- Integral of an `ℝ≥0∞`-valued simple function. -/
def lintegral (f : SimpleFunc X) (μ : Measure X) : ℝ≥0∞ :=
  ∑ x ∈ f.range, x * μ (f ⁻¹' {x})