ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4550 on D4490: Set of stationary events
Formulation 0
Let $P = (\Omega, \mathcal{F}, \mathbb{P}, T)$ be a D2839: Probability-preserving system such that
(i) $P$ is an D4492: Ergodic probability-preserving system
(ii) $E \in \mathcal{F}$ is an D1716: Event in $P$
Then \begin{equation} \lim_{N \to \infty} \frac{ \# \left\{ n \in \{ 0, \ldots, N - 1 \} : T^n \in E \right\} }{N} \overset{a.s.}{=} \mathbb{P}(E) \end{equation}
Proofs
Proof 0
Let $P = (\Omega, \mathcal{F}, \mathbb{P}, T)$ be a D2839: Probability-preserving system such that
(i) $P$ is an D4492: Ergodic probability-preserving system
(ii) $E \in \mathcal{F}$ is an D1716: Event in $P$
Applying results
(i) R4551: Expressing a finite composition of indicator function and measure-preserving transformation in terms of set cardinality
(ii) R1868: Composition of indicator function with set endomorphism
(iii) R4549:
(iv) R2089: Unsigned basic expectation is compatible with probability measure

we have \begin{equation} \begin{split} \lim_{N \to \infty} \frac{\# \{ n \in \{ 0, \ldots, N - 1 \} : T^n \in E \}}{N} & = \lim_{N \to \infty} \frac{1}{N} \sum_{n = 0}^{N - 1} I_{T^{-n} E} \\ & = \lim_{N \to \infty} \frac{1}{N} \sum_{n = 0}^{N - 1} (I_E \circ T^n) \overset{a.s.}{=} \mathbb{E} (I_E) = \mathbb{P}(E) \end{split} \end{equation} $\square$