Birkhoff time average with n + 1 terms.

birkhoffAverageReal T f n ω := (∑_{i=0}^{n} f (T^[i] ω)) / (n + 1).

The n + 1 denominator side-steps the n = 0 division issue; this is the sequence we want to converge to ∫ f dμ under Birkhoff's theorem.

Partial Birkhoff sum with k terms. birkhoffPartialSum T f k ω := ∑_{i=0}^{k-1} f (T^[i] ω).

Average and partial sum are related: A_n = S_{n+1} / (n + 1).

Partial sums are measurable when T and f are.

Running maximum of Birkhoff partial sums: maxPartialSum T f n ω = max{S_0(ω), S_1(ω), …, S_n(ω)}.

Since S_0 = 0, this satisfies maxPartialSum T f n ω ≥ 0.

Each term f ∘ T^[i] has the same integral as f.

Integral of the (n+1)-term Birkhoff average equals ∫ f.

Recursion S_{k+1}(ω) = f(ω) + S_k(T ω).

Algebraic recursion for time averages: A_n(T ω) = ((n+2) · A_{n+1}(ω) - f(ω)) / (n+1).

Bound M_n ≤ ∑_{i < n} |f ∘ T^[i]|, used for integrability.

M_n is integrable when f is, in finite measure.

Existence of an index k ∈ {1, …, n} achieving the running max when the max is strictly positive.

The Garsia pointwise inequality (key step for the maximal ergodic inequality): for all ω : Ω,

M_n(ω) - M_n(T ω) ≤ 1_{M_n > 0}(ω) · f(ω).

Proof: on {M_n > 0}, picking k* ∈ {1, …, n} with S_{k*}(ω) = M_n(ω) and using S_{k*}(ω) = f(ω) + S_{k* - 1}(T ω) with S_{k* - 1}(T ω) ≤ M_n(T ω) gives f(ω) ≥ M_n(ω) - M_n(T ω). On {M_n = 0} (the complement), M_n(ω) - M_n(T ω) = -M_n(T ω) ≤ 0.

The maximal ergodic inequality (Garsia 1965). For T : Ω → Ω measure-preserving on a probability/finite-measure space and f : Ω → ℝ integrable, for every n : ℕ,

∫_{ω : 0 < maxPartialSum T f n ω} f dμ ≥ 0.

For ergodic T and integrable g with ∫g dμ < 0, the "infinitely often positive partial sum" set {ω | ∀ n, ∃ N ≥ n, S_N(g, ω) > 0} cannot have full measure.

Proof: that set is contained in B := ⋃_n {ω | maxPartialSum T g n ω > 0} (= {ω | ∃ N ≥ 1, S_N(g, ω) > 0}). By the maximal ergodic inequality, ∫_{M_n > 0} g dμ ≥ 0 for each n. By dominated convergence, ∫_B g dμ = lim_n ∫_{M_n > 0} g dμ ≥ 0. If the "infinitely often" set has full measure, so does B, hence ∫_B g dμ = ∫_Ω g dμ < 0. Contradiction.

(Ergodicity is not actually needed here; the contradiction is direct from the maximal ergodic inequality + DCT.)

The Hardy bound (finite n): for any m n : ℕ, m · μ({maxPartialSum T (g - m) n > 0}) ≤ ‖g‖₁.

The maximal ergodic inequality 0 ≤ ∫_E (g - m) rearranges to m · μ(E) ≤ ∫_E g ≤ ∫|g|, where E := {maxPartialSum (g - m) n > 0}. For m = 0 the bound is trivial.

The Hardy bound (union): the union of {maxPartialSum (g - m) n > 0} over n is bounded by ‖g‖₁ / m (in ENNReal).

A.e. boundedness of Birkhoff averages (Hardy-Littlewood-style). For T measure-preserving and g integrable, the sequence n ↦ birkhoffAverageReal T g n ω has bounded range a.e.

Proof: combine maxPartialSum_meas_iUnion_le (Hardy union bound) with the inclusion {¬BddAbove range A_·} ⊆ ⋂_m ⋃_n {maxPartialSum (g-m) n > 0} (positive Birkhoff sum from A_k > m) and exists_nat_gt (Archimedean choice of m large to push ‖g‖₁/m < ε).

The Birkhoff-average limsup is T-invariant (a.e.). For measure preserving T and integrable f, the function limsupAvg ω := limsup_n A_n(f, ω) satisfies limsupAvg ∘ T =ᵐ limsupAvg.

Proof: from birkhoffAverageReal_ae_bddAbove applied to f and to -f, a.e. the sequence A_n(f, ω) is bounded. The recursion A_n(f, Tω) - A_{n+1}(f, ω) = (A_{n+1}(f, ω) - f(ω))/(n+1) then gives A_n(f, Tω) - A_{n+1}(f, ω) → 0 (bounded numerator / n+1). Combining with Filter.limsup_nat_add shifts back to limsup A_n(f, Tω) = limsup A_n(f, ω).

Measurability of ω ↦ limsup A_n(f, ω) (as a real-valued function; when the sequence is unbounded the value is the Real.limsup junk value but the function remains measurable).

For ergodic T and integrable g with ∫g dμ < 0, the limsup of Birkhoff averages of g is ≤ 0 a.e.

Proof: by T-invariance (birkhoffAverageReal_limsup_comp_T_ae) and ergodicity (Ergodic.ae_eq_const_of_ae_eq_comp_ae), lsa =ᵐ const c for some c : ℝ. We show c ≤ 0 by contradiction: if c > 0, then a.e. ∃ᶠ n, A_n(g, ω) > c/2 > 0 (from limsup = c), hence ∀ k, ∃ N ≥ k, S_N(g, ω) > 0 (with N := n + 1). This full-measure set violates birkhoff_neg_mean_sup_null.

The upper sandwich: for every ε > 0, a.e. ω, eventually birkhoffAverageReal T f n ω < ∫f dμ + ε.

The lower sandwich: for every ε > 0, a.e. ω, eventually ∫f dμ - ε < birkhoffAverageReal T f n ω.

Proof: apply the upper sandwich to -f and negate.

The Birkhoff individual ergodic theorem.

For a probability-preserving ergodic transformation T : Ω → Ω and an integrable observable f : Ω → ℝ, the Birkhoff time averages

A_n ω := (∑_{i=0}^{n} f (T^[i] ω)) / (n + 1)

converge almost everywhere to the spatial mean ∫ f dμ.