Bourgain's polynomial ergodic theorem

bourgain_polynomial_ergodic

Submitter: Kim Morrison.

Notes: For a measure-preserving system on a probability space, every integer-polynomial iterate sequence a, and every f ∈ L^p with p > 1, the polynomial ergodic averages (1/n) ∑_{k<n} f(T^[a k] x) converge pointwise almost everywhere. Trusted helpers (IsIntegerPolynomialSequence, polynomialErgodicAverage) are non-holes. Mathlib has Birkhoff's pointwise ergodic theorem but not Bourgain's polynomial extension. Candidate from §173 of the Knill survey.

Source: J. Bourgain, *Pointwise ergodic theorems for arithmetic sets*, Publ. Math. IHÉS 69 (1989). Knill, *Some fundamental theorems in mathematics*, §173.

Informal solution: Reduce, via a transfer/Calderón principle, to a maximal inequality for the discrete polynomial averaging operators on ℤ. Bourgain's proof establishes the L^p (p > 1) bound for the associated maximal function using circle-method / Hardy–Littlewood estimates: split the Fourier multiplier into major arcs (where it is approximated by a continuous averaging multiplier controlled by the Dunford–Schwartz/Wiener maximal theorem) and minor arcs (controlled by Weyl-type exponential sum bounds and a variational/oscillation argument). The maximal inequality, together with pointwise convergence on a dense subclass (e.g. eigenfunctions / bounded functions), yields a.e. convergence of the averages for all f ∈ L^p by the Banach principle. The limit F is the pointwise limit. Requires harmonic-analysis machinery absent from Mathlib.

theorem declaration uses `sorry`bourgain_polynomial_ergodic [IsProbabilityMeasure μ] {p : ℝ≥0∞} (hp : 1 < p) (hp_ne_top : p ≠ ∞)
    {T : X → X} (hT : MeasurePreserving T μ μ)
    {a : ℕ → ℕ} (ha : LeanEval.Dynamics.BourgainErgodic.IsIntegerPolynomialSequence a)
    {f : X → ℝ} (hf : MemLp f p μ) :
    ∃ F : X → ℝ,
      ∀ᵐ x ∂μ,
        Tendsto (fun n : ℕ => polynomialErgodicAverage a T f (n + 1) x) atTop (𝓝 (F x)) := byX:Type u_1inst✝¹:MeasurableSpace Xμ:Measure Xinst✝:IsProbabilityMeasure μp:ℝ≥0∞hp:1 < php_ne_top:p ≠ ∞T:X → XhT:MeasurePreserving T μ μa:ℕ → ℕha:IsIntegerPolynomialSequence af:X → ℝhf:MemLp f p μ⊢ ∃ F, ∀ᵐ (x : X) ∂μ, Tendsto (fun n => polynomialErgodicAverage a T f (n + 1) x) atTop (𝓝 (F x))
  sorryAll goals completed! 🐙

Solved by

Not yet solved.