6.2. Concrete examples🔗

Mathlib contains proofs that certain maps are ergodic. Here are two examples of maps on the circle \mathbb{R} / \mathbb{Z} (with its Haar measure):

1. Given given a natural number n > 1, the map x ↦ nx is ergodic. This appears in Mathlib as AddCircle.ergodic_nsmul.

2. Given a point a, the map x ↦ x + a is ergodic iff a is has infinite order (i.e., is irrational). This appears in Mathlib as AddCircle.ergodic_add_right.