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