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
Formulation 0
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 \begin{equation} \int_X f \, d \mu : = \sup_{\phi \in \text{MS} : 0 \leq \phi \leq f} \int_X \phi \, d \mu \end{equation}
Formulation 1
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 \begin{equation} \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\} \end{equation}
Children
Unsigned basic expectation
Results
Finite additivity of unsigned basic integral
Markov's inequality
Tonelli's theorem for sums and integrals
Unsigned basic expectation is compatible with probability measure
Unsigned basic integral over an empty set equals zero