Ergodic theory

Ergodic theory studies measure-preserving transformations and their statistical behaviour: ergodic averages, recurrence, mixing and the structure of measure-preserving actions.

• Bilinear polynomial ergodic averages
• Bourgain's polynomial ergodic theorem
• Genericity of weak mixing
• Lax approximation theorem
• Multiplicative recurrence along Pythagorean pairs
• Rokhlin lemma
• Birkhoff ergodic theorem
• Kingman's subadditive ergodic theorem

TheoremFurstenberg multiple recurrence theorem#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\alpha\), let \(T : \alpha \to \alpha\) be a measurable map preserving \(\mu\), and let \(A\) be a measurable set with \(\mu(A) > 0\). For \(m \in \mathbb{N}\) write \(T^{-m}(A)\) for the preimage of \(A\) under the \(m\)-th iterate of \(T\). Then for every integer \(k > 0\) there is an integer \(n > 0\) such that

\[\mu\Big(\bigcap_{i=0}^{k-1} T^{-i n}(A)\Big) > 0.\]

Proof: We apply the finitary Szemerédi theorem to dense sets of return times in finite orbit segments, using an averaging argument to obtain a positive-measure family of such segments.

public theorem furstenberg_multipleRecurrence
    {α : Type*} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ]
    {T : α → α} (hT : MeasurePreserving T μ μ)
    {A : Set α} (hA : MeasurableSet A) (hApos : 0 < μ A)
    (k : ℕ) (hk : 0 < k) :
    ∃ n : ℕ, 0 < n ∧ 0 < μ (⋂ i ∈ Finset.range k, T^[i * n] ⁻¹' A)

Sources

• H. Furstenberg, J. Analyse Math. 31 (1977) and Recurrence in Ergodic Theory (1981); Lean states one-transformation arithmetic-progression k-term intersection form without ergodicity hypothesis.

Uses 1

Proof usesSzemerédi's theorem

TheoremKrylov–Bogolyubov theorem#✓fully proved

Every continuous map \(T : X \to X\) of a nonempty compact metric space \(X\) to itself has an invariant Borel probability measure: there is a probability measure \(\mu\) on the Borel \(\sigma\)-algebra of \(X\) whose pushforward under \(T\) equals \(\mu\).

theorem krylov_bogolyubov
    {X : Type*} [MetricSpace X] [CompactSpace X] [Nonempty X]
    [MeasurableSpace X] [BorelSpace X]
    {T : X → X} (hT : Continuous T) :
    ∃ μ : Measure X, IsProbabilityMeasure μ ∧ Measure.map T μ = μ

Sources

• N. M. Krylov and N. N. Bogolyubov, Ann. Math. 38 (1937), 65-113, DOI 10.2307/1968511.

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.