Weak-type (1,1) maximal bound

Let \(\Omega=\{p,q,r,s\}\) carry the uniform probability measure with mass \(1/4\) at each point, let \(T\) be the identity map, and set

Every positive-time orbit average equals the starting value because the orbit never moves. At strict threshold \(a=2\),

Thus the event measure is \(1/4\). The integrable input size is

so the weak-\((1,1)\) inequality reads

This controls the probability of obtaining a large average. It does not bound every average pointwise by \(7/8\): at \(p\), the average is \(4\).

A weak-type (1,1) maximal bound turns integrable size into control of a bad set. For a real observable, it says that the set of starting points where at least one positive-time average has large absolute value has measure at most the observable’s \(L^1\) size divided by the positive threshold. The first \(1\) refers to the integrable input scale. The second \(1\) refers to a weak \(L^1\) level-set estimate, not to an integrable norm bound for a maximal function.

Random-matrix-theory milestone 26 (RMT-26) applies this estimate to an approximation error. That is the quantitative stability needed to pass pointwise convergence from a dense good class to every real integrable observable. The complete implementation narrative is The Missing Step Closes: Pointwise Birkhoff by Maximal Control in Lean. The connected textbook chapter is Pointwise Birkhoff from Maximal Control and Dense Good Functions.

Exact event-level definition

Let \(\Omega\) be a state space, let \(T:\Omega\to\Omega\) be a discrete-time map, and let \(h:\Omega\to\mathbb R\) be a real observable. At a natural horizon \(n\), define the normalized Birkhoff average

For a real threshold \(a\), the absolute positive-time exceedance event is

RMT-26 names this set directly instead of defining a new real-valued supremum:

def birkhoffAverageAbsoluteExceedanceSet
    (T : Ω → Ω) (h : Ω → ℝ) (a : ℝ) : Set Ω :=
  {ω | ∃ k, 1 ≤ k ∧
    a < |birkhoffAverage ℝ T h k ω|}

Assume that \(\mu\) is a finite measure on \(\Omega\), \(T\) preserves \(\mu\), \(h\) is integrable, and \(a\gt0\). The checked weak estimate is

The notation \(\mu_{\mathbb R}\) denotes Mathlib’s real-valued projection of the extended nonnegative measure. Finite total mass ensures that no infinite set measure is sent through the projection. The numerator is exactly the \(L^1\) norm of a real integrable representative.

In standard weak-type notation, an operator \(\mathcal M\) has weak type \((1,1)\) with constant \(C\) when

The RMT-26 result has the event-level shape with \(C=1\). It deliberately does not construct \(\mathcal Mh\) as a finite real number at every point. The existential event remains meaningful even when the sequence of absolute averages is unbounded.

Why the estimate is absolute

The earlier infinite-horizon Birkhoff-average exceedance event is one-sided. It records a witness to \(a\lt A_nh(\omega)\), and its bound uses the positive part of \(h\). RMT-26 needs control of \(|A_nh|\) because the error between two average sequences can have either sign.

For every horizon, the finite triangle inequality gives

At horizon zero both sides are zero under Lean’s totalized inverse convention. At positive horizons this is the ordinary triangle inequality for a finite sum, divided by the nonnegative integer \(n\). Therefore

Apply the RMT-24 one-sided weak estimate to \(|h|\). Since \(|h|\ge0\), its positive part is itself, and the numerator simplifies to \(\int|h|\,d\mu\). This proves the absolute theorem without adding an invertibility or ergodicity premise and without defining a supremum function.

Threshold scaling and near-misses

For the four-point example, strictness gives:

| threshold \(a\) | event \(\{|A_nh|\gt a\text{ for some }n\ge1\}\) | event measure | \(\lVert h\rVert_1/a\) | |—:|—|—:|—:| | \(1\) | \(\{p,q\}\) | \(1/2\) | \(7/4\) | | \(2\) | \(\{p\}\) | \(1/4\) | \(7/8\) | | \(4\) | \(\varnothing\) | \(0\) | \(7/16\) |

Raising the threshold shrinks both the actual event and the theorem’s inverse-threshold budget. The bound need not be sharp.

Two tempting alterations fail:

• Dropping the absolute value at threshold \(1\) keeps \(p\) but loses \(q\), whose average is \(-2\). A one-sided estimate cannot control a signed approximation error in both directions.
• Setting \(a=0\) makes the strict absolute event \(\{p,q,r\}\), of measure \(3/4\). Lean totalizes real division by zero to zero, so the displayed quotient would be \(0\), producing the false claim \(3/4\leq0\). The hypothesis \(0\lt a\) is therefore mathematically essential.

At a nonstrict threshold \(2\), \(q\) would also enter because \(|h(q)|=2\). The checked event is strict. Its complement consequently yields the useful statement that every positive-time absolute average is at most the threshold.

Why weak control is the right closure tool

Suppose \(f\) is a target observable and \(g\) is a nearby observable whose Birkhoff averages already converge almost everywhere. Set \(h=f-g\). Small \(L^1\) distance means that

is small. It does not imply a pointwise bound on \(h\), and it certainly does not imply that every orbit average of \(h\) is uniformly small. The weak estimate gives precisely the available replacement:

Outside this controlled event, every positive-time error average has absolute value at most \(a\). Choose \(a=\varepsilon/3\). If the average sequence of \(g\) is already Cauchy at scale \(\varepsilon/3\), then the three-term comparison

makes the average sequence of \(f\) Cauchy at scale \(\varepsilon\), except on the maximal-error event and the null set where \(g\) fails to converge. This is the engine behind the Birkhoff Cauchy exceptional set estimate.

If pointwise-good approximants can be chosen at arbitrarily small \(L^1\) distance, the upper bound tends to zero at every fixed positive scale. The exceptional set is null. A countable intersection over reciprocal scales then gives full-sequence almost-everywhere convergence. Weak control is enough because the desired conclusion is also almost everywhere. A strong \(L^1\)-norm estimate for a maximal function is neither stated nor consumed.

This pattern is historically associated with maximal-to-pointwise proofs. Yosida and Kakutani’s 1939 transformation theorem introduced an explicit maximal ergodic theorem. Yosida’s 1940 development paired maximal control with a closure principle, and Keane and Petersen’s 2006 proof presents a compact modern probability-space route. RMT-26 follows the same high-level strategy through repository-specific finite and infinite event theorems.

Event bounds, not pointwise bounds

The conclusion controls a set measure. It must not be rewritten as

for each point or horizon. That expression has the wrong logical form and the wrong units. The actual theorem says that the set on which some horizon crosses \(a\) is small. A few starting points may have very large orbit averages while the estimate remains true.

Nor does the theorem say that the event measure equals the quotient. The right side may exceed the total mass of the space, as the two-point example shows. One may combine it with the monotonicity bound \(\mu(M_a)\le\mu(\Omega)\), but RMT-26 does not package that minimum because the quotient form is exactly what the closure argument needs.

Boundary cases and nonclaims

• The threshold is strictly positive. At \(a=0\), the event can be nonempty, while real division by zero is totalized in Lean. A theorem with the displayed quotient at zero would therefore be false in general. Negative thresholds are even less suitable: since absolute values are nonnegative, every point crosses every negative threshold at time one.
• The crossing is strict. Equality \(|A_nh|=a\) does not witness the event. The complement consequently supplies the useful weak inequality \(|A_nh|\le a\) at every positive horizon.
• Time zero is excluded. The definition requires \(1\le n\). The totalized empty average cannot create a witness.
• Finite measure is explicit. Probability normalization is stronger and unnecessary. On an infinite-measure space, Mathlib’s real projection sends infinite extended mass to zero, so the displayed real-valued argument cannot be reused unchanged. Finite total mass is the checked boundary of this proof route, not a claim that the broader pointwise theorem is false on every infinite-measure space.
• The zero measure is allowed. Both sides are zero. This is a valid but vacuous measure bound and does not establish pointwise smallness.
• Only measure preservation is assumed of the dynamics. Ergodicity, injectivity, surjectivity, invertibility, and mixing are absent.
• Integrability is representative-sensitive only on null sets. Changing \(h\) on a null set may alter the raw event at individual points. Under the measure-preserving hypotheses, the measure estimate remains an almost-everywhere statement about the chosen representative.

The weak bound does not identify a limit, prove convergence by itself, show that the maximal event is invariant, give an \(L^1\)-integrable maximal function, establish norm convergence of averages, or imply an ergodic constant. It also does not prove Kingman’s subadditive theorem, a Lyapunov exponent, or an Oseledets filtration or splitting.

In Lean

ω ∈ birkhoffAverageAbsoluteExceedanceSet T h a

measureReal_birkhoffAverageAbsoluteExceedanceSet_le hT hh ha

Tiny standalone worksheet

Save this finite arithmetic model as WeakTypeTutorial.lean:

import Std

inductive Point where | p | q | r | s
deriving Repr, DecidableEq

def h : Point → Int
  | .p => 4 | .q => -2 | .r => 1 | .s => 0

def absInt (z : Int) : Nat := z.natAbs

def crosses (threshold : Nat) (x : Point) : Bool :=
  decide (threshold < absInt (h x))

def points : List Point := [.p, .q, .r, .s]

def eventCount (threshold : Nat) : Nat :=
  (points.filter (crosses threshold)).length

def l1Numerator : Nat :=
  points.foldl (fun total x => total + absInt (h x)) 0

#eval points.map (crosses 1)
#eval points.map (crosses 2)
#eval points.map (crosses 4)
#eval eventCount 2
#eval l1Numerator

example : eventCount 2 = 1 := by decide
example : l1Numerator = 7 := by decide
example : 2 * eventCount 2 ≤ l1Numerator := by decide

Run it with:

source "$HOME/.elan/env"
elan run leanprover/lean4:v4.32.0 lean WeakTypeTutorial.lean

The threshold-\(2\) event count should be \(1\), and the unnormalized \(L^1\) numerator should be \(7\). Multiplying the probability inequality by the common denominator \(4\) yields the checked integer inequality \(2\cdot1\leq7\). This imports only Std; it does not formalize measures, integrals, or the maximal theorem.

import NonlinearDynamics.Random.RandomCocycles.PointwiseBirkhoff

open NonlinearDynamics.Random.RandomCocycles

#check abs_birkhoffAverage_le_birkhoffAverage_abs
#check birkhoffAverageAbsoluteExceedanceSet
#check mem_birkhoffAverageAbsoluteExceedanceSet_iff
#check birkhoffAverageAbsoluteExceedanceSet_subset
#check measureReal_birkhoffAverageAbsoluteExceedanceSet_le
#check measureReal_birkhoffCauchyExceptionalSet_le

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

Related concepts

• Finite maximal ergodic inequality supplies the horizon-uniform finite estimate upstream of the infinite event.
• Infinite-horizon Birkhoff-average exceedance event explains the exact positive-time existential event and its one-sided weak bound.
• Birkhoff Cauchy exceptional set shows how the absolute estimate controls persistent tail separation.
• Birkhoff convergence event is the final set entered after the reciprocal-scale Cauchy argument.
• Almost everywhere explains the null-set language used in the closure step.

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 gives the historical transformation maximal theorem. Its assumptions and notation are not identical to the RMT-26 interface.

Kôsaku Yosida. Ergodic theorems of Birkhoff-Khintchine’s type, Japanese Journal of Mathematics 17, 31-36, 1940. Pages 33-34 combine maximal control with a dense-class closure argument.

Adriano Garsia. A Simple Proof of E. Hopf’s Maximal Ergodic Theorem, Journal of Mathematics and Mechanics 14(3), 381-382, 1965. This short paper is a primary source for the finite-maximum proof style upstream of the repository’s finite event inequality.

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, with arXiv:math/0608251. The paper treats a possibly noninvertible measure-preserving transformation on a probability space and cleanly separates maximal control from the convergence corollary.

Mathlib contributors. Finite-measure real-valued measure interface and the pinned Mathlib 4.32.0 tree at commit 81a5d257. These interfaces make the finiteness boundary of the real-valued estimate explicit.

Nonlinear Dynamics in Lean contributors. InfiniteHopfMaximal.lean and PointwiseBirkhoff.lean, the checked sources for the one-sided and absolute event bounds.