Category:Integral of Positive Measurable Function

From ProofWiki
Jump to navigation Jump to search

This category contains results about Integral of Positive Measurable Function.

Let $\struct {X, \Sigma, \mu}$ be a measure space.

We define the $\mu$-integral of positive measurable functions, denoted $\ds \int \cdot \rd \mu: \MM_{\overline \R}^+ \to \overline \R_{\ge 0}$, as:

$\forall f \in \MM_{\overline \R}^+: \ds \int f \rd \mu := \sup \set {\map {I_\mu} g: g \le f, g \in \EE^+}$


$\MM_{\overline \R}^+$ denotes the space of positive $\Sigma$-measurable functions
$\overline \R_{\ge 0}$ denotes the positive extended real numbers
$\sup$ is a supremum in the extended real ordering
$\map {I_\mu} g$ denotes the $\mu$-integral of the positive simple function $g$
$g \le f$ denotes pointwise inequality
$\EE^+$ denotes the space of positive simple functions