The maximal ergodic inequality (Hopf/Garsia)

For an integrable f and a measure-preserving T, on the set where some forward Birkhoff sum is positive the integral of f is nonnegative: 0 ≤ ∫_{ {x | ∃ n, 0 < birkhoffSum T f (n+1) x} } f dμ. This inequality is the analytic gateway to the pointwise (Birkhoff) ergodic theorem.

The proof follows Garsia's short combinatorial argument. We introduce the maximal function maxBirkhoff T g N x = max_{0 ≤ k ≤ N} birkhoffSum T g k x for a measurable representative g of f, establish the pointwise Garsia inequality maxBirkhoff … x - maxBirkhoff … (T x) ≤ g x on the set where the maximal function is positive, integrate it, pass to the limit N → ∞, and transfer back from g to f.

Main results

• Oseledets.maxBirkhoff: Garsia's maximal function maxBirkhoff T g N x = max_{0 ≤ k ≤ N} birkhoffSum T g k x.
• Oseledets.maxBirkhoff_le_add: Garsia's pointwise inequality maxBirkhoff T g N x ≤ g x + maxBirkhoff T g N (T x) on the set where the maximal function is positive.
• Oseledets.setIntegral_maxBirkhoff_pos_nonneg: Garsia's inequality at a fixed level N.
• Oseledets.setIntegral_birkhoffSum_pos_nonneg: the maximal ergodic inequality.

References

• A. M. Garsia, A simple proof of E. Hopf's maximal ergodic theorem, J. Math. Mech. 14 (1965), 381–382.

noncomputable def Oseledets.maxBirkhoff {X : Type u_1} (T : X → X) (g : X → ℝ) (N : ℕ) (x : X) : ℝ

Garsia's maximal function: maxBirkhoff T g N x = max_{0 ≤ k ≤ N} birkhoffSum T g k x. Because the k = 0 term equals birkhoffSum T g 0 x = 0, this quantity is always ≥ 0. The nonemptiness witness is the literal Finset.nonempty_range_add_one, matching Finset.measurable_range_sup''.

Equations

• Oseledets.maxBirkhoff T g N x = (Finset.range (N + 1)).sup' ⋯ fun (k : ℕ) => birkhoffSum T g k x

theorem Oseledets.maxBirkhoff_nonneg {X : Type u_1} {T : X → X} (g : X → ℝ) (N : ℕ) (x : X) : 0 ≤ maxBirkhoff T g N x

The k = 0 term of maxBirkhoff is birkhoffSum T g 0 x = 0, so the maximal function is nonnegative everywhere.

theorem Oseledets.maxBirkhoff_succ {X : Type u_1} {T : X → X} (g : X → ℝ) (N : ℕ) (x : X) : maxBirkhoff T g (N + 1) x = max (birkhoffSum T g (N + 1) x) (maxBirkhoff T g N x)

The recursion maxBirkhoff T g (N+1) x = birkhoffSum T g (N+1) x ⊔ maxBirkhoff T g N x, from range (N+2) = insert (N+1) (range (N+1)).

theorem Oseledets.measurable_birkhoffSum {X : Type u_1} [MeasurableSpace X] {T : X → X} (hT : Measurable T) {g : X → ℝ} (hg : Measurable g) (k : ℕ) : Measurable fun (x : X) => birkhoffSum T g k x

Each Birkhoff partial sum x ↦ birkhoffSum T g k x is measurable when g is measurable and T is measurable.

theorem Oseledets.measurable_maxBirkhoff {X : Type u_1} [MeasurableSpace X] {T : X → X} (hT : Measurable T) {g : X → ℝ} (hg : Measurable g) (N : ℕ) : Measurable (maxBirkhoff T g N)

The maximal function maxBirkhoff T g N is measurable when g and T are.

theorem Oseledets.integrable_birkhoffSum {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {g : X → ℝ} (hg : MeasureTheory.Integrable g μ) (k : ℕ) : MeasureTheory.Integrable (fun (x : X) => birkhoffSum T g k x) μ

Each Birkhoff partial sum x ↦ birkhoffSum T g k x is integrable when g is integrable and T is measure-preserving.

theorem Oseledets.integrable_maxBirkhoff {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {g : X → ℝ} (hg : MeasureTheory.Integrable g μ) (N : ℕ) : MeasureTheory.Integrable (maxBirkhoff T g N) μ

The maximal function maxBirkhoff T g N is integrable when g is integrable and T is measure-preserving.

theorem Oseledets.add_sup'_eq {ι : Type u_2} (s : Finset ι) (H : s.Nonempty) (c : ℝ) (f : ι → ℝ) : c + s.sup' H f = s.sup' H fun (b : ι) => c + f b

A real constant can be pulled inside a nonempty Finset.sup': c + s.sup' H f = s.sup' H (fun b => c + f b). (Mathlib has no Finset.sup'_add, so we prove it directly by le_antisymm.)

theorem Oseledets.maxBirkhoff_le_add {X : Type u_1} {T : X → X} (g : X → ℝ) (N : ℕ) (x : X) (hx : 0 < maxBirkhoff T g N x) : maxBirkhoff T g N x ≤ g x + maxBirkhoff T g N (T x)

Garsia's pointwise inequality. On the set where maxBirkhoff T g N is positive, maxBirkhoff T g N x ≤ g x + maxBirkhoff T g N (T x).

Key identity: pulling the constant g x through the sup' and applying birkhoffSum_succ' shows g x + maxBirkhoff T g N (T x) is the maximum of the shifted partial sums birkhoffSum T g (k+1) x over k ≤ N. Since the maximum defining maxBirkhoff T g N x is positive it is attained at some index k₀ ≥ 1 (the index 0 gives birkhoffSum T g 0 x = 0), and birkhoffSum T g k₀ x is one of the shifted sums, hence ≤ the shifted maximum.

theorem Oseledets.birkhoffSum_congr_ae {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {f g : X → ℝ} (hfg : f =ᵐ[μ] g) (n : ℕ) : (fun (x : X) => birkhoffSum T f n x) =ᵐ[μ] fun (x : X) => birkhoffSum T g n x

If f =ᵐ[μ] g and T is measure-preserving, then the Birkhoff sums agree a.e.: birkhoffSum T f n =ᵐ[μ] birkhoffSum T g n. Each summand f ∘ T^[k] =ᵐ[μ] g ∘ T^[k] because T^[k] is measure-preserving, and a finite a.e.-equal sum is a.e.-equal.

theorem Oseledets.setIntegral_maxBirkhoff_pos_nonneg {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {g : X → ℝ} (hg : MeasureTheory.Integrable g μ) (hgm : Measurable g) (N : ℕ) : 0 ≤ ∫ (x : X) in {x : X | 0 < maxBirkhoff T g N x}, g x ∂μ

Garsia's inequality for a fixed level N. For a measurable integrable g, the integral of g over the set {x | 0 < maxBirkhoff T g N x} is nonnegative.

This is the heart of the maximal ergodic inequality. We integrate the pointwise Garsia inequality maxBirkhoff T g N x - maxBirkhoff T g N (T x) ≤ g x over the level set E N, then use measure-preservation (∫ maxBirkhoff∘T = ∫ maxBirkhoff) and the fact that maxBirkhoff vanishes off E N to cancel the two maximal-function integrals.

theorem Oseledets.monotone_setOf_maxBirkhoff_pos {X : Type u_1} {T : X → X} (g : X → ℝ) : Monotone fun (N : ℕ) => {x : X | 0 < maxBirkhoff T g N x}

The level sets {x | 0 < maxBirkhoff T g N x} are monotone in N, because maxBirkhoff T g N is monotone in N (the sup' is over a larger range).

theorem Oseledets.iUnion_setOf_maxBirkhoff_pos {X : Type u_1} {T : X → X} (g : X → ℝ) : ⋃ (N : ℕ), {x : X | 0 < maxBirkhoff T g N x} = {x : X | ∃ (n : ℕ), 0 < birkhoffSum T g (n + 1) x}

The union of the level sets {x | 0 < maxBirkhoff T g N x} over all N is exactly the target set {x | ∃ n, 0 < birkhoffSum T g (n+1) x}.

theorem Oseledets.setIntegral_birkhoffSum_pos_nonneg_of_measurable {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {g : X → ℝ} (hg : MeasureTheory.Integrable g μ) (hgm : Measurable g) : 0 ≤ ∫ (x : X) in {x : X | ∃ (n : ℕ), 0 < birkhoffSum T g (n + 1) x}, g x ∂μ

Maximal ergodic inequality, measurable version. For a measurable integrable g and measure-preserving T, the integral of g over the set where some forward Birkhoff partial sum is positive is nonnegative. The general (only a.e. measurable) case is obtained by passing to a measurable representative.

theorem Oseledets.setIntegral_birkhoffSum_pos_nonneg {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {f : X → ℝ} (hf : MeasureTheory.Integrable f μ) : 0 ≤ ∫ (x : X) in {x : X | ∃ (n : ℕ), 0 < birkhoffSum T f (n + 1) x}, f x ∂μ

Maximal ergodic inequality (Hopf/Garsia). For a measure-preserving T and an integrable f, the integral of f over the set where some forward Birkhoff partial sum is positive is nonnegative.

The proof reduces to the measurable case setIntegral_birkhoffSum_pos_nonneg_of_measurable by passing to the measurable representative g = hf.1.mk f and transferring both the target set (the two sets agree a.e. since the Birkhoff sums agree a.e.) and the integrand (f =ᵐ[μ] g).