Abstract: 
Ergodic theory is the branch of mathematics that studies the behaviour of measure preserving transformations, in finite or infinite measure. It interacts both with probability theory (mainly through measure theory) and with geometry as a lot of interesting examples are from geometric origin. We implement the first definitions and theorems of ergodic theory, including notably PoicarĂ© recurrence theorem for finite measure preserving systems (together with the notion of conservativity in general), induced maps, Kac's theorem, Birkhoff theorem (arguably the most important theorem in ergodic theory), and variations around it such as conservativity of the corresponding skew product, or Atkinson lemma. 
BibTeX: 
@article{Ergodic_TheoryAFP,
author = {Sebastien Gouezel},
title = {Ergodic Theory},
journal = {Archive of Formal Proofs},
month = dec,
year = 2015,
note = {\url{http://isaafp.org/entries/Ergodic_Theory.html},
Formal proof development},
ISSN = {2150914x},
}
