GitHub - estradilua/pointwise-birkhoff: A proof of Pointwise Birkhoff Ergodic Theorem in Lean

$$\lim_{n \to \infty}\frac1n \sum_{i=0}^{n-1} \varphi \circ f^i(x) = \mathbb{E}_{\mu}(\varphi \mid \mathcal{I})(x) \quad\text{a.e.}$$

Name		Name	Last commit message	Last commit date
Latest commit History 67 Commits
.vscode		.vscode
BirkhoffErgodicThm		BirkhoffErgodicThm
.gitignore		.gitignore
BirkhoffErgodicThm.lean		BirkhoffErgodicThm.lean
LICENSE		LICENSE
README.md		README.md
lake-manifest.json		lake-manifest.json
lakefile.lean		lakefile.lean
lakefile.olean		lakefile.olean
lean-toolchain		lean-toolchain

Provide feedback