### 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.

### License

BSD License

### Topics

- Mathematics/Probability theory

### Session Ergodic_Theory

- SG_Library_Complement
- ME_Library_Complement
- Fekete
- Asymptotic_Density
- Measure_Preserving_Transformations
- Recurrence
- Invariants
- Ergodicity
- Shift_Operator
- Kingman
- Gouezel_Karlsson
- Kohlberg_Neyman_Karlsson
- Transfer_Operator
- Normalizing_Sequences

### Used by

- Roth’s Theorem on Arithmetic Progressions
- The Laws of Large Numbers
- Gromov Hyperbolicity
- Lp spaces

## Cite

×

Ergodic_Theory-AFP

    @article{Ergodic_Theory-AFP,
      author  = {Sebastien Gouezel},
      title   = {Ergodic Theory},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Ergodic_Theory.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016