Solution (source code)

= Solution

The <Birkhoff ergodic theorem> states that if $T$ is a <measure-preserving transformation> and $f\in L^1(\mu)$, then
$$
\boxed{
\frac1n\sum_{j=0}^{n-1}f(T^jx)
\longrightarrow
\mathbb E[f\mid\mathcal I](x)
\quad\text{for almost every }x
},
$$
where $\mathcal I$ is the <invariant sigma-algebra>. The limit has the same integral as $f$. If $T$ is an <ergodic transformation>, the limit is the constant $\int_Xf\,d\mu$ almost everywhere.