Birkhoff ergodic theorem

TheoremHopf maximal ergodic theorem#✓fully proved

Let \(\mu\) be a finite measure on a measurable space \(\alpha\), let \(T : \alpha \to \alpha\) preserve \(\mu\), and let \(f : \alpha \to \mathbb{R}\) be measurable and \(\mu\)-integrable. For a natural number \(n\) write \(S_n f(x) = \sum_{k=0}^{n-1} f(T^k x)\). Then the integral of \(f\) with respect to \(\mu\) over the set of points \(x \in \alpha\) such that \(S_n f(x) > 0\) for some natural number \(n\) is nonnegative.

theorem maximal_ergodic
    {α : Type*} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ]
    {T : α → α} (hT : MeasurePreserving T μ μ)
    {f : α → ℝ} (hf : Measurable f) (hfi : Integrable f μ) :
    0 ≤ ∫ x in {x | ∃ n, 0 < birkhoffSum T f n x}, f x ∂μ

Used by 2

Used byBirkhoff pointwise ergodic theorem (ergodic case) · Kingman's subadditive ergodic theorem (nonnegative case)

DefinitionMaximal divergence set#✓fully proved

Let \(\alpha\) be a measurable space, \(T : \alpha \to \alpha\) a map, \(g : \alpha \to \mathbb{R}\) a function and \(c\) a real number. The maximal divergence set of \(T\), \(g\) and \(c\) is the set of points \(x \in \alpha\) for which there is a rational number \(q > c\) such that \(n q < \sum_{k=0}^{n-1} g(T^k x)\) for infinitely many natural numbers \(n\).

noncomputable def DickSet {α : Type*} [MeasurableSpace α]
    (T : α → α) (g : α → ℝ) (c : ℝ) : Set α :=
  ⋃ (q : ℚ) (_ : c < (q : ℝ)), ⋂ (N : ℕ), ⋃ (n : ℕ) (_ : N ≤ n),
    {x | (n : ℝ) * (q : ℝ) < birkhoffSum T g n x}

Used by 6

Used byBirkhoff pointwise ergodic theorem (ergodic case) · Invariance of the maximal divergence set · Invariance of the maximal divergence set under iterates · Measurability of the maximal divergence set · Membership in the maximal divergence set · Kingman's subadditive ergodic theorem (nonnegative case)

TheoremMeasurability of the maximal divergence set#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(T : \alpha \to \alpha\) preserve \(\mu\), and let \(g : \alpha \to \mathbb{R}\) be measurable. Then for every real number \(c\), the maximal divergence set of \(T\), \(g\) and \(c\) is a measurable set.

theorem dick_measurable
    {α : Type*} [MeasurableSpace α] {μ : Measure α}
    {T : α → α} (hT : MeasurePreserving T μ μ)
    {g : α → ℝ} (hg : Measurable g) (c : ℝ) :
    MeasurableSet (DickSet T g c)

Uses 1 · Used by 2

Statement usesMaximal divergence set

Used byBirkhoff pointwise ergodic theorem (ergodic case) · Kingman's subadditive ergodic theorem (nonnegative case)

TheoremMembership in the maximal divergence set#✓fully proved

Let \(\alpha\) be a measurable space, \(T : \alpha \to \alpha\) a map, \(g : \alpha \to \mathbb{R}\) a function, \(c\) a real number and \(x \in \alpha\). Then \(x\) lies in the maximal divergence set of \(T\), \(g\) and \(c\) if and only if there is a rational number \(q > c\) such that for every natural number \(N\) there is a natural number \(n \ge N\) with \(n q < \sum_{k=0}^{n-1} g(T^k x)\).

theorem dick_mem {α : Type*} [MeasurableSpace α]
    {T : α → α} {g : α → ℝ} {c : ℝ} {x : α} :
    x ∈ DickSet T g c ↔ ∃ q : ℚ, c < (q : ℝ) ∧
      ∀ N : ℕ, ∃ n : ℕ, N ≤ n ∧ (n : ℝ) * (q : ℝ) < birkhoffSum T g n x

Uses 1 · Used by 4

Statement usesMaximal divergence set

Used byBirkhoff pointwise ergodic theorem (ergodic case) · Invariance of the maximal divergence set · Invariance of the maximal divergence set under iterates · Kingman's subadditive ergodic theorem (nonnegative case)

TheoremInvariance of the maximal divergence set#✓fully proved

Let \(\alpha\) be a measurable space. For every map \(T : \alpha \to \alpha\), every function \(g : \alpha \to \mathbb{R}\) and every real number \(c\), the preimage under \(T\) of the maximal divergence set of \(T\), \(g\) and \(c\) equals that set.

theorem dick_inv {α : Type*} [MeasurableSpace α]
    {T : α → α} {g : α → ℝ} {c : ℝ} :
    T ⁻¹' DickSet T g c = DickSet T g c

Uses 2 · Used by 1

Statement usesMaximal divergence set

Proof usesMembership in the maximal divergence set

Used byBirkhoff pointwise ergodic theorem (ergodic case)

TheoremInvariance of the maximal divergence set under iterates#✓fully proved

Let \(\alpha\) be a measurable space, \(T : \alpha \to \alpha\) a map, \(g : \alpha \to \mathbb{R}\) a function and \(c\) a real number. For every natural number \(k\) and every \(x \in \alpha\), the point \(T^k x\) lies in the maximal divergence set of \(T\), \(g\) and \(c\) if and only if \(x\) does.

theorem dick_iter {α : Type*} [MeasurableSpace α]
    {T : α → α} {g : α → ℝ} {c : ℝ} (k : ℕ) (x : α) :
    (T^[k] x ∈ DickSet T g c) ↔ (x ∈ DickSet T g c)

Uses 2 · Used by 2

Statement usesMaximal divergence set

Proof usesMembership in the maximal divergence set

Used byBirkhoff pointwise ergodic theorem (ergodic case) · Kingman's subadditive ergodic theorem (nonnegative case)

TheoremBirkhoff sums of a function cut off to an invariant set, inside the set#✓fully proved

Let \(\alpha\) be a measurable space, \(T : \alpha \to \alpha\) a map, \(g : \alpha \to \mathbb{R}\) a function, \(c\) a real number, and \(D \subseteq \alpha\) a set such that for every natural number \(k\) and every \(x \in \alpha\), \(T^k x \in D\) if and only if \(x \in D\). Let \(h : \alpha \to \mathbb{R}\) satisfy \(h(y) = g(y) - c\) for \(y \in D\) and \(h(y) = 0\) for \(y \notin D\). Then for every \(x \in D\) and every natural number \(n\), \(\sum_{k=0}^{n-1} h(T^k x) = \sum_{k=0}^{n-1} g(T^k x) - n c\).

theorem dick_sum_in {α : Type*} [MeasurableSpace α]
    {T : α → α} {g : α → ℝ} {c : ℝ}
    (D : Set α)
    (hiter : ∀ (k : ℕ) (x : α), (T^[k] x ∈ D) ↔ (x ∈ D))
    (hfun : α → ℝ) (hfundef : ∀ y : α, hfun y = D.indicator (fun y => g y - c) y)
    (x : α) (hx : x ∈ D) (n : ℕ) :
    birkhoffSum T hfun n x = birkhoffSum T g n x - n * c

Used by 2

Used byBirkhoff pointwise ergodic theorem (ergodic case) · Kingman's subadditive ergodic theorem (nonnegative case)

TheoremBirkhoff sums of a function cut off to an invariant set, outside the set#✓fully proved

Let \(\alpha\) be a measurable space, \(T : \alpha \to \alpha\) a map, \(g : \alpha \to \mathbb{R}\) a function, \(c\) a real number, and \(D \subseteq \alpha\) a set such that for every natural number \(k\) and every \(x \in \alpha\), \(T^k x \in D\) if and only if \(x \in D\). Let \(h : \alpha \to \mathbb{R}\) satisfy \(h(y) = g(y) - c\) for \(y \in D\) and \(h(y) = 0\) for \(y \notin D\). Then for every \(x \notin D\) and every natural number \(n\), \(\sum_{k=0}^{n-1} h(T^k x) = 0\).

theorem dick_sum_out {α : Type*} [MeasurableSpace α]
    {T : α → α} {g : α → ℝ} {c : ℝ}
    (D : Set α)
    (hiter : ∀ (k : ℕ) (x : α), (T^[k] x ∈ D) ↔ (x ∈ D))
    (hfun : α → ℝ) (hfundef : ∀ y : α, hfun y = D.indicator (fun y => g y - c) y)
    (x : α) (hx : x ∉ D) (n : ℕ) :
    birkhoffSum T hfun n x = 0

Used by 2

Used byBirkhoff pointwise ergodic theorem (ergodic case) · Kingman's subadditive ergodic theorem (nonnegative case)

TheoremBirkhoff pointwise ergodic theorem (ergodic case)#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\alpha\), let \(T : \alpha \to \alpha\) be ergodic with respect to \(\mu\) (in particular \(T\) preserves \(\mu\)), and let \(g : \alpha \to \mathbb{R}\) be \(\mu\)-integrable. Then for \(\mu\)-almost every \(x \in \alpha\), the Birkhoff averages \(\frac{1}{n} \sum_{k=0}^{n-1} g(T^k x)\) converge to \(\int g \, d\mu\) as \(n \to \infty\).

theorem birkhoff_pointwise_ergodic
    {α : Type*} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ]
    {T : α → α} (hT : Ergodic T μ)
    {g : α → ℝ} (hg : Integrable g μ) :
    ∀ᵐ x ∂μ, Filter.Tendsto (fun n => birkhoffAverage ℝ T g n x) Filter.atTop
      (nhds (∫ y, g y ∂μ))

Sources

• G. D. Birkhoff, Proc. Natl. Acad. Sci. USA 17 (1931); Walters, Intro to Ergodic Theory; Lean states ergodic case for ℝ-valued integrable functions while general theorem gives conditional expectation onto invariant σ-algebra.

Uses 8 · Used by 2

Proof usesMaximal divergence set · Invariance of the maximal divergence set · Invariance of the maximal divergence set under iterates · Measurability of the maximal divergence set · Membership in the maximal divergence set · Birkhoff sums of a function cut off to an invariant set, inside the set · Birkhoff sums of a function cut off to an invariant set, outside the set · Hopf maximal ergodic theorem

Used byBirkhoff limit of an ergodic map is the space average · Birkhoff's ergodic theorem in \(L^1\) for bounded functions

TheoremIntegrability of Birkhoff sums#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(T : \alpha \to \alpha\) preserve \(\mu\), and let \(g : \alpha \to \mathbb{R}\) be \(\mu\)-integrable. Then for every \(n \in \mathbb{N}\) the Birkhoff sum \(x \mapsto \sum_{k=0}^{n-1} g(T^k x)\) is \(\mu\)-integrable.

theorem integrable_birkhoffSum_of_measurePreserving
    (hmp : MeasurePreserving T μ μ) {g : α → ℝ} (hg : Integrable g μ) (n : ℕ) :
    Integrable (birkhoffSum T g n) μ

Used by 7

Used byMaximal ergodic theorem · Integrability of Birkhoff averages · Maximal ergodic inequality on an invariant set · Lower limit of the normalized defect is finite almost everywhere · Expectation of a subadditive cocycle grows at most linearly · Truncated defect is a nonnegative subadditive cocycle · Negative defect is a subadditive cocycle

TheoremIntegrability of Birkhoff averages#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(T : \alpha \to \alpha\) preserve \(\mu\), and let \(g : \alpha \to \mathbb{R}\) be \(\mu\)-integrable. Then for every \(n \in \mathbb{N}\) the Birkhoff average \(x \mapsto \frac{1}{n} \sum_{k=0}^{n-1} g(T^k x)\) is \(\mu\)-integrable (for \(n = 0\) it is the zero function).

theorem integrable_birkhoffAverage_of_measurePreserving
    (hmp : MeasurePreserving T μ μ) {g : α → ℝ} (hg : Integrable g μ) (n : ℕ) :
    Integrable (birkhoffAverage ℝ T g n) μ

Uses 1 · Used by 7

Proof usesIntegrability of Birkhoff sums

Used byBirkhoff's ergodic theorem in \(L^1\) (ergodic case) · Integrability of the Birkhoff limit · Birkhoff averages are \(L^1\)-contractions · Oscillation set of Birkhoff averages is null · Birkhoff limit preserves integrals over invariant sets · Birkhoff averages converge almost everywhere to the Birkhoff limit · Birkhoff's ergodic theorem in \(L^1\) for bounded functions

TheoremInvariance of the integral under iterates#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(T : \alpha \to \alpha\) preserve \(\mu\), and let \(u : \alpha \to \mathbb{R}\) be \(\mu\)-integrable. Then for every \(k \in \mathbb{N}\), writing \(T^k\) for the \(k\)-th iterate of \(T\), we have \(\int u(T^k x) \, d\mu(x) = \int u \, d\mu\).

theorem integral_comp_iterate_of_measurePreserving
    (hmp : MeasurePreserving T μ μ) {u : α → ℝ} (hu : Integrable u μ) (k : ℕ) :
    ∫ x, u (T^[k] x) ∂μ = ∫ x, u x ∂μ

Used by 1

Used byBirkhoff averages preserve the integral

TheoremBirkhoff averages preserve the integral#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(T : \alpha \to \alpha\) preserve \(\mu\), and let \(u : \alpha \to \mathbb{R}\) be \(\mu\)-integrable. Then for every \(n \ge 1\), \(\int \frac{1}{n} \sum_{k=0}^{n-1} u(T^k x) \, d\mu(x) = \int u \, d\mu\).

theorem integral_birkhoffAverage_of_measurePreserving
    (hmp : MeasurePreserving T μ μ) {u : α → ℝ} (hu : Integrable u μ)
    {n : ℕ} (hn : 0 < n) :
    ∫ x, birkhoffAverage ℝ T u n x ∂μ = ∫ x, u x ∂μ

Uses 1 · Used by 1

Proof usesInvariance of the integral under iterates

Used byBirkhoff averages are \(L^1\)-contractions

TheoremTriangle inequality for Birkhoff averages#✓fully proved

Let \(T : \alpha \to \alpha\) be a map. For \(f : \alpha \to \mathbb{R}\) and \(n \ge 1\) write \(A_n f(x) = \frac{1}{n} \sum_{k=0}^{n-1} f(T^k x)\) for the \(n\)-th Birkhoff average of \(f\), and \(A_0 f = 0\). Then for every \(u : \alpha \to \mathbb{R}\), every \(n \in \mathbb{N}\) and every \(x \in \alpha\), writing \(|u|\) for the function \(y \mapsto |u(y)|\), we have \(|A_n u(x)| \le A_n |u|(x)\).

theorem norm_birkhoffAverage_le_birkhoffAverage_norm
    {u : α → ℝ} (n : ℕ) (x : α) :
    ‖birkhoffAverage ℝ T u n x‖ ≤ birkhoffAverage ℝ T (fun y => ‖u y‖) n x

Used by 2

Used byBirkhoff averages are \(L^1\)-contractions · Birkhoff averages of a bounded function are bounded

TheoremMonotonicity of Birkhoff averages#✓fully proved

Let \(T : \alpha \to \alpha\) be a map. For \(u : \alpha \to \mathbb{R}\), \(n \ge 1\) and \(x \in \alpha\), write \(A_n u(x) = \frac{1}{n} \sum_{k=0}^{n-1} u(T^k x)\) for the \(n\)-th Birkhoff average of \(u\) at \(x\), and \(A_0 u(x) = 0\). If \(u, v : \alpha \to \mathbb{R}\) satisfy \(u(y) \le v(y)\) for every \(y \in \alpha\), then \(A_n u(x) \le A_n v(x)\) for every \(n \in \mathbb{N}\) and every \(x \in \alpha\).

theorem birkhoffAverage_le_birkhoffAverage
    {u v : α → ℝ} (h : ∀ y, u y ≤ v y) (n : ℕ) (x : α) :
    birkhoffAverage ℝ T u n x ≤ birkhoffAverage ℝ T v n x

Used by 1

Used byBirkhoff averages of a bounded function are bounded

TheoremBirkhoff averages of a bounded function are bounded#✓fully proved

Let \(T : \alpha \to \alpha\) be a map, let \(M \ge 0\), and let \(g : \alpha \to \mathbb{R}\) satisfy \(|g(x)| \le M\) for every \(x \in \alpha\). Then for every \(n \in \mathbb{N}\) and every \(x \in \alpha\), the Birkhoff average \(\frac{1}{n} \sum_{k=0}^{n-1} g(T^k x)\) (taken to be \(0\) for \(n = 0\)) has absolute value at most \(M\).

theorem norm_birkhoffAverage_le_of_bounded
    {g : α → ℝ} {M : ℝ} (hM : 0 ≤ M) (hgb : ∀ x, ‖g x‖ ≤ M) (n : ℕ) (x : α) :
    ‖birkhoffAverage ℝ T g n x‖ ≤ M

Uses 2 · Used by 1

Proof usesMonotonicity of Birkhoff averages · Triangle inequality for Birkhoff averages

Used byBirkhoff's ergodic theorem in \(L^1\) for bounded functions

TheoremBirkhoff averages are \(L^1\)-contractions#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(T : \alpha \to \alpha\) preserve \(\mu\), and let \(g, h : \alpha \to \mathbb{R}\) be \(\mu\)-integrable. For a function \(f : \alpha \to \mathbb{R}\) and \(n \ge 1\) write \(A_n f(x) = \frac{1}{n} \sum_{k=0}^{n-1} f(T^k x)\), and \(A_0 f = 0\). Then for every \(n \in \mathbb{N}\), \(\int |A_n g(x) - A_n h(x)| \, d\mu(x) \le \int |g(x) - h(x)| \, d\mu(x)\).

theorem integral_norm_birkhoffAverage_sub_le
    (hmp : MeasurePreserving T μ μ) {g h : α → ℝ}
    (hg : Integrable g μ) (hh : Integrable h μ) (n : ℕ) :
    ∫ x, ‖birkhoffAverage ℝ T g n x - birkhoffAverage ℝ T h n x‖ ∂μ ≤
      ∫ x, ‖g x - h x‖ ∂μ

Uses 3 · Used by 1

Proof usesIntegrability of Birkhoff averages · Birkhoff averages preserve the integral · Triangle inequality for Birkhoff averages

Used byBirkhoff's ergodic theorem in \(L^1\) (ergodic case)

TheoremBirkhoff's ergodic theorem in \(L^1\) for bounded functions#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\alpha\), let \(T : \alpha \to \alpha\) be ergodic with respect to \(\mu\) (in particular \(T\) preserves \(\mu\)), let \(M \ge 0\), and let \(g : \alpha \to \mathbb{R}\) be \(\mu\)-integrable with \(|g(x)| \le M\) for every \(x \in \alpha\). For \(n \ge 1\) let \(A_n g(x) = \frac{1}{n} \sum_{k=0}^{n-1} g(T^k x)\). Then \(\int \left| A_n g(x) - \int g \, d\mu \right| d\mu(x) \to 0\) as \(n \to \infty\).

This follows from the almost-everywhere ergodic theorem and dominated convergence.

theorem tendsto_integral_norm_birkhoffAverage_of_bounded
    [IsProbabilityMeasure μ]
    (hT : Ergodic T μ) {g : α → ℝ} (hg : Integrable g μ)
    {M : ℝ} (hM : 0 ≤ M) (hgb : ∀ x, ‖g x‖ ≤ M) :
    Tendsto (fun n => ∫ x, ‖birkhoffAverage ℝ T g n x - ∫ y, g y ∂μ‖ ∂μ)
      atTop (𝓝 0)

Uses 3 · Used by 1

Proof usesBirkhoff pointwise ergodic theorem (ergodic case) · Integrability of Birkhoff averages · Birkhoff averages of a bounded function are bounded

Used byBirkhoff's ergodic theorem in \(L^1\) (ergodic case)

TheoremBirkhoff's ergodic theorem in \(L^1\) (ergodic case)#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\alpha\), let \(T : \alpha \to \alpha\) be ergodic with respect to \(\mu\) (in particular \(T\) preserves \(\mu\)), and let \(g : \alpha \to \mathbb{R}\) be \(\mu\)-integrable. For \(n \ge 1\) let \(A_n g(x) = \frac{1}{n} \sum_{k=0}^{n-1} g(T^k x)\) be the Birkhoff averages of \(g\). Then \(\int \left| A_n g(x) - \int g \, d\mu \right| d\mu(x) \to 0\) as \(n \to \infty\); that is, the Birkhoff averages of \(g\) converge to the constant \(\int g \, d\mu\) in \(L^1(\mu)\).

theorem birkhoff_ergodic_theorem_L1
    [IsProbabilityMeasure μ]
    (hT : Ergodic T μ) {g : α → ℝ} (hg : Integrable g μ) :
    Tendsto (fun n => ∫ x, ‖birkhoffAverage ℝ T g n x - ∫ y, g y ∂μ‖ ∂μ)
      atTop (𝓝 0)

Uses 3

Proof usesIntegrability of Birkhoff averages · Birkhoff averages are \(L^1\)-contractions · Birkhoff's ergodic theorem in \(L^1\) for bounded functions

DefinitionMaximal Birkhoff partial sum#✓fully proved

The maximal Birkhoff sum max_{1 ≤ n ≤ N} ∑_{k<n} f (T^[k] x) over the first N times.

noncomputable def maxPartialSum (T : α → α) (f : α → ℝ) (N : ℕ) (hN : 1 ≤ N) (x : α) : ℝ :=
  (Finset.Icc 1 N).sup' (by rw [Finset.nonempty_Icc]; exact hN)
    (fun n => birkhoffSum T f n x)

Used by 2

Used byMaximal ergodic theorem · Maximal ergodic inequality on an invariant set

TheoremMaximal ergodic theorem#✓fully proved

Maximal ergodic theorem (E. Hopf, 1954), in the finite form of A. M. Garsia, A simple proof of E. Hopf's maximal ergodic theorem, 1965: for measure-preserving T and integrable f, the integral of f over {max_{1 ≤ n ≤ N} S_n f > 0} is nonnegative. See also MathlibExt.Dynamics.Ergodic.BirkhoffWanted.maximal_ergodic, the limiting form for measurable f.

theorem garsia_maximal_inequality (hT : MeasurePreserving T μ μ) (hf : Integrable f μ)
    {N : ℕ} (hN : 1 ≤ N) :
    0 ≤ ∫ x in {x | 0 < maxPartialSum T f N hN x}, f x ∂μ

Uses 3 · Used by 1

Statement usesMaximal Birkhoff partial sum

Proof usesIntegrability of Birkhoff sums · Integral is invariant under a measure-preserving map

Used byMaximal ergodic inequality on an invariant set

DefinitionInvariant set of a map#✓fully proved

E is invariant under T: x ∈ E ↔ T x ∈ E, i.e. T ⁻¹' E = E (see isInvariantSet_iff_preimage_eq).

def IsInvariantSet (T : α → α) (E : Set α) : Prop := ∀ x, x ∈ E ↔ T x ∈ E

Used by 8

Used byBirkhoff limit is a conditional expectation on invariant sets · Invariant set as a set equal to its preimage · Invariant set is invariant under every iterate · Oscillation set of Birkhoff averages is null · Birkhoff limit preserves integrals over invariant sets · Maximal ergodic inequality on an invariant set · Birkhoff averages converge almost everywhere to the Birkhoff limit · Integral of the Kingman limit is at most the time constant

TheoremInvariant set as a set equal to its preimage#✓fully proved

IsInvariantSet T E is the condition T ⁻¹' E = E used by Mathlib's PreErgodic and MeasurableSpace.invariants.

theorem isInvariantSet_iff_preimage_eq {E : Set α} : IsInvariantSet T E ↔ T ⁻¹' E = E

Uses 1

Statement usesInvariant set of a map

TheoremInvariant set is invariant under every iterate#✓fully proved

An invariant set is invariant under every iterate.

theorem IsInvariantSet.iterate {E : Set α} (hE : IsInvariantSet T E) (k : ℕ) (x : α) :
    x ∈ E ↔ T^[k] x ∈ E

Uses 1 · Used by 1

Statement usesInvariant set of a map

Used byMaximal ergodic inequality on an invariant set

DefinitionUpper limit of Birkhoff averages#✓fully proved

The upper limit limsup_n A_n f x of the Birkhoff averages, in EReal.

noncomputable def fStar (T : α → α) (f : α → ℝ) (x : α) : EReal :=
  limsup (fun n => ((birkhoffAverage ℝ T f n x : ℝ) : EReal)) atTop

Used by 8

Used byBirkhoff limit of a function · Birkhoff limit is a conditional expectation on invariant sets · Upper limit of Birkhoff averages is invariant · Integrability of the Birkhoff limit · Oscillation set of Birkhoff averages · Oscillation set of Birkhoff averages is null · Birkhoff limit preserves integrals over invariant sets · Birkhoff averages converge almost everywhere to the Birkhoff limit

DefinitionLower limit of Birkhoff averages#✓fully proved

The lower limit liminf_n A_n f x of the Birkhoff averages, in EReal.

noncomputable def fStarLow (T : α → α) (f : α → ℝ) (x : α) : EReal :=
  liminf (fun n => ((birkhoffAverage ℝ T f n x : ℝ) : EReal)) atTop

Used by 4

Used byOscillation set of Birkhoff averages · Oscillation set of Birkhoff averages is null · Birkhoff limit preserves integrals over invariant sets · Birkhoff averages converge almost everywhere to the Birkhoff limit

TheoremUpper limit of Birkhoff averages is invariant#✓fully proved

The upper limit of the Birkhoff averages is T-invariant.

theorem fStar_comp (x : α) : fStar T f (T x) = fStar T f x

Uses 1 · Used by 4

Statement usesUpper limit of Birkhoff averages

Used byBirkhoff limit is a conditional expectation on invariant sets · Oscillation set of Birkhoff averages is null · Birkhoff limit preserves integrals over invariant sets · Birkhoff averages converge almost everywhere to the Birkhoff limit

TheoremMaximal ergodic inequality on an invariant set#✓fully proved

The maximal inequality on an invariant set: if every point of the invariant set E has some positive Birkhoff sum of g, then ∫_E g dμ ≥ 0.

theorem setIntegral_nonneg_of_invariant (hT : MeasurePreserving T μ μ) {g : α → ℝ}
    (hg : Integrable g μ) {E : Set α} (hEmeas : NullMeasurableSet E μ) (hEinv : IsInvariantSet T E)
    (hpos : ∀ x ∈ E, ∃ n, 1 ≤ n ∧ 0 < birkhoffSum T g n x) :
    0 ≤ ∫ x in E, g x ∂μ

Uses 5 · Used by 3

Statement usesInvariant set of a map

Proof usesIntegrability of Birkhoff sums · Invariant set is invariant under every iterate · Maximal ergodic theorem · Maximal Birkhoff partial sum

Used byOscillation set of Birkhoff averages is null · Birkhoff limit preserves integrals over invariant sets · Birkhoff averages converge almost everywhere to the Birkhoff limit

DefinitionOscillation set of Birkhoff averages#✓fully proved

The invariant set {f_* < a} ∩ {b < f*} where the Birkhoff averages oscillate across [a, b].

def levelSet (T : α → α) (f : α → ℝ) (a b : ℝ) : Set α :=
  {x | fStarLow T f x < (a : EReal) ∧ (b : EReal) < fStar T f x}

Uses 2 · Used by 2

Statement usesUpper limit of Birkhoff averages · Lower limit of Birkhoff averages

Used byOscillation set of Birkhoff averages is null · Birkhoff averages converge almost everywhere to the Birkhoff limit

TheoremOscillation set of Birkhoff averages is null#✓fully proved

For a < b the oscillation set levelSet T f a b is null.

theorem measure_levelSet_eq_zero (hT : MeasurePreserving T μ μ) (hf : Integrable f μ)
    {a b : ℝ} (hab : a < b) : μ (levelSet T f a b) = 0

Uses 7 · Used by 1

Statement usesOscillation set of Birkhoff averages

Proof usesIntegrability of Birkhoff averages · Invariant set of a map · Upper limit of Birkhoff averages · Lower limit of Birkhoff averages · Upper limit of Birkhoff averages is invariant · Maximal ergodic inequality on an invariant set

Used byBirkhoff averages converge almost everywhere to the Birkhoff limit

DefinitionBirkhoff limit of a function#✓fully proved

The limit of the Birkhoff averages of f (defined as f* cast to ℝ; it is the limit almost everywhere by tendsto_birkhoffAverage_ae).

noncomputable def birkhoffLimit (T : α → α) (f : α → ℝ) (x : α) : ℝ := (fStar T f x).toReal

Uses 1 · Used by 12

Statement usesUpper limit of Birkhoff averages

Used byBirkhoff limit is a conditional expectation on invariant sets · Birkhoff limit of an ergodic map is the space average · Integrability of the Birkhoff limit · Birkhoff limit preserves integrals over invariant sets · Birkhoff averages converge almost everywhere to the Birkhoff limit · Birkhoff's pointwise ergodic theorem · Kingman's theorem: normalized cocycle converges almost everywhere · Upper limit of a cocycle bounded by Birkhoff limits of blocks · Upper limit of a normalized cocycle is finite almost everywhere · Integrability of the Kingman limit for nonnegative cocycles · Integral of the Kingman limit is at most the time constant · Integrable function along an orbit divided by time tends to zero

TheoremBirkhoff averages converge almost everywhere to the Birkhoff limit#✓fully proved

The Birkhoff averages of an integrable f converge a.e. to birkhoffLimit T f.

theorem tendsto_birkhoffAverage_ae (hT : MeasurePreserving T μ μ) (hf : Integrable f μ) :
    ∀ᵐ x ∂μ, Tendsto (fun n => birkhoffAverage ℝ T f n x) atTop (𝓝 (birkhoffLimit T f x))

Uses 9 · Used by 7

Statement usesBirkhoff limit of a function

Proof usesIntegrability of Birkhoff averages · Invariant set of a map · Upper limit of Birkhoff averages · Lower limit of Birkhoff averages · Upper limit of Birkhoff averages is invariant · Oscillation set of Birkhoff averages · Oscillation set of Birkhoff averages is null · Maximal ergodic inequality on an invariant set

Used byBirkhoff limit of an ergodic map is the space average · Integrability of the Birkhoff limit · Birkhoff limit preserves integrals over invariant sets · Birkhoff's pointwise ergodic theorem · Kingman's theorem: normalized cocycle converges almost everywhere · Upper limit of a cocycle bounded by Birkhoff limits of blocks · Integrable function along an orbit divided by time tends to zero

TheoremBirkhoff averages are L1 contractions#✓fully proved

Birkhoff averages are L¹-contractions. See also MathlibExt.Probability.BirkhoffErgodicL1.integral_norm_birkhoffAverage_sub_le, the same bound for differences, stated with integrals of norms.

theorem eLpNorm_birkhoffAverage_le (hT : MeasurePreserving T μ μ) (hf : Integrable f μ) (n : ℕ) :
    eLpNorm (fun x => birkhoffAverage ℝ T f n x) 1 μ ≤ eLpNorm f 1 μ

Used by 1

Used byIntegrability of the Birkhoff limit

TheoremIntegrability of the Birkhoff limit#✓fully proved

The Birkhoff limit of an integrable function is integrable.

theorem integrable_birkhoffLimit (hT : MeasurePreserving T μ μ) (hf : Integrable f μ) :
    Integrable (birkhoffLimit T f) μ

Uses 5 · Used by 4

Statement usesBirkhoff limit of a function

Proof usesIntegrability of Birkhoff averages · Birkhoff averages are L1 contractions · Upper limit of Birkhoff averages · Birkhoff averages converge almost everywhere to the Birkhoff limit

Used byBirkhoff limit is a conditional expectation on invariant sets · Birkhoff limit preserves integrals over invariant sets · Integrability of the Kingman limit for nonnegative cocycles · Integral of the Kingman limit is at most the time constant

TheoremBirkhoff limit preserves integrals over invariant sets#✓fully proved

On every measurable invariant set E, ∫_E birkhoffLimit T f dμ = ∫_E f dμ.

theorem setIntegral_birkhoffLimit (hT : MeasurePreserving T μ μ) (hf : Integrable f μ) {E : Set α}
    (hEmeas : MeasurableSet E) (hEinv : IsInvariantSet T E) :
    ∫ x in E, f x ∂μ = ∫ x in E, birkhoffLimit T f x ∂μ

Uses 9 · Used by 2

Statement usesInvariant set of a map · Birkhoff limit of a function

Proof usesIntegrability of Birkhoff averages · Upper limit of Birkhoff averages · Lower limit of Birkhoff averages · Upper limit of Birkhoff averages is invariant · Integrability of the Birkhoff limit · Maximal ergodic inequality on an invariant set · Birkhoff averages converge almost everywhere to the Birkhoff limit

Used byBirkhoff limit is a conditional expectation on invariant sets · Integral of the Kingman limit is at most the time constant

TheoremBirkhoff limit is a conditional expectation on invariant sets#✓fully proved

The Birkhoff limit is the conditional expectation of f given the invariant σ-algebra.

theorem birkhoffLimit_ae_eq_condExp (hT : MeasurePreserving T μ μ) (hf : Integrable f μ) :
    birkhoffLimit T f =ᵐ[μ] μ[f | MeasurableSpace.invariants T]

Uses 6 · Used by 1

Statement usesBirkhoff limit of a function

Proof usesInvariant set of a map · Upper limit of Birkhoff averages · Upper limit of Birkhoff averages is invariant · Integrability of the Birkhoff limit · Birkhoff limit preserves integrals over invariant sets

Used byBirkhoff's pointwise ergodic theorem

TheoremBirkhoff's pointwise ergodic theorem#✓fully proved

Birkhoff's pointwise ergodic theorem (G. D. Birkhoff, Proof of the ergodic theorem, 1931): for T preserving a finite measure μ and integrable f, the averages (1/n) ∑_{k<n} f ∘ T^k converge μ-a.e. to μ[f | MeasurableSpace.invariants T]. See also MathlibExt.Dynamics.Ergodic.BirkhoffWanted.birkhoff_pointwise_ergodic, the ergodic case, and birkhoffLimit_ae_eq_integral_of_ergodic.

theorem tendsto_birkhoffAverage_condExp_ae (hT : MeasurePreserving T μ μ) (hf : Integrable f μ) :
    ∀ᵐ x ∂μ, Tendsto (fun n => birkhoffAverage ℝ T f n x) atTop
      (𝓝 ((μ[f | MeasurableSpace.invariants T]) x))

Uses 3

Proof usesBirkhoff limit of a function · Birkhoff limit is a conditional expectation on invariant sets · Birkhoff averages converge almost everywhere to the Birkhoff limit

TheoremBirkhoff limit of an ergodic map is the space average#✓fully proved

For ergodic T on a probability space the Birkhoff limit is the constant ∫ f dμ; this is MathlibExt.Dynamics.Ergodic.BirkhoffWanted.birkhoff_pointwise_ergodic combined with tendsto_birkhoffAverage_ae.

theorem birkhoffLimit_ae_eq_integral_of_ergodic [IsProbabilityMeasure μ] (hT : Ergodic T μ)
    (hf : Integrable f μ) : ∀ᵐ x ∂μ, birkhoffLimit T f x = ∫ y, f y ∂μ

Uses 3

Statement usesBirkhoff limit of a function

Proof usesBirkhoff pointwise ergodic theorem (ergodic case) · Birkhoff averages converge almost everywhere to the Birkhoff limit

38 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.