ThmDex – An index of mathematical definitions, results, and conjectures.
Distribution formula for unsigned basic integral
Formulation 2
Let $M = (X, \mathcal{F}, \mu)$ be a D2707: Sigma-bounded measure space such that
(i) $f : X \to [0, \infty]$ is an D5610: Unsigned basic Borel function on $M$
Then \begin{equation} \int_X f \, d \mu = \int_{[0, \infty]} \mu(f \geq t) \, d t \end{equation}
Formulation 2
Let $M = (X, \mathcal{F}, \mu)$ be a D2707: Sigma-bounded measure space such that
(i) $f : X \to [0, \infty]$ is an D5610: Unsigned basic Borel function on $M$
Then \begin{equation} \int_X f \, d \mu = \int_{[0, \infty]} \mu(\{ x \in X : f(x) \geq t \}) \, d t \end{equation}
Proofs
Proof 0
Let $M = (X, \mathcal{F}, \mu)$ be a D2707: Sigma-bounded measure space such that
(i) $f : X \to [0, \infty]$ is an D5610: Unsigned basic Borel function on $M$
Introduce the D3808: Function positive hypograph for $f$ as \begin{equation} \Gamma : = \{ (x, t) \in X \times \mathbb{R} : 0 \leq t \leq f(x) \} \end{equation} and let $\Gamma_t = \{ x \in X : (x, t) \in \Gamma \}$ denote a corresponding slice set at each $t \in \mathbb{R}$. We have the chain of equivalencies \begin{equation} \begin{split} (x, t) \in \Gamma \quad & \iff \quad 0 \leq t \leq f(x) \\ & \iff \quad x \in \{ f \geq t \} \\ \end{split} \end{equation} Thus we have the equality \begin{equation} \begin{split} \Gamma_t & = \{ x \in X : (x, t) \in \Gamma \} \\ & = \{ x \in X : f(x) \geq t \} \\ & = \{ f \geq t \} \end{split} \end{equation} Let $\upsilon$ now denote the Lebesgue measure on $\mathbb{R}$. We may now apply results
(i) R2311: Tonelli's theorem for indicator functions
(ii) R2308: Area interpretation of unsigned basic integral

to obtain \begin{equation} \int_X f \, d \mu = (\mu \times \upsilon)(\Gamma) = \int_{[0, \infty]} \mu(\Gamma_t) \, d \upsilon = \int_{[0, \infty]} \mu( f \geq t ) \, d t \end{equation} $\square$