3.1. 実数直線上の単関数
定義.
f : \mathbb{R} \to [0,\infty] とする。
f が 単関数 であるとは、次を満たすことをいう。
-
任意の
a \in [0,\infty]に対して、ファイバーf^{-1}\{a\}が可測である。 -
像
\operatorname{Im}fが有限である。
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
定義.
f : \mathbb{R} \to [0,\infty] を単関数とする。
その 積分 を
\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})