Integration identity for nonnegative random variables

I'm trying to furnish a proof for the following identity, and would like to have my proof checked.

Suppose $$(\Omega, \mathcal{F}, \mathbf{P})$$ is a probability space on which random variable $$X: \Omega \to \mathbf{R}$$ is defined. If $$X$$ is nonnegative, then $$\mathbf{E} X= \int_0^\infty \mathbf{P}\{X \geq t\}\, dt.$$

Here's the proof: $$\mathbf{E}X = \int_\Omega X(\omega) d\mathbf{P}(\omega) = \int_\Omega \left(\int_{\mathbf{R}_+} \mathbf{1}_{[0, X(\omega)]}(t) ~dt \right) ~d\mathbf{P}(\omega).$$ The first equality is trivial: $$\lambda([0, X(\omega)]) = X(\omega)$$, where $$\lambda$$ denotes Lebesgue measure.

By Fubini's Theorem, we may interchange the measures. $$\mathbf{E}X = \int_{\mathbf{R}_+} \left(\int_\Omega\mathbf{1}_{[0, X(\omega)]}(t) ~d\mathbf{P}(\omega) \right) ~dt = \int_0^\infty \mathbf{P}\{X \geq t\} \, dt.$$ The last equality arises by obseving that for $$t \geq 0$$, $$0 \leq t \leq X(\omega)$$ iff $$X(\omega) \geq t$$, and the set $$X^{-1}([t, \infty)) \in \mathcal{F}$$.

The only thing that isn't immediate is the use of Fubini: the map $$(t, \omega) \mapsto \begin{cases} 1, & X(\omega) \geq t \\ 0 & \text{else} \end{cases}$$ needs to be $$\mathcal{F} \otimes \mathcal{B}_\mathbf{R}$$ measurable, i.e., the set $$A = \{(\omega, t) : X(\omega) \geq t\}$$ needs to be measurable. If $$\phi_n \uparrow X$$ are nonnegative simple functions, then $$A_0 = \cap_n A_n$$, where $$A_n = \{(\omega, t) : X(\omega) - t > -1/n\}.$$ Notice that $$A_n = \cup_m \{ (\omega, t) : \phi_m(\omega) - t > -1/n\}$$. Note that $$\phi_m = \sum_i c_i \mathbf{1}_{F_i}$$, where $$F_i$$ are disjoint and $$c_i > 0$$. Finally, notice that $$\{ (\omega, t) : \phi_m(\omega) - t > -1/n\} = \cup_{i=1}^n (F_i \times [0, c_i + 1/n)) \cup (\cap_i F_i^c) \times [0, 1/n).$$ This set is hence measurable, and now the result follows since the product sigma algebra is closed under intersection and union.

• Yes.    – Did Dec 10 '18 at 2:51
• Your question is very specific, and user Did has already given you the confirmation. Nonetheless, I'd still like to make a link to a closely related post. – Lee David Chung Lin Dec 10 '18 at 4:33