[proofplan]
The proof has two ingredients. First, the transformation $t\mapsto 1-t$ preserves the uniform distribution on $(0,1)$, so $Y=g(U)$ and $Y'=g(1-U)$ have the same distribution and therefore the same variance. Second, we expand the variance of $Y+Y'$ directly from the definitions of variance and covariance, then use homogeneity of variance under multiplication by $1/2$.
[/proofplan]
[step:Verify that the random variables have finite second moments]
Let $R:(0,1)\to(0,1)$ be the Borel map defined by $R(t)=1-t$. Since $U\sim\operatorname{Unif}(0,1)$, the law of $U$ is $\mathcal{L}^1$ restricted to $(0,1)$. Applying the law of the [random variable](/page/Random%20Variable) to the non-negative Borel function $t\mapsto g(t)^2$ gives
\begin{align*}
\mathbb{E}[Y^2]=\int_{\Omega} g(U(\omega))^2\,d\mathbb{P}(\omega)=\int_0^1 g(t)^2\,d\mathcal{L}^1(t)<\infty.
\end{align*}
The map $R$ preserves $\mathcal{L}^1$ on $(0,1)$, so $R\circ U=1-U$ also has law $\operatorname{Unif}(0,1)$. Applying the law of the random variable to $R\circ U$ and the non-negative Borel function $t\mapsto g(t)^2$ gives
\begin{align*}
\mathbb{E}[(Y')^2]=\int_{\Omega} g(1-U(\omega))^2\,d\mathbb{P}(\omega)=\int_0^1 g(t)^2\,d\mathcal{L}^1(t)<\infty.
\end{align*}
Thus $Y,Y'\in L^2(\Omega,\mathcal{F},\mathbb{P})$, and their variances and covariance are finite.
[/step]
[step:Use the reflection symmetry of the uniform distribution]
Because $R:(0,1)\to(0,1)$, $R(t)=1-t$, preserves $\mathcal{L}^1$ on $(0,1)$, the random variables $U$ and $1-U=R\circ U$ have the same distribution. Since $g$ is Borel measurable, the pushforwards of these two laws under $g$ are equal. Hence $Y=g(U)$ and $Y'=g(1-U)$ have the same distribution.
In particular,
\begin{align*}
\mathbb{E}[Y']=\mathbb{E}[Y]
\end{align*}
and
\begin{align*}
\operatorname{Var}(Y')=\operatorname{Var}(Y).
\end{align*}
[guided]
The only distributional point in the proof is the antithetic symmetry. Define the reflection map $R:(0,1)\to(0,1)$ by $R(t)=1-t$. This map is Borel measurable, and it preserves one-dimensional [Lebesgue measure](/page/Lebesgue%20Measure) on $(0,1)$: reflecting an interval inside $(0,1)$ gives another interval with the same length, and the equality extends to Borel sets by the defining [regularity of Lebesgue measure](/theorems/4910).
Since $U\sim\operatorname{Unif}(0,1)$, the law of $U$ is $\mathcal{L}^1$ restricted to $(0,1)$. Therefore $R\circ U=1-U$ has the same law as $U$. Now apply the same measurable function $g:(0,1)\to\mathbb{R}$ to both random variables. Equal input laws give equal output laws, so $g(U)$ and $g(1-U)$ have the same distribution.
Thus $Y$ and $Y'$ have identical first and second moments. Since both are square-integrable, variance is determined by the formula
\begin{align*}
\operatorname{Var}(Z)=\mathbb{E}[Z^2]-\mathbb{E}[Z]^2
\end{align*}
for any real-valued $Z\in L^2(\Omega,\mathcal{F},\mathbb{P})$. Applying this formula to $Z=Y$ and $Z=Y'$ gives
\begin{align*}
\operatorname{Var}(Y')=\operatorname{Var}(Y).
\end{align*}
[/guided]
[/step]
[step:Expand the variance of the averaged pair]
Define the centered random variables $A:\Omega\to\mathbb{R}$ and $B:\Omega\to\mathbb{R}$ by
\begin{align*}
A=Y-\mathbb{E}[Y]
\end{align*}
and
\begin{align*}
B=Y'-\mathbb{E}[Y'].
\end{align*}
By square-integrability, $A,B\in L^2(\Omega,\mathcal{F},\mathbb{P})$. The [Cauchy-Schwarz inequality](/theorems/432) in $L^2(\Omega,\mathcal{F},\mathbb{P})$ gives
\begin{align*}
\mathbb{E}[|AB|]\leq \mathbb{E}[A^2]^{1/2}\mathbb{E}[B^2]^{1/2}<\infty,
\end{align*}
so $AB\in L^1(\Omega,\mathcal{F},\mathbb{P})$. Using the definition of variance and covariance,
\begin{align*}
\operatorname{Var}(Y+Y')=\mathbb{E}[(A+B)^2].
\end{align*}
Expanding the square inside the expectation and using linearity of expectation gives
\begin{align*}
\operatorname{Var}(Y+Y')=\mathbb{E}[A^2]+2\mathbb{E}[AB]+\mathbb{E}[B^2].
\end{align*}
By definition, $\mathbb{E}[A^2]=\operatorname{Var}(Y)$, $\mathbb{E}[B^2]=\operatorname{Var}(Y')$, and $\mathbb{E}[AB]=\operatorname{Cov}(Y,Y')$. Hence
\begin{align*}
\operatorname{Var}(Y+Y')=\operatorname{Var}(Y)+\operatorname{Var}(Y')+2\operatorname{Cov}(Y,Y').
\end{align*}
Substituting $\operatorname{Var}(Y')=\operatorname{Var}(Y)$ gives
\begin{align*}
\operatorname{Var}(Y+Y')=2\operatorname{Var}(Y)+2\operatorname{Cov}(Y,Y').
\end{align*}
[/step]
[step:Divide by the square of the averaging factor]
Since variance is homogeneous of degree two under scalar multiplication,
\begin{align*}
\operatorname{Var}\left(\frac{Y+Y'}{2}\right)=\frac{1}{4}\operatorname{Var}(Y+Y').
\end{align*}
Using the identity from the previous step,
\begin{align*}
\operatorname{Var}\left(\frac{Y+Y'}{2}\right)=\frac{1}{4}\left(2\operatorname{Var}(Y)+2\operatorname{Cov}(Y,Y')\right).
\end{align*}
Simplifying the constants yields
\begin{align*}
\operatorname{Var}\left(\frac{Y+Y'}{2}\right)=\frac{1}{2}\operatorname{Var}(Y)+\frac{1}{2}\operatorname{Cov}(Y,Y').
\end{align*}
This is the asserted antithetic variance identity.
[/step]
