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
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}
Also known as
Lower unsigned basic integral
Child definitions
» D5103: Unsigned basic expectation
Results
» R1232: Tonelli's theorem for sums and integrals
» R1236: Markov's inequality
» R3515: Unsigned basic integral zero iff function almost everywhere zero
» R1233: Finite additivity of unsigned basic integral
» R4323:
» R1213: Linearity of unsigned basic integral
» R1242: Unsigned basic integral is compatible with measure
» R2089: Unsigned basic expectation is compatible with probability measure
» R2535: Chebyshov's inequality
» R4698: Unsigned basic integral with respect to a point measure
» R4746: Superadditivity and subadditivity of limit superior and limit inferior for unsigned basic integral
» R1204: Fatou's lemma for unsigned basic integral
» R1214: Isotonicity of unsigned basic integral
» R5300: Unsigned basic integral over an empty set equals zero