3.1. Simple Functions on ℝ🔗

Definition.

Let f : \mathbb{R} \to [0,\infty]. We call f 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

/-- An `ℝ≥0∞`-valued simple function on `ℝ` with respect to the inductively defined measurable
sets. -/
structure SimpleFunc where
  /-- The underlying function. -/
  toFun : ℝ → ℝ≥0∞
  measurableSet_fiber' : ∀ x, MeasurableSet (toFun ⁻¹' {x})
  finite_range' : (Set.range toFun).Finite

Definition.

Let f : \mathbb{R} \to [0,\infty] be simple. Its integral is defined by \Simp \int_{x \in \mathbb{R}} f(x)\,dx \coloneqq \sum_{y \in \operatorname{Im} f} y \cdot m(f^{-1}\{y\}).

Lean code

/-- Integral of a simple function over `ℝ`. -/
def lintegral (f : SimpleFunc) : ℝ≥0∞ :=
  ∑ x ∈ f.range, x * measure (f ⁻¹' {x})