Skip to content

lua-vr/pointwise-birkhoff

Repository files navigation

$$\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.}$$

About

A proof of Pointwise Birkhoff Ergodic Theorem in Lean

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Contributors 3

  •  
  •  
  •  

Languages