Bourgain's polynomial ergodic theorem

DefinitionInteger polynomial sequences#✓fully proved

A sequence \(a : \mathbb{N} \to \mathbb{N}\) is an integer polynomial sequence if there is a polynomial \(P\) with integer coefficients such that \(P(n) \ge 0\) and \(a(n) = P(n)\) for every \(n \in \mathbb{N}\).

def IsIntegerPolynomialSequence (a : ℕ → ℕ) : Prop :=
  ∃ P : Polynomial ℤ,
    ∀ n : ℕ, 0 ≤ P.eval (n : ℤ) ∧ a n = Int.toNat (P.eval (n : ℤ))

Used by 1

Used byBourgain's polynomial ergodic theorem

DefinitionPolynomial ergodic averages#✓fully proved

Given a sequence \(a : \mathbb{N} \to \mathbb{N}\), a map \(T : X \to X\), a function \(f : X \to \mathbb{R}\), \(n \in \mathbb{N}\) and \(x \in X\), the \(n\)-th polynomial ergodic average of \(f\) at \(x\) is

\[\frac{1}{n} \sum_{k=0}^{n-1} f\bigl(T^{a(k)}(x)\bigr),\]

where \(T^{a(k)}\) is the \(a(k)\)-fold iterate of \(T\); for \(n = 0\) the average is \(0\).

noncomputable def polynomialErgodicAverage (a : ℕ → ℕ) (T : X → X) (f : X → ℝ)
    (n : ℕ) (x : X) : ℝ :=
  (n : ℝ)⁻¹ * ∑ k ∈ range n, f (T^[a k] x)

Used by 1

Used byBourgain's polynomial ergodic theorem

TheoremBourgain's polynomial ergodic theorem#●ready to prove

Let \((X, \mu)\) be a probability space, let \(T : X \to X\) be a measure-preserving map, let \(a : \mathbb{N} \to \mathbb{N}\) be an integer polynomial sequence, and let \(f : X \to \mathbb{R}\) be a function in \(L^p(\mu)\) for some \(p\) with \(1 < p < \infty\). Then there is a function \(F : X \to \mathbb{R}\) such that for \(\mu\)-almost every \(x \in X\) the polynomial ergodic averages \(\frac{1}{n} \sum_{k=0}^{n-1} f(T^{a(k)}(x))\), \(n \ge 1\), where \(T^{a(k)}\) is the \(a(k)\)-fold iterate of \(T\), converge to \(F(x)\) as \(n \to \infty\).

public theorem_wanted bourgain_polynomial_ergodic
    [IsProbabilityMeasure μ] {p : ℝ≥0∞} (hp : 1 < p) (hp_ne_top : p ≠ ∞)
    {T : X → X} (hT : MeasurePreserving T μ μ)
    {a : ℕ → ℕ} (ha : IsIntegerPolynomialSequence a)
    {f : X → ℝ} (hf : MemLp f p μ) :
    ∃ F : X → ℝ,
      ∀ᵐ x ∂μ,
        Tendsto (fun n : ℕ => polynomialErgodicAverage a T f (n + 1) x) atTop (𝓝 (F x))

Sources

• J. Bourgain, Pointwise ergodic theorems for arithmetic sets, Publ. Math. IHÉS 69 (1989). Knill, Some fundamental theorems in mathematics, §173. Problem bourgain_polynomial_ergodic of the lean-eval benchmark.

Uses 2

Statement usesInteger polynomial sequences · Polynomial ergodic averages

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.