ThmDex – An index of mathematical definitions, results, and conjectures.
Real variance partition into first and second moments
Formulation 0
Let $X \in \text{Random}(\mathbb{R})$ be a D3161: Random real number such that
(i) \begin{equation} \mathbb{E} |X|^2 < \infty \end{equation}
Then \begin{equation} \text{Var} X = \mathbb{E}(X^2) - (\mathbb{E} X)^2 \end{equation}
Formulation 1
Let $X \in \text{Random}(\mathbb{R})$ be a D3161: Random real number such that
(i) \begin{equation} \mathbb{E} |X|^2 < \infty \end{equation}
Then \begin{equation} \mathbb{E}[(X - \mathbb{E} X)^2] = \mathbb{E}(X^2) - (\mathbb{E} X)^2 \end{equation}
Formulation 2
Let $X \in \text{Random}(\mathbb{R})$ be a D3161: Random real number such that
(i) \begin{equation} \mathbb{E} |X|^2 < \infty \end{equation}
Then \begin{equation} \text{Var} X = \mathbb{E}(X X) - \mathbb{E} X \mathbb{E} X \end{equation}
Formulation 3
Let $P = (\Omega, \mathcal{F}, \mathbb{P})$ be a D1159: Probability space such that
(i) $X : \Omega \to \mathbb{R}$ is a D3161: Random real number on $P$
(ii) \begin{equation} \mathbb{E} |X|^2 < \infty \end{equation}
Then \begin{equation} \text{Var}(X) = \mathbb{E} (X^2) - (\mathbb{E} X)^2 \end{equation}
Formulation 4
Let $P = (\Omega, \mathcal{F}, \mathbb{P})$ be a D1159: Probability space such that
(i) $X : \Omega \to \mathbb{R}$ is a D3161: Random real number on $P$
(ii) \begin{equation} \mathbb{E} |X|^2 < \infty \end{equation}
Then \begin{equation} \mathbb{E}[(X - \mathbb{E} X)^2] = \mathbb{E} (X X) - \mathbb{E} X \mathbb{E} X \end{equation}
Proofs
Proof 0
Let $X \in \text{Random}(\mathbb{R})$ be a D3161: Random real number such that
(i) \begin{equation} \mathbb{E} |X|^2 < \infty \end{equation}
Since $\mathbb{E} |X|^2 < \infty$, result R3581: Absolute moment inherits finiteness from greater exponents for random complex number guarantees that also $\mathbb{E} |X| < \infty$. Additionally, result R4514: Even integer absolute moments coincide with moments for random basic real number shows that $\mathbb{E} |X|^2 = \mathbb{E} X^2$, whence $\mathbb{E} X^2 < \infty$ as well. That is, all the relevant quantities exist and are finite.

Then, by direct computation, we have \begin{equation} \begin{split} \mathsf{Var}(X) & = \mathbb{E}[(X - \mathbb{E} X)^2] \\ & = \mathbb{E}(X^2) - \mathbb{E}(2 X \mathbb{E} X) + (\mathbb{E} X)^2 \\ & = \mathbb{E}(X^2) - 2 \mathbb{E} (X) \mathbb{E}(X) + (\mathbb{E} X)^2 \\ & = \mathbb{E}(X^2) - 2 \mathbb{E} (X)^2 + (\mathbb{E} X)^2 \\ & = \mathbb{E}(X^2) - (\mathbb{E} X)^2 \end{split} \end{equation} $\square$