Theorem: Birkhoff's Ergodic Theorem

Let $\struct {X, \BB, \mu, T}$ be a measure-preserving dynamical system.
Let $f: X \to \overline \R$ be a $\mu$-integrable function.
Then a $\mu$-integrable function $\tilde f$ exists such that:
:$\forall x \in X : \map {\tilde f} {T x} = \map {\tilde f} x$
and:
:$\ds \lim_{n \mathop \to \infty} \dfrac 1 n \sum_{n \mathop = 0}^{n - 1} f \circ T^n = \tilde f$
converges $\mu$-almost everywhere and in $L^1$-norm.
Furthermore, we have:
:$\tilde f = \expect {f \mid \II_T}$
where:
:$\expect {f \mid \II_T}$ denotes the conditional expectation of $f$ given $\II_T$
:$\II_T := \set { A \in \BB : T^{-1} \sqbrk A = A }$

Proof:
Let $f_0 : X \to \R$ be a bounded measurable function.
For $N \in \N_{>0}$, let:
:$\ds \map {A_N} {f_0} = \frac 1 N \sum_{n \mathop = 0}^{N-1} f_0 \circ T^n$
By $L^1$ Mean Ergodic Theorem, there is a $\mu$-integrable function $F_0$ such that:
:$F_0 \circ T = F_0$
and:
:$\ds \lim_{N \mathop \to \infty}\norm {F_0 - \map {A_N} {f_0}}_1 = 0$
Let $\epsilon > 0$.
Then fix an $M$ such that:
:$\ds \norm {F_0 - \map {A_M} {f_0} }_1 < \epsilon ^2$
Let:
:$g = F_0 - \map {A_M} {f_0}$
By Maximal Ergodic Theorem:
:$\ds \epsilon \map \mu {\set { \sup_{N \mathop \ge 1} \size {\map {A_N} g} > \epsilon  } } \le \int \size g \rd \mu$
Therefore:
:$\ds \map \mu {\set { \sup_{N \mathop \ge 1} \size {\map {A_N} g} > \epsilon  } } \le \epsilon$
On the other hand:
{{begin-eqn}}
{{eqn | l =　\size {\map {A_N} {\map {A_M} {f_0} } - \map {A_N} {f_0} }
      | o = \le
      | r = \frac {3 M \paren {M-1} \norm {f_0}_\infty}{2 N}
}}
{{end-eqn}}
In particular:
{{begin-eqn}}
{{eqn | l = \limsup_{N \mathop \to \infty} \size {F_0 - \map {A_N} {f_0} }
      | r = \limsup_{N \mathop \to \infty} \size {\map {A_N} g}
}}
{{eqn | o = \le
      | r = \sup _{N \mathop \ge 1} \size {\map {A_N} g}
}}
{{end-eqn}}
Therefore, for all $\epsilon > \epsilon' > 0$:
{{begin-eqn}}
{{eqn | l = \map \mu {\set {\limsup_{N \mathop \to \infty} \size {F_0 - \map {A_N} {f_0} } > \epsilon } }
      | o = \le
      | r = \map \mu {\set {\limsup_{N \mathop \to \infty} \size {F_0 - \map {A_N} {f_0} } > \epsilon' } }
}}
{{eqn | o = \le
      | r = \map \mu {\set {\sup _{N \mathop \ge 1} \size {\map {A_N} g} > \epsilon' } }
}}
{{eqn | o = \le
      | r = \epsilon'
}}
{{end-eqn}}
Letting $\epsilon' \to 0$:
:$\ds \map \mu {\set {\limsup_{N \mathop \to \infty} \size {F_0 - \map {A_N} {f_0} } > \epsilon } } = 0$
Thus:
{{begin-eqn}}
{{eqn | l = \map \mu {\set {\limsup_{N \mathop \to \infty} \size {F_0 - \map {A_N} {f_0} } > 0 } }
      | r = \map \mu {\bigcup_{k\ge 1} \set {\limsup_{N \mathop \to \infty} \size {F_0 - \map {A_N} {f_0} } > \frac 1 k } }
}}
{{eqn | o = \le
      | r = \sum_{k \mathop \ge 1} \map \mu {\set {\limsup_{N \mathop \to \infty} \size {F_0 - \map {A_N} {f_0} } > \frac 1 k } }
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{qed|lemma}}
Finally, $f$ be an $\mu$-integrable function.
By $L^1$ Mean Ergodic Theorem, there is a $\mu$-integrable function $F$ such that:
:$F \circ T = F$
and:
:$\ds \lim_{N \mathop \to \infty}\norm {F - \map {A_N} f}_1 = 0$
Let $\epsilon > 0$.
Then there exists a bounded function $f_0$ such that:
:$\ds \norm {f - f_0 }_1 < \epsilon ^2$
For example, for a sufficiently large $M > 0$, choose:
:$\ds f_0 = f \cdot \chi_{\set {\size f \le M} }$
Then:
{{begin-eqn}}
{{eqn | o =
      | r = \map \mu {\set {\limsup_{N \mathop \to \infty} \size {F - \map {A_N} f } > 2 \epsilon } }
}}
{{eqn | o = \le
      | r = \map \mu {\set {\limsup_{N \mathop \to \infty} \paren { \size {F - F_0} + \size {F_0 - \map {A_N} {f_0} } + \size {\map {A_N} {f - f_0} } } > 2 \epsilon } }
}}
{{eqn | r = \map \mu {\set { \size {F - F_0} + \limsup_{N \mathop \to \infty} \size {\map {A_N} {f - f_0} } > 2 \epsilon } }
}}
{{eqn | o = \le
      | r = \map \mu {\set { \size {F - F_0} > \epsilon } } + \map \mu {\set { \limsup_{N \mathop \to \infty} \size {\map {A_N} {f - f_0} } > \epsilon } }
}}
{{eqn | o = \le
      | r = \frac 2 \epsilon \int \size {F-F_0} \rd \mu
}}
{{eqn | o = \le
      | r = 2 \epsilon
}}
{{end-eqn}}
Similarly to the argument for $f_0$ and $F_0$ above, it follows:
:$\ds \map \mu {\set {\limsup_{N \mathop \to \infty} \size {F - \map {A_N} f } > 0} } = 0$
{{Finish|Reasning}}