# Ergodic Theory

 Title: Ergodic Theory Author: Sebastien Gouezel Submission date: 2015-12-01 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_Theory-AFP, author = {Sebastien Gouezel}, title = {Ergodic Theory}, journal = {Archive of Formal Proofs}, month = dec, year = 2015, note = {\url{http://isa-afp.org/entries/Ergodic_Theory.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: Gromov_Hyperbolicity, Lp Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.