Finite Maximal Ergodic Inequalities: From Orbit Maxima to Threshold Events

Begin with four equally weighted states

Take the finite state space

with the uniform probability measure, so every state has mass \(1/4\). Let the transformation cycle through the states:

This map preserves the uniform measure because it only permutes four equal atoms. Define the real observable

Fix horizon \(N=4\). For each starting state \(x\), the finite Birkhoff sum \(S_k g(x)\) adds the first \(k\) values seen from \(x\). The empty sum \(S_0g(x)\) is zero. The complete ledger is:

All four terminal sums are \(-1\). Looking only at time four would therefore miss every positive prefix. The running maximum remembers them, and the strict finite Hopf event is

State \(a\) is the instructive atom. Its first observable value is negative, yet its two-step sum is

The theorem does not say \(g(x)\) is pointwise nonnegative on the event.

See the pointwise inequality atom by atom

The proof’s finite pointwise statement is

For this cycle, no abstraction is needed:

The uniform integral is just the average of four atom values. The maximum differences cancel around the cycle:

The indicator side is

Thus the finite Hopf conclusion is visible before any general integration machinery:

Turn the same orbit into an average-threshold event

For positive \(k\), divide each partial sum by \(k\). The four average rows are:

At strict threshold \(a=1\),

The third average from \(d\) equals one and therefore does not qualify, but its first average is two, so \(d\) still has a strict witness. The exact integral chain is

Dividing by the positive threshold one gives the finite weak estimate \(\frac12\le\frac54\).

Two boundaries fix the theorem statements

First set the threshold to zero. The strict positive-average event is \(\{a,b,d\}\), with mass \(3/4\). The undivided theorem still gives a valid statement whose left side is zero. But a putative weak theorem without \(0\lt a\) would read

which is false under Lean’s total division. Threshold positivity is needed exactly when division occurs, not in the preceding multiplication estimate.

Now set the horizon to zero. Every partial-sum list is just \([0]\), and every maximum is zero. Therefore

If the event were defined nonstrictly by \(0\le M_0g\), all four states would qualify at time zero. In fact, because every finite maximum includes the zero sum, the nonstrict event is the whole space at every horizon. This is why the formal definition uses strict positivity.

Suppose a real observable is read along an orbit. At each finite time one can add everything seen so far, then ask whether any of those running totals is positive. That question remembers the whole finite prefix, not only its last sum. It is exactly the kind of pathwise selection that can look difficult to integrate: each starting point may choose a different winning time.

The finite maximal ergodic argument avoids integrating the chosen time. It packages all choices into one maximum. Strict positivity ensures that a maximizer occurs at a positive time. The first summand can then be peeled from that winning sum, leaving a partial sum along the shifted orbit. When the transformation preserves the measure, the original and shifted maxima have the same integral. Their difference cancels, and what remains is a nonnegative integral of the observable over the strict event.

Random-matrix-theory milestone 23 (RMT-23) formalizes this finite mechanism in Lean. The compact concept page is finite maximal ergodic inequality . The declaration-complete implementation account is The Finite Hopf Maximal Ergodic Lemma in Lean. The immediate conceptual predecessor is Birkhoff Convergence Events Before the Pointwise Ergodic Theorem.

Choose a route up

Learning objectives

By the summit, a reader should be able to:

1. state the exact zero-based convention for a finite Birkhoff sum;
2. distinguish a running maximum from the positive part of a terminal sum;
3. explain why including time zero makes the maximum nonnegative;
4. explain why a nonstrict event would be the entire state space;
5. rewrite strict-event membership as a positive-time witness;
6. derive the horizon-zero and horizon-one boundaries;
7. prove that finite maxima increase with the horizon;
8. derive ordinary measurability of a finite maximum;
9. derive integrability of a finite maximum under preservation;
10. distinguish ordinary measurability from almost-everywhere strong measurability;
11. choose a maximizing index without making it a measurable function;
12. prove that a positive maximizing index cannot be zero;
13. peel the first observable value from a successor Birkhoff sum;
14. compare the remainder with the shifted running maximum;
15. handle the complement of the strict event without a maximizing witness;
16. combine the two pointwise branches with an indicator;
17. explain precisely where measure preservation enters;
18. derive the cancellation of the two maximal-function integrals;
19. state the finite Hopf-style integral inequality;
20. explain why no finite-measure or probability premise is needed there;
21. explain why neither injectivity nor invertibility is needed;
22. encode an average-threshold event using \(g-a\);
23. prove the centered-sum identity and membership equivalence;
24. locate the exact reason a finite-measure premise appears for centering;
25. derive the threshold integral lower bound for every real \(a\);
26. replace \(g\) by its positive part on the right side;
27. identify why \(a\gt0\) is needed only for division;
28. distinguish a finite-horizon estimate from an infinite maximal theorem;
29. describe the contributions and limits of the four historical sources;
30. map all twenty-five public declarations to their proof layers;
31. interpret all eleven compiled boundary probes; and
32. state the exact remaining work toward a pointwise ergodic theorem.

Common setup and notation

Let:

• \(\Omega\) be a type equipped with a measurable space;
• \(\mu\) be a measure on \(\Omega\);
• \(T:\Omega\to\Omega\) be a discrete-time transformation;
• \(T^j\) be the \(j\)-fold iterate of \(T\);
• \(g:\Omega\to\mathbb R\) be a real observable;
• \(N\in\mathbb N\) be a fixed finite horizon;
• \(k\in\mathbb N\) be a candidate time; and
• \(\omega\in\Omega\) be a starting point.

Write

for the finite Birkhoff sum. Write

for the running maximum through time \(N\), and

for its strict positivity event.

When a threshold \(a\in\mathbb R\) is present, write

and

The restriction \(k\ge1\) matters because the average at time zero is totalized in Lean but division is only order-reflecting at a positive denominator.

Start with finite orbit sums

Mathlib’s finite Birkhoff sum uses Finset.range k. That range contains the natural numbers strictly below \(k\). Consequently,

Two successor identities are useful, and they peel opposite ends:

The maximal proof uses the second identity. It removes the first orbit value and leaves the same observable along the orbit starting at \(T\omega\).

The finite maximum is encoded with a nonempty finite supremum:

def finiteBirkhoffSumMax (T : Ω → Ω) (g : Ω → ℝ) (N : ℕ) : Ω → ℝ :=
  fun ω ↦
    (Finset.range (N + 1)).sup' Finset.nonempty_range_add_one
      (fun k ↦ birkhoffSum T g k ω)

The range \(N+1\) contains exactly \(0,\ldots,N\). The proof object Finset.nonempty_range_add_one certifies that sup’ really has an element to maximize. This avoids inventing a default maximum outside the mathematical index set.

Every candidate sum lies below the maximum:

If \(M\le N\), every index available at horizon \(M\) remains available at horizon \(N\). Hence

This is monotonicity in the horizon, not monotonicity of the individual partial sums. The sequence \(S_kg(\omega)\) may rise and fall.

Put time zero inside the maximum

Since \(S_0g(\omega)=0\) and zero is one of the maximized values,

for every map, observable, horizon, and point. No measurable structure is needed.

At horizon zero there is only one candidate:

These two small facts determine the event convention. If one defined

then \(F_N(g)=\Omega\) for every \(g\). It would remember nothing about the positive-time orbit. The strict event

removes that degeneracy.

The exact membership theorem is

For the forward direction, strict positivity of a finite supremum supplies an index with positive value. That index cannot be zero because \(S_0=0\). For the reverse direction, any positive candidate is bounded above by the maximum, so the maximum is positive.

Two boundaries follow:

The event also increases with its horizon. A positive witness available by time \(M\) remains available by time \(N\) whenever \(M\le N\).

Measurability and integrability are different gates

The finite maximum has both an ordinary-measurability route and an integrability route. They should not be collapsed.

Ordinary measurability

Assume \(T\) and \(g\) are measurable. Every finite iterate \(T^j\) is measurable, every composition \(g\circ T^j\) is measurable, and every finite Birkhoff sum is measurable. A finite supremum of measurable real functions is measurable through Mathlib’s finite lattice API. Therefore

is measurable, and the strict superlevel comparison

is a measurable set.

This route mentions no measure. It cannot require preservation, probability, integrability, or ergodicity.

Integrability

Assume instead that \(T\) preserves \(\mu\) and \(g\) is integrable with respect to \(\mu\). Preservation propagates integrability along every finite iterate, so each \(g\circ T^j\) is integrable. Finite sums remain integrable. The maximum of two integrable real functions is integrable, and finite induction closes the whole maximum.

Thus

This theorem does not require \(\mu(\Omega)\lt\infty\). It does not require a probability measure. The integrability of \(g\) controls the finitely many orbit terms, while preservation keeps their integrals from changing under composition.

An integrable function in Mathlib is almost-everywhere strongly measurable. That does not assert ordinary measurability of the exact representative supplied by the caller. RMT-23 therefore derives NullMeasurableSet (finiteHopfEvent T g N) μ directly from the almost-everywhere measurability of the integrable maximum. This is exactly the set interface needed by indicator integrability and set integration. The almost everywhere entry explains the representative distinction.

Peel a positive maximizing index

Fix \(\omega\in E_N(g)\). Because the index set is finite and nonempty, some \(k\le N\) attains the maximum:

The maximum is positive, so \(S_kg(\omega)\gt0\). Time zero has sum zero, hence \(k\ne0\). There is a natural number \(j\) with \(k=j+1\).

Now apply the first-summand successor identity:

The last step is valid because \(j\le N\). In fact \(j\lt N\), but the weaker bound is enough to place \(S_jg(T\omega)\) among the terms maximized by \(M_Ng(T\omega)\).

Rearrange:

This is the on-event branch.

Now suppose \(\omega\notin E_N(g)\). The maximum is nonnegative everywhere, yet it is not positive here. Therefore

The shifted maximum remains nonnegative, so

This is the off-event branch. It needs no selected maximizer.

Combining them gives the global pointwise inequality

This proof architecture is close to Garsia’s concise 1965 presentation, but the Lean theorem fixes its exact finite range and strict event explicitly. The running maximum is not the positive part of the terminal sum. A terminal sum can be negative even though an earlier partial sum was positive.

Preservation performs the cancellation

The pointwise inequality becomes useful only after all terms are known to be integrable. Let

The integrability theorem supplies \(M\in L^1(\mu)\). Measure preservation also gives \(M\circ T\in L^1(\mu)\). The null-measurable event theorem makes \(\mathbf1_Eg\) integrable.

Monotonicity of the integral applied to the pointwise inequality yields

The private helper integral_comp_of_measurePreserving proves

Its proof uses Mathlib’s integral_map and the equality of the pushforward measure with \(\mu\). Therefore the entire left side is zero:

The indicator integral is the set integral, so

This is integral_finiteHopfEvent_nonneg.

Why the assumptions are genuinely weak

The theorem needs:

• a measurable space on \(\Omega\), so measure theory is meaningful;
• a measure \(\mu\);
• MeasurePreserving T μ μ; and
• Integrable g μ.

It does not need:

• \(\mu(\Omega)\lt\infty\);
• probability normalization;
• a sigma-finite measure;
• ergodicity;
• injectivity;
• surjectivity;
• invertibility; or
• an ordinarily measurable raw representative for \(g\).

The bundled MeasurePreserving premise includes measurability of \(T\). The proof also uses its pushforward equality. It never asks for a preimage point or an inverse transformation.

The infinite counting-measure probe is especially instructive. On \(\mathbb N\) with counting measure, take the identity transformation and an integrable point mass. The total measure is infinite, but the theorem still applies. Finite measure appears only later when a nonzero constant threshold must itself be integrable.

Center by a threshold, not by an expectation

Fix \(a\in\mathbb R\) and define

This is threshold centering. It does not say that \(h\) has integral zero. Unless \(a\) has been chosen from a normalized expectation and the needed integral identity has been proved, “mean centered” would overstate the construction.

Finite sums respect subtraction:

For \(k\ge1\), multiplication or division by \(k\gt0\) preserves strict order:

Therefore

RMT-23 names this set finiteBirkhoffAverageExceedanceSet T g N a. It is a union over a finite range of positive horizons, encoded through one already developed strict maximal event.

The event increases with \(N\). Ordinary measurability follows from measurability of \(T\) and \(g\). Its null-measurable integrability route adds [IsFiniteMeasure μ] because the constant function \(\omega\mapsto a\) must be integrable before \(g-a\) can be fed to the finite Hopf lemma.

The threshold integral inequality

Assume now that \(\mu\) is finite, \(T\) preserves \(\mu\), and \(g\) is integrable. Apply the core lemma to \(h=g-a\) and \(E=E_{N,a}(g)\):

Set-integral subtraction and integration of a constant over a set give

Thus

The notation \(\mu_{\mathbb R}\) is Mathlib’s finite real-valued measure projection. The displayed inequality is valid for every \(a\in\mathbb R\), including zero and negative thresholds.

The sign must remain explicit: the argument has not divided by \(a\), so it does not require a sign assumption on \(a\). For negative \(a\), the left side is nonpositive because the event measure is nonnegative. The result remains correct even when it is not a useful upper bound on the event’s size.

Remove the event from the right side

Define the positive part

Pointwise, \(g\le g^+\). Therefore

Since \(g^+\ge0\), restricting its integral to a set cannot exceed its integral over the whole space:

Combining these inequalities gives the horizon-uniform bound

The right side depends on \(g\) and \(\mu\), but not on \(N\). This uniformity is what makes the finite statement useful in a future monotone limiting argument.

The notation \(g^+\) here really is a pointwise positive part. This should not be confused with Garsia’s historical notation \(S_n^+\), which denotes a running maximum of several partial sums in the cited proof.

Divide only after proving positivity

If \(a\gt0\), division preserves the inequality:

This is a weak finite maximal estimate. The phrase weak refers to control of the measure of a threshold event rather than pointwise control of every average.

The proof signature makes the timing exact:

• finiteBirkhoffAverageExceedanceSet_integral_lower_bound accepts any real \(a\);
• finiteBirkhoffAverageExceedanceSet_posPart_bound also accepts any real \(a\); and
• measureReal_finiteBirkhoffAverageExceedanceSet_le alone takes ha : 0 < a.

At \(a=0\), the division theorem would be meaningless. At \(a\lt0\), dividing would reverse order. The earlier integral inequalities remain valid because they do neither operation.

Seven bridges from the orbit ledger to Lean

The first four bridges build the finite Hopf inequality. The last three turn it into a threshold-event estimate. Each Lean expression names an exact project declaration; the copyable module probe and full project command follow the bridges.

Bridge 1: maximize every partial sum, including time zero

finiteBirkhoffSumMax T g N ω

Bridge 2: strict event membership produces a positive-time witness

mem_finiteHopfEvent_iff

Bridge 3: combine the selected and unselected atoms

finiteBirkhoffSumMax_sub_comp_le_indicator (T := T) (g := g) N ω

Bridge 4: preservation cancels the shifted maximum

integral_finiteHopfEvent_nonneg hT hg N

Bridge 5: threshold centering is exactly average exceedance

mem_finiteBirkhoffAverageExceedanceSet_iff

Bridge 6: remove the event from the right side

finiteBirkhoffAverageExceedanceSet_posPart_bound hT hg N a

Bridge 7: divide only with a positive threshold

measureReal_finiteBirkhoffAverageExceedanceSet_le hT hg N ha

Type-check the exact project interface

import NonlinearDynamics.Random.RandomCocycles.FiniteHopfMaximal

open NonlinearDynamics.Random.RandomCocycles

#check finiteBirkhoffSumMax
#check finiteBirkhoffSumMax_nonneg
#check mem_finiteHopfEvent_iff
#check finiteBirkhoffSumMax_sub_comp_le_indicator
#check integral_finiteHopfEvent_nonneg
#check mem_finiteBirkhoffAverageExceedanceSet_iff
#check finiteBirkhoffAverageExceedanceSet_posPart_bound
#check measureReal_finiteBirkhoffAverageExceedanceSet_le

cd formalization
lake env lean NonlinearDynamics/Random/RandomCocycles/FiniteHopfMaximal.lean

cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomCocycles/FiniteHopfMaximal.lean

Run the entire four-cycle ledger with Std

The following file imports only Lean’s Std library. It defines its own four-cycle, finite sums, running maxima, rational averages, indicators, and uniform atom integrals. It does not import Mathlib or the project. Save the block byte for byte as /tmp/FiniteHopfMaximalDeepDiveTutorial.lean:

import Std

namespace FiniteHopfMaximalDeepDiveTutorial

inductive OrbitState where
  | a
  | b
  | c
  | d
  deriving Repr, DecidableEq

def states : List OrbitState :=
  [.a, .b, .c, .d]

def stateName : OrbitState → String
  | .a => "a"
  | .b => "b"
  | .c => "c"
  | .d => "d"

def step : OrbitState → OrbitState
  | .a => .b
  | .b => .c
  | .c => .d
  | .d => .a

def observable : OrbitState → Int
  | .a => -2
  | .b => 3
  | .c => -4
  | .d => 2

def iterate : Nat → OrbitState → OrbitState
  | 0, x => x
  | n + 1, x => iterate n (step x)

def orbitSum : Nat → OrbitState → Int
  | 0, _ => 0
  | n + 1, x => orbitSum n x + observable (iterate n x)

def orbitValues (horizon : Nat) (x : OrbitState) : List Int :=
  (List.range horizon).map fun j => observable (iterate j x)

def partialSums (horizon : Nat) (x : OrbitState) : List Int :=
  (List.range (horizon + 1)).map fun k => orbitSum k x

def runningMaximaFrom : Int → List Int → List Int
  | _, [] => []
  | current, value :: rest =>
      let next := max current value
      next :: runningMaximaFrom next rest

def runningMaxima (horizon : Nat) (x : OrbitState) : List Int :=
  runningMaximaFrom 0 (partialSums horizon x)

def finiteMax (horizon : Nat) (x : OrbitState) : Int :=
  (partialSums horizon x).foldl max 0

def inStrictEvent (horizon : Nat) (x : OrbitState) : Bool :=
  decide (0 < finiteMax horizon x)

def inNonstrictEvent (horizon : Nat) (x : OrbitState) : Bool :=
  decide (0 ≤ finiteMax horizon x)

def average (k : Nat) (x : OrbitState) : Rat :=
  (orbitSum k x : Rat) / (k : Rat)

def positiveTimeAverages (horizon : Nat) (x : OrbitState) : List Rat :=
  (List.range horizon).map fun j => average (j + 1) x

def exceedsAverage
    (horizon : Nat) (threshold : Rat) (x : OrbitState) : Bool :=
  (List.range horizon).any fun j =>
    decide (threshold < average (j + 1) x)

def selectedStates (horizon : Nat) : List OrbitState :=
  states.filter fun x => inStrictEvent horizon x

def thresholdStates
    (horizon : Nat) (threshold : Rat) : List OrbitState :=
  states.filter fun x => exceedsAverage horizon threshold x

def indicatorContribution (horizon : Nat) (x : OrbitState) : Int :=
  if inStrictEvent horizon x then observable x else 0

def sumObservable (selected : List OrbitState) : Int :=
  selected.foldl (fun total x => total + observable x) 0

def quarterIntegral (numerator : Int) : Rat :=
  (numerator : Rat) / 4

def positivePartSum : Int :=
  states.foldl (fun total x => total + max (observable x) 0) 0

structure OrbitRow where
  start : String
  values : List Int
  sums : List Int
  maxima : List Int
  strictPositive : Bool
  averages : List Rat
  averageAboveOne : Bool
  deriving Repr, DecidableEq

def orbitRow (x : OrbitState) : OrbitRow :=
  { start := stateName x
    values := orbitValues 4 x
    sums := partialSums 4 x
    maxima := runningMaxima 4 x
    strictPositive := inStrictEvent 4 x
    averages := positiveTimeAverages 4 x
    averageAboveOne := exceedsAverage 4 1 x }

structure PointwiseRow where
  start : String
  maximumHere : Int
  maximumAfterStep : Int
  difference : Int
  indicatorTimesObservable : Int
  inequalityHolds : Bool
  deriving Repr, DecidableEq

def pointwiseRow (x : OrbitState) : PointwiseRow :=
  let here := finiteMax 4 x
  let shifted := finiteMax 4 (step x)
  let contribution := indicatorContribution 4 x
  { start := stateName x
    maximumHere := here
    maximumAfterStep := shifted
    difference := here - shifted
    indicatorTimesObservable := contribution
    inequalityHolds := decide (here - shifted ≤ contribution) }

structure IntegralLedger where
  strictEvent : List String
  maxDifferenceNumerator : Int
  indicatorNumerator : Int
  eventIntegral : Rat
  thresholdOneEvent : List String
  thresholdOneMeasure : Rat
  thresholdOneLeftSide : Rat
  thresholdOneEventIntegral : Rat
  positivePartIntegral : Rat
  weakBoundAtOneHolds : Bool
  zeroThresholdEvent : List String
  zeroThresholdMeasure : Rat
  dividedRightAtZero : Rat
  weakBoundAtZeroWouldHold : Bool
  zeroHorizonStrictEvent : List String
  zeroHorizonNonstrictEvent : List String
  deriving Repr, DecidableEq

def integralLedger : IntegralLedger :=
  let strict := selectedStates 4
  let pointwise := states.map pointwiseRow
  let differenceTotal :=
    pointwise.foldl (fun total row => total + row.difference) 0
  let indicatorTotal :=
    pointwise.foldl
      (fun total row => total + row.indicatorTimesObservable) 0
  let thresholdOne := thresholdStates 4 1
  let thresholdZero := thresholdStates 4 0
  let positiveIntegral := quarterIntegral positivePartSum
  { strictEvent := strict.map stateName
    maxDifferenceNumerator := differenceTotal
    indicatorNumerator := indicatorTotal
    eventIntegral := quarterIntegral indicatorTotal
    thresholdOneEvent := thresholdOne.map stateName
    thresholdOneMeasure := (thresholdOne.length : Rat) / 4
    thresholdOneLeftSide := 1 * ((thresholdOne.length : Rat) / 4)
    thresholdOneEventIntegral :=
      quarterIntegral (sumObservable thresholdOne)
    positivePartIntegral := positiveIntegral
    weakBoundAtOneHolds :=
      decide ((thresholdOne.length : Rat) / 4 ≤ positiveIntegral / 1)
    zeroThresholdEvent := thresholdZero.map stateName
    zeroThresholdMeasure := (thresholdZero.length : Rat) / 4
    dividedRightAtZero := positiveIntegral / 0
    weakBoundAtZeroWouldHold :=
      decide ((thresholdZero.length : Rat) / 4 ≤ positiveIntegral / 0)
    zeroHorizonStrictEvent :=
      (states.filter fun x => inStrictEvent 0 x).map stateName
    zeroHorizonNonstrictEvent :=
      (states.filter fun x => inNonstrictEvent 0 x).map stateName }

#eval states.map orbitRow
#eval states.map pointwiseRow
#eval integralLedger

example : partialSums 4 .a = [0, -2, 1, -3, -1] := by
  native_decide
example : partialSums 4 .b = [0, 3, -1, 1, -1] := by
  native_decide
example : partialSums 4 .c = [0, -4, -2, -4, -1] := by
  native_decide
example : partialSums 4 .d = [0, 2, 0, 3, -1] := by
  native_decide

example : runningMaxima 4 .a = [0, 0, 1, 1, 1] := by
  native_decide
example : runningMaxima 4 .b = [0, 3, 3, 3, 3] := by
  native_decide
example : runningMaxima 4 .c = [0, 0, 0, 0, 0] := by
  native_decide
example : runningMaxima 4 .d = [0, 2, 2, 3, 3] := by
  native_decide

example : selectedStates 4 = [.a, .b, .d] := by
  native_decide
example : thresholdStates 4 1 = [.b, .d] := by
  native_decide
example : thresholdStates 4 0 = [.a, .b, .d] := by
  native_decide

example : (states.map pointwiseRow).map PointwiseRow.difference =
    [-2, 3, -3, 2] := by native_decide
example : (states.map pointwiseRow).map
    PointwiseRow.indicatorTimesObservable = [-2, 3, 0, 2] := by
  native_decide
example : (states.map pointwiseRow).all PointwiseRow.inequalityHolds = true := by
  native_decide

example : integralLedger.eventIntegral = (3 : Rat) / 4 := by
  native_decide
example : integralLedger.thresholdOneMeasure = (1 : Rat) / 2 := by
  native_decide
example : integralLedger.thresholdOneEventIntegral = (5 : Rat) / 4 := by
  native_decide
example : integralLedger.positivePartIntegral = (5 : Rat) / 4 := by
  native_decide
example : integralLedger.weakBoundAtOneHolds = true := by
  native_decide
example : integralLedger.dividedRightAtZero = 0 := by
  native_decide
example : integralLedger.weakBoundAtZeroWouldHold = false := by
  native_decide
example : integralLedger.zeroHorizonStrictEvent = [] := by
  native_decide
example : integralLedger.zeroHorizonNonstrictEvent =
    ["a", "b", "c", "d"] := by
  native_decide

end FiniteHopfMaximalDeepDiveTutorial

The key syntax is ordinary and finite:

• inductive OrbitState creates exactly four named states;
• iterate advances the cycle without importing Mathlib’s iterate API;
• List.range (horizon + 1) includes the zero-time sum;
• foldl max 0 accumulates a running finite maximum from the forced zero;
• Rat keeps all averages and uniform atom integrals exact;
• decide computes a finite comparison; and
• every native_decide example supplies a kernel-checked proof of the displayed ledger.

With the pinned compiler installed, a human types:

source "$HOME/.elan/env"
elan run leanprover/lean4:v4.32.0 lean \
  /tmp/FiniteHopfMaximalDeepDiveTutorial.lean

This is a standalone tutorial suitable for a normal macOS or Linux host. It imports only Std, enumerates four states, and does not compile Mathlib or this project. Successful execution prints exactly:

[{ start := "a",
   values := [-2, 3, -4, 2],
   sums := [0, -2, 1, -3, -1],
   maxima := [0, 0, 1, 1, 1],
   strictPositive := true,
   averages := [-2, (1 : Rat)/2, -1, (-1 : Rat)/4],
   averageAboveOne := false },
 { start := "b",
   values := [3, -4, 2, -2],
   sums := [0, 3, -1, 1, -1],
   maxima := [0, 3, 3, 3, 3],
   strictPositive := true,
   averages := [3, (-1 : Rat)/2, (1 : Rat)/3, (-1 : Rat)/4],
   averageAboveOne := true },
 { start := "c",
   values := [-4, 2, -2, 3],
   sums := [0, -4, -2, -4, -1],
   maxima := [0, 0, 0, 0, 0],
   strictPositive := false,
   averages := [-4, -1, (-4 : Rat)/3, (-1 : Rat)/4],
   averageAboveOne := false },
 { start := "d",
   values := [2, -2, 3, -4],
   sums := [0, 2, 0, 3, -1],
   maxima := [0, 2, 2, 3, 3],
   strictPositive := true,
   averages := [2, 0, 1, (-1 : Rat)/4],
   averageAboveOne := true }]
[{ start := "a",
   maximumHere := 1,
   maximumAfterStep := 3,
   difference := -2,
   indicatorTimesObservable := -2,
   inequalityHolds := true },
 { start := "b",
   maximumHere := 3,
   maximumAfterStep := 0,
   difference := 3,
   indicatorTimesObservable := 3,
   inequalityHolds := true },
 { start := "c",
   maximumHere := 0,
   maximumAfterStep := 3,
   difference := -3,
   indicatorTimesObservable := 0,
   inequalityHolds := true },
 { start := "d",
   maximumHere := 3,
   maximumAfterStep := 1,
   difference := 2,
   indicatorTimesObservable := 2,
   inequalityHolds := true }]
{ strictEvent := ["a", "b", "d"],
  maxDifferenceNumerator := 0,
  indicatorNumerator := 3,
  eventIntegral := (3 : Rat)/4,
  thresholdOneEvent := ["b", "d"],
  thresholdOneMeasure := (1 : Rat)/2,
  thresholdOneLeftSide := (1 : Rat)/2,
  thresholdOneEventIntegral := (5 : Rat)/4,
  positivePartIntegral := (5 : Rat)/4,
  weakBoundAtOneHolds := true,
  zeroThresholdEvent := ["a", "b", "d"],
  zeroThresholdMeasure := (3 : Rat)/4,
  dividedRightAtZero := 0,
  weakBoundAtZeroWouldHold := false,
  zeroHorizonStrictEvent := [],
  zeroHorizonNonstrictEvent := ["a", "b", "c", "d"] }

The first value is the full orbit table, the second is the atomwise indicator inequality, and the third is the integral, threshold, and boundary ledger. Because the transcript is exact, a changed rational, event member, or theorem boundary is visible immediately.

Four sources, four different scopes

Historical names in ergodic theory can compress several different theorem forms. RMT-23 keeps a source ledger so attribution does not become a claim of formal equivalence.

Yosida and Kakutani, 1939

Kôsaku Yosida and Shizuo Kakutani’s Birkhoff’s Ergodic Theorem and the Maximal Ergodic Theorem is the priority source for the maximal ergodic theorem. The article occupies pages 165-168. Its Theorem 2 is an infinite-horizon statement about orbit averages, and pages 166-167 prove it by selecting finite maximal intervals. That interval argument is historical ancestry, not RMT-23’s finite maximum-minus-shift proof. RMT-23 cites the paper for priority and conceptual lineage, not as a line-by-line source file for the Lean development.

Hopf, 1954

Eberhard Hopf’s The General Temporally Discrete Markoff Process works in a broader Markov-process and positive-operator setting. The DOI resolves to a 33-page article. This chapter cites it at article level only. It would be inaccurate to attach one page to RMT-23’s exact transformation theorem without a page-level archival audit, and it would be inaccurate to say the Lean module formalizes Hopf’s full operator generality.

Garsia, 1965

Adriano M. Garsia’s A Simple Proof of E. Hopf’s Maximal Ergodic Theorem is the exact proof-architecture source. Page 381 uses a finite running maximum, the strict positive event, and a pointwise comparison that peels the first summand or observable term in an operator partial sum. In the Koopman specialization used by RMT-23, that term is one orbit value. The paper is only two pages long. Garsia’s positive norm-nonincreasing operator proof uses positivity and contraction; exact equality of the current and shifted maximum integrals is the measure-preserving Koopman specialization used in RMT-23.

The notation distinguishes two different objects. Garsia’s \(S_n^+\) is a maximum over partial sums, not \(\max(S_n,0)\), the positive part of the single terminal value. RMT-23 names the object finiteBirkhoffSumMax to prevent that ambiguity.

Keane and Petersen, 2006

Michael Keane and Karl Petersen’s Easy and Nearly Simultaneous Proofs of the Ergodic Theorem and Maximal Ergodic Theorem develops a strengthening and its relation to the pointwise theorem. Pages 248-249 show a finite-to-infinite route. The arXiv abstract explicitly says the paper proves a strengthening that yields the pointwise theorem.

RMT-23 does not formalize that passage. It establishes the finite event, finite inequality, and horizon-uniform weak estimate. Countable unions, infinite suprema, approximation, and almost-everywhere convergence remain future milestones.

The complete twenty-five-declaration ledger

The frozen 509-line module exposes exactly twenty-five public declarations in source order. It also contains one private integral-transport helper and eleven anonymous compiled probes. The SHA-256 of the audited source is 3f385c36fae5d0483ea592468d4d79d197e74a4e241b63f859b0aaace03a8b58.

The private declaration integral_comp_of_measurePreserving is intentionally not part of the public count. It proves integral invariance under composition using integral_map and hT.map_eq. Keeping it private avoids creating a project-level duplicate of general Mathlib transport infrastructure while making the core proof readable.

Proof architecture as a dependency graph

The module has three largely separable layers.

Layer A: finite order and event geometry

Declarations 1 through 5 and 8, 11 through 16 are pointwise finite mathematics. Several explicitly omit the measurable-space instance. They establish candidate domination, nonnegativity, horizon monotonicity, exact boundaries, the positive witness, peeling, and the indicator inequality.

Layer B: analytic legitimacy and cancellation

Declarations 6, 7, 9, 10, and 17 prove that the objects can be measured and integrated. Ordinary measurability and integrability are kept as separate routes. The private transport helper plus the pointwise indicator inequality produce the core set-integral result.

Layer C: centered threshold consequences

Declarations 18 through 25 reinterpret the strict event for \(g-a\) as an average-exceedance event. Finite total measure enters to integrate the constant threshold. The final two declarations remove the event from the right side and divide only under a positive-threshold proof.

This separation matters for reuse. A later theorem can use the pointwise inequality without measure theory, the core finite lemma on an infinite measure space, or the threshold corollaries on a finite measure space.

Eleven probes guard the theorem boundary

The anonymous example blocks are compiled theorems. They do not increase the public API, but they reject tempting premise drift.

Probe 1: horizon zero

For arbitrary \(T\) and \(g\), \(E_0(g)=\varnothing\). This tests the strict time-zero convention.

Probe 2: horizon one

For arbitrary \(T,g,\omega\), membership in \(E_1(g)\) is exactly \(0\lt g(\omega)\). This tests the sum range and off-by-one convention.

Probe 3: zero observable

For every finite horizon, the zero observable has empty strict event. Every partial sum is zero.

Probe 4: the nonstrict event

The set \(\{\omega:0\le M_Ng(\omega)\}\) is the full space. This compiles the reason strict positivity is essential rather than leaving it as rhetoric.

Probe 5: identity dynamics

The core nonnegative event integral works for the identity transformation and an arbitrary integrable observable.

Probe 6: zero measure

The theorem works for the zero measure and the zero observable under any measurable transformation. This checks that probability normalization and positive mass are absent.

Probe 7: infinite counting measure

Counting measure on the natural numbers is not finite. An integrable point mass under identity dynamics still satisfies the core theorem. This checks that [IsFiniteMeasure μ] must not leak into declaration 17.

Probe 8: a noninjective preserved transformation

A constant map on the Boolean type preserves a Dirac measure at its fixed point but is not injective. The theorem still applies. Invertibility is not hidden in preservation.

Probe 9: preservation is not disposable

On a Dirac measure at true, a constant map sends the mass to false. With an explicitly chosen two-point observable, the finite event contains the measured point while its event integral is negative. The transformation is measurable and the observable integrable, but preservation fails. This counterexample refutes the corresponding cancellation claim without the preservation premise.

Probe 10: negative threshold

The threshold integral lower bound is instantiated at \(a=-1\). This checks that positivity must not be demanded before division.

Probe 11: positive-threshold weak estimate

The final theorem is instantiated with \(a\gt0\), confirming the exact premise needed for ordered division.

Axiom and source-integrity audit

The module prints the axioms of:

• integral_finiteHopfEvent_nonneg;
• finiteBirkhoffAverageExceedanceSet_integral_lower_bound; and
• measureReal_finiteBirkhoffAverageExceedanceSet_le.

The checked module contains no sorry, admit, unsafe declarations, or custom project axioms. The expected theorem footprint is the standard Lean and Mathlib classical quotient infrastructure already present in prior milestones, not a new mathematical assumption.

All Mathlib source links in this chapter point to the exact commit 81a5d257c8e410db227a6665ed08f64fea08e997, corresponding to the pinned v4.32.0 checkout. Current online documentation is convenient for browsing, but the pinned checkout is the API authority for what compiled.

Solved exercises

Exercise 1: expand the first four sums

Write \(S_0g(\omega)\), \(S_1g(\omega)\), \(S_2g(\omega)\), and \(S_3g(\omega)\).

Exercise 2: compute a conceptual running maximum

Suppose the finite partial sums through time four are \(0,-2,1,-1,3\). What is the running maximum, and is the point in the strict event?

Exercise 3: terminal positive part is not enough

Give a finite sequence of partial sums whose terminal value is negative but whose running maximum is positive.

Exercise 4: time-zero nonnegativity

Why is \(M_Ng(\omega)\ge0\) true without any assumption on \(T\) or \(g\)?

Exercise 5: reject the nonstrict event

Prove that \(\{\omega:0\le M_Ng(\omega)\}=\Omega\).

Exercise 6: horizon zero

Compute \(M_0g\) and \(E_0(g)\).

Exercise 7: horizon one

Show that \(\omega\in E_1(g)\) exactly when \(g(\omega)\gt0\).

Exercise 8: horizon monotonicity

Why can \(M_Mg(\omega)\le M_Ng(\omega)\) hold even when the partial sums decrease between times \(M\) and \(N\)?

Exercise 9: event monotonicity

Deduce \(E_M(g)\subseteq E_N(g)\) from \(M\le N\).

Exercise 10: identify the measurable route

Which premises prove that \(M_Ng\) is ordinarily measurable?

Exercise 11: identify the integrable route

Why does integrability of \(g\) alone not prove integrability of \(g\circ T^j\)?

Exercise 12: ordinary versus null measurability

Why does the core theorem use a null-measurable event rather than deriving ordinary measurability directly from Integrable g μ?

Exercise 13: a positive maximizer is not zero

Suppose \(M_Ng(\omega)\gt0\) and \(S_kg(\omega)=M_Ng(\omega)\). Prove \(k\ne0\).

Exercise 14: peel the first value

For \(k=j+1\), rewrite \(S_kg(\omega)\) using the shifted orbit.

Exercise 15: bound the remainder

Why is \(S_jg(T\omega)\le M_Ng(T\omega)\) in the peeling proof?

Exercise 16: derive the on-event branch

Combine Exercises 14 and 15 to bound the maximum difference.

Exercise 17: derive the off-event branch

Suppose \(\omega\notin E_N(g)\). Prove \(M_Ng(\omega)-M_Ng(T\omega)\le0\).

Exercise 18: combine with an indicator

State one pointwise inequality valid on and off the event.

Exercise 19: no measurable argmax

Why does the proof not need the maximizing index to vary measurably with \(\omega\)?

Exercise 20: locate preservation

Which equality uses measure preservation in the core argument?

Exercise 21: perform the cancellation

Compute \(\int_\Omega(M_Ng-M_Ng\circ T)\,d\mu\) under preservation.

Exercise 22: identify unnecessary dynamics

Does the proof ever solve \(T\upsilon=\omega\)?

Exercise 23: infinite total mass

Why can the core theorem hold under counting measure even though the full space has infinite measure?

Exercise 24: center a finite sum

Prove \(S_k(g-a)=S_kg-ka\).

Exercise 25: translate positivity to an average

For \(k\ge1\), show \(0\lt S_k(g-a)(\omega)\) if and only if \(a\lt A_kg(\omega)\).

Exercise 26: why finite measure appears

Why does the centered integrability theorem assume finite total measure?

Exercise 27: no sign condition yet

Why is the inequality \(a\mu_{\mathbb R}(E)\le\int_Eg\,d\mu\) valid for negative \(a\)?

Exercise 28: positive-part domination

Prove \(\int_Eg\,d\mu\le\int_\Omega g^+\,d\mu\).

Exercise 29: locate threshold positivity

Why does the weak estimate require \(a\gt0\)?

Exercise 30: horizon uniformity

Which side of the positive-part bound is independent of \(N\), and why does that matter?

Exercise 31: preservation countermodel

What does the Boolean Dirac probe show?

Exercise 32: state the exact summit

Summarize RMT-23 in one sentence without saying that it proves the pointwise ergodic theorem.

Premise ledger

There is one subtle receiver distinction. The core theorem’s MeasurePreserving argument contains measurability and map equality. Describing the result as requiring “only integrability” would be false. The correct statement is that it needs preservation and integrability, but no finite-mass, probability, ergodicity, or invertibility premise.

Nonclaim ledger

RMT-23 does not establish:

1. an infinite-horizon maximal function;
2. measurability or integrability of an infinite supremum;
3. the infinite maximal ergodic theorem;
4. almost-everywhere convergence of Birkhoff averages;
5. membership in the Birkhoff convergence event ;
6. the pointwise Birkhoff ergodic theorem;
7. convergence to a conditional expectation;
8. convergence to a space average under ergodicity;
9. convergence in \(L^1\), probability, or distribution;
10. an interchange of limit and integral;
11. a strong-type \(L^1\) maximal bound;
12. an event-measure bound at zero or negative threshold;
13. expectation centering or mean zero for \(g-a\);
14. probability normalization of the ambient measure;
15. ergodicity of \(T\);
16. injectivity, surjectivity, or invertibility of \(T\);
17. mixing, independence, or correlation decay;
18. a result for a general positive contraction or Markov operator;
19. Hopf’s full 1954 operator theorem;
20. a line-by-line formalization of Yosida and Kakutani’s 1939 article;
21. Kingman’s subadditive ergodic theorem;
22. a density theorem for favorable subadditive-process starts;
23. a signed matrix-cocycle growth limit;
24. a Lyapunov exponent; or
25. an Oseledets filtration or splitting.

What remains after the finite estimate

The events \(E_{N,a}(g)\) increase with \(N\). Their union is the set where at least one positive-time finite Birkhoff average exceeds \(a\):

Because the finite positive-part bound is uniform in \(N\), continuity from below of a finite measure suggests an infinite weak estimate. That passage still needs to be formalized carefully. One must connect the set-theoretic union to a precisely chosen infinite maximal object, often an extended-real-valued supremum, prove the relevant measurability, and transport the real-valued measure bounds without silently assuming more than the finite theorem provides.

Even an infinite maximal inequality is not itself the pointwise ergodic theorem. A standard route first proves convergence on a dense class of observables for which the limit is controlled, then uses a maximal estimate to control the exceptional set arising from approximation, and finally extends to every integrable observable. Identification and invariance of the limit require further arguments.

The 2006 Keane-Petersen source is useful precisely because it makes the finite-to-infinite relationship explicit. It is not evidence that those later steps are already present in Lean.

For the larger subadditive program, the pointwise Birkhoff theorem is still only one ingredient. Earlier phase-averaging and ordered-interval-packing milestones need a checked density or frequency bridge before finite subadditive estimates can yield convergence of normalized process values. RMT-23 advances the analytic Birkhoff branch without completing Kingman’s theorem.

Where to continue

The finite maximal ergodic inequality entry is the compact definition and assumption reference.

The Birkhoff sum entry develops the finite sum, its two successor identities, and powered-map block interpretation.

The ergodic probability base entry keeps preservation, probability, ergodicity, and integrability separate. RMT-23 is a concrete demonstration that the historical adjective “ergodic” does not force an ergodicity premise into every maximal lemma.

Birkhoff Convergence Events Before the Pointwise Ergodic Theorem is the event-theoretic predecessor. It proves exact invariance and conditional rigidity while explicitly leaving convergence existence open.

The Finite Hopf Maximal Ergodic Lemma in Lean maps the twenty-five public declarations and eleven probes to the checked Lean proof commands.

References

Kôsaku Yosida and Shizuo Kakutani. Birkhoff’s Ergodic Theorem and the Maximal Ergodic Theorem, Proceedings of the Imperial Academy 15(6), 165-168, 1939. Theorem 2 is an infinite-horizon average theorem; pages 166-167 prove it using finite maximal intervals. That is not RMT-23’s finite maximum-minus-shift proof. The J-STAGE archive records the publication date as July 12, 1939. This is the priority source; its whole paper is not claimed as a formalization target of RMT-23.

Eberhard Hopf. The General Temporally Discrete Markoff Process, Journal of Rational Mechanics and Analysis 3, 13-45, 1954. This chapter uses an article-level citation only. Hopf’s setting is broader than a single measure-preserving transformation, and no page-specific identity with the RMT-23 theorem is asserted.

Adriano M. Garsia. A Simple Proof of E. Hopf’s Maximal Ergodic Theorem, Journal of Mathematics and Mechanics 14(3), 381-382, 1965. Page 381 is the exact finite strict-event and pointwise running-maximum source used to audit the RMT-23 proof architecture. Its \(S_n^+\) is a running maximum, not the positive part of the terminal sum.

Michael Keane and Karl Petersen. Easy and Nearly Simultaneous Proofs of the Ergodic Theorem and Maximal Ergodic Theorem, IMS Lecture Notes-Monograph Series 48, 248-251, 2006, related DOI 10.1214/074921706000000266. Pages 248-249 supply the finite-to-infinite comparison. The arXiv record describes a strengthening that also yields the pointwise theorem; RMT-23 formalizes neither that strengthening nor the limiting conclusion.

Mathlib contributors. Finite Birkhoff sums, with the pinned definition and successor laws. RMT-23 reuses the zero-based sum and the first-summand shifted recurrence.

Mathlib contributors. Integration under a mapped measure, with the pinned integral_map theorem. The private RMT-23 helper uses integral_map together with the pinned MeasurePreserving.map_eq field to cancel the shifted maximum integral.

Mathlib contributors. Measurable and integrable lattice operations provide the finite-supremum and maximum infrastructure, including the pinned finite-supremum measurability lemmas, used to package the running maximum without a measurable argmax.

The exact upstream revision audited throughout is commit 81a5d257, the Mathlib v4.32.0 revision pinned by formalization/lake-manifest.json.