ThmDex – An index of mathematical definitions, results, and conjectures.
 ▼ Set of symbols ▼ Alphabet ▼ Deduction system ▼ Theory ▼ Zermelo-Fraenkel set theory ▼ Set ▼ Binary cartesian set product ▼ Binary relation ▼ Map ▼ Simple map ▼ Simple function ▼ Measurable simple complex function ▼ Simple integral
Definition D1747
Unsigned basic integral

Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that
 (i) $\text{MS} = \text{MS}(X \to [0, \infty])$ is the D2958: Set of measurable simple functions on $M$ (ii) $f : X \to [0, \infty]$ is a D313: Measurable function on $M$
The unsigned basic integral of $f$ with respect to $M$ is the D5237: Unsigned basic number $$\int_X f \, d \mu : = \sup_{\phi \in \text{MS} : 0 \leq \phi \leq f} \int_X \phi \, d \mu$$

Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that
 (i) $\text{MS} = \text{MS}(X \to [0, \infty])$ is the D2958: Set of measurable simple functions on $M$ (ii) $f : X \to [0, \infty]$ is a D313: Measurable function on $M$
The unsigned basic integral of $f$ with respect to $M$ is the D5237: Unsigned basic number $$\int_X f \, d \mu : = \sup \left\{ \int_X \phi \, d \mu \mid \phi \in \text{MS} \text{ such that } 0 \leq \phi \leq f \right\}$$
Children
 ▶ D5103: Unsigned basic expectation
Results
 ▶ R1233: Finite additivity of unsigned basic integral ▶ R1236: Markov's inequality ▶ R1232: Tonelli's theorem for sums and integrals ▶ R2089: Unsigned basic expectation is compatible with probability measure ▶ R5300: Unsigned basic integral over an empty set equals zero