ThmDex – An index of mathematical definitions, results, and conjectures.

Result R3517 on D5103: Unsigned basic expectation
Subresult of R3515: Unsigned basic integral zero iff function almost everywhere zero

Unsigned basic expectation zero iff random number almost surely zero

Formulation 0

Let $P = (\Omega, \mathcal{F}, \mathbb{P})$ be a D1159: Probability space such that

(i)	$X : \Omega \to [0, \infty]$ is a D5101: Random unsigned basic number on $P$

Then \begin{equation} X \overset{a.s.}{=} 0 \quad \iff \quad \mathbb{E} X = 0 \end{equation}

Formulation 1

Let $X \in \text{Random} [0, \infty]$ be a D5101: Random unsigned basic number.

Then \begin{equation} X \overset{a.s.}{=} 0 \quad \iff \quad \mathbb{E} X = 0 \end{equation}

Proofs

Proof 0

Let $P = (\Omega, \mathcal{F}, \mathbb{P})$ be a D1159: Probability space such that

(i)	$X : \Omega \to [0, \infty]$ is a D5101: Random unsigned basic number on $P$