Infinite-horizon Birkhoff-average exceedance event

Start with four equally likely states

The map \(T\) moves one step around the cycle

and the observable \(g:\Omega\to\mathbb R\) reads

An observable is a numerical reading attached to each state. The measure \(\mu\) is a probability measure because the four masses add to one. Every subset of this finite space is an event .

For a start \(x\), add the first \(n\) readings along its orbit and divide by \(n\):

The first expression is a Birkhoff sum . The second is its finite-time average. Fix the threshold

The question is deliberately modest: does the average cross \(1/2\) at least once at a positive finite time?

Work out every crossing

The exact first six averages are:

Bold entries strictly exceed \(1/2\). Thus \(x_0\) crosses at times \(1,2,5\), \(x_3\) crosses at time \(2\), and the other two starts do not cross in this table.

The table is enough only after we rule out later crossings. Each complete four-step block has sum

For any starting phase, deleting complete four-step blocks leaves a partial sum no larger than \(3\). Hence

The last inequality is not strict at its numerical upper bound, so it still excludes the required strict crossing. We have now checked every time, rather than only the six displayed times.

The at-least-once event is therefore

Three questions that sound similar but are not

For a fixed positive \(N\), compare these two tail questions:

The first says there is at least one witness at or after \(N\). The second says every time at or after \(N\) is a witness. A single symbol change, \(\exists\) to \(\forall\), changes the event drastically.

In the four-cycle example,

The sets \(F_N\) shrink because a later lower bound gives fewer possible witness times. Their intersection is the event of arbitrarily late, or infinitely many, strict crossings:

For \(G_N\), choose a multiple of four with \(n\ge N\). Its average is zero, so it does not exceed \(1/2\). Consequently \(G_N=\varnothing\) for every \(N\), and the eventually always above event is also empty:

The project event asks neither tail question. It asks only

so it is exactly \(F_1\). In this example that event has two points even though both stronger tail events are empty.

Prefix unions are different from tail intersections

For a finite upper horizon \(N\), define the prefix event

As \(N\) grows, a prefix search keeps all earlier witnesses, so these events increase. In the example,

The infinite-horizon event is their exact union:

The proof is elementary in both directions:

1. If \(x\in E_a(g)\), recover its finite witness time \(n\) and choose the finite horizon \(N=n\).
2. If \(x\in E_{N,a}(g)\) for some \(N\), keep the same witness \(n\) and remove only the upper bound \(n\le N\).

No measure, measurable structure, topology, integrability, or regularity of \(T\) is needed for this set equality.

Do not confuse the increasing prefix family \(E_{N,a}\) with the decreasing tail family \(F_N\). Their quantifiers are

What the limit superior can and cannot tell us

The limit superior , written \(\limsup_{n\to\infty}A_n\), records the largest value that a sequence keeps approaching along arbitrarily late times. It is a tail notion, unlike one early crossing.

For the four-cycle, complete four-step blocks contribute zero and every remaining partial sum has absolute value at most \(3\). Therefore

and dividing the bounded remainder by \(n\) gives

Therefore

for all four starts, including the two points in \(E_{1/2}(g)\). This is the central misconception guardrail: an infinite search for one finite witness does not describe the long-time limit.

For a real sequence with a well-defined finite limit superior, the safe logical implications are:

and

Strict inequality is lost in the reverse direction. The sequence \(a+1/n\) crosses \(a\) forever but has limit superior exactly \(a\). The sequence \(a-1/n\) also has limit superior \(a\) but never crosses \(a\). Likewise, eventual strict crossing at every time implies only that the limit inferior is at least \(a\), not necessarily strictly greater than \(a\).

General definition

Let \(\Omega\) be any state space, let \(T:\Omega\to\Omega\) be a discrete-time transformation, let \(g:\Omega\to\mathbb R\) be a real observable, and let \(a\in\mathbb R\). The infinite-horizon Birkhoff-average exceedance set is

The word infinite-horizon means that there is no fixed upper bound on the search. Every successful point still comes with one ordinary finite witness \(k\). The definition introduces no infinite-duration average and no real-valued maximum over all times.

The comparison is strict. If \(A_k g(\omega)=a\), time \(k\) is not a witness. Time zero is excluded because an average of zero observations should not create membership through a totalized library convention.

Measurability: two proof routes

A measurable space specifies which subsets may be treated as events, and a measurable function has measurable preimages of measurable value-space sets. The four-state example uses the discrete measurable structure, so every subset and every function is measurable.

The repository exposes two different general interfaces.

Ordinary measurable-set route

If \(T\) and \(g\) are measurable, every finite average is measurable. Each strict superlevel set is then measurable, and the countable prefix union is a measurable set:

Null-measurable route

Suppose instead that \(T\) is a measure-preserving transformation for a measure \(\mu\), and \(g\) is integrable . Then every positive-time average has enough almost-everywhere measurability for its strict superlevel set to agree with a measurable set outside a null set . A countable union preserves that property, so \(E_a(g)\) is null measurable with respect to \(\mu\).

This second conclusion is weaker than ordinary measurability and is stated as such in Lean. It needs no finite total mass, probability normalization, or ergodicity. It is an example of why almost-everywhere language must not be silently replaced by pointwise language.

Measures of the increasing finite events

A measure in Mathlib returns an extended nonnegative real: an ordinary nonnegative number together with a possible value \(\infty\). Continuity from below gives

in that extended number system. For this theorem, monotonicity of the prefix events is enough. The target may be infinite, and the checked interface does not require the sets themselves to be measurable.

Mathlib also defines a real-valued projection

written μ.real S in Lean. This totalized operation maps infinite mass to zero. It is therefore not continuous at \(\infty\). The repository’s real-valued convergence theorem uses the clean sufficient local condition

That condition is sufficient, not necessary for every special family.

Here is the failure mode it prevents. Under counting measure on the natural numbers, let \(H_N=\{0,\ldots,N-1\}\). Then \(H_N\uparrow\mathbb N\), but

because the union has infinite extended mass. The real sequence \(N\) does not converge to zero.

The weak measure bound, numerically first

Return to the uniform four-cycle. The positive part \(g^+(x)=\max\{g(x),0\}\) equals \(3\) at \(x_0\) and \(0\) elsewhere, so

We already found \(\mu(E_{1/2}(g))=1/2\). The multiplication form says

Dividing by the positive threshold gives

The right side can exceed one even on a probability space. The theorem is an upper bound, not a probability normalization formula and not an equality.

In general, if \(\mu\) is finite, \(T\) preserves \(\mu\), and \(g\) is integrable, the checked multiplication estimate is

This form is valid for every real \(a\). Division is order preserving only when \(a\gt0\), which yields

The numerator is the integral of the positive part, not the absolute value and not the integral of a centered observable.

In Lean

The definition says exactly that one positive natural time is a strict witness.

ω ∈ birkhoffAverageExceedanceSet T g a ↔\n  ∃ k, 1 ≤ k ∧ a < birkhoffAverage ℝ T g k ω

The exact checked definition and membership theorem are:

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

@[simp] theorem mem_birkhoffAverageExceedanceSet_iff
    {a : ℝ} {ω : Ω} :
    ω ∈ birkhoffAverageExceedanceSet T g a ↔
      ∃ k, 1 ≤ k ∧ a < birkhoffAverage ℝ T g k ω := by
  rfl

The exact prefix union is a separate theorem.

birkhoffAverageExceedanceSet T g a =\n  ⋃ N : ℕ, finiteBirkhoffAverageExceedanceSet T g N a

Ordinary measurability records its assumptions explicitly.

measurableSet_birkhoffAverageExceedanceSet hT hg a

The measure limit stays in extended nonnegative reals unless a finite target licenses the real projection.

tendsto_measure_finiteBirkhoffAverageExceedanceSet (T := T) (g := g) (μ := μ) a

Finally, positivity appears exactly where the multiplication estimate is divided by \(a\).

measureReal_birkhoffAverageExceedanceSet_le hT hg ha

The exact checked theorem is:

theorem measureReal_birkhoffAverageExceedanceSet_le
    [IsFiniteMeasure μ]
    (hT : MeasurePreserving T μ μ) (hg : Integrable g μ)
    {a : ℝ} (ha : 0 < a) :
    μ.real (birkhoffAverageExceedanceSet T g a) ≤
      (∫ ω, max (g ω) 0 ∂μ) / a

Standalone tutorial

Standalone tutorial. This worksheet imports only Lean’s Std library. It does not import Mathlib or this project. It computes integer orbit sums for the exact four-cycle above. At positive time \(n\), the threshold test

is encoded without fractions as \(n\lt2S_n\).

Save this as InfiniteHorizonExceedanceWorksheet.lean in a temporary directory outside the repository:

import Std

namespace InfiniteHorizonExceedanceWorksheet

inductive Point where
  | p0
  | p1
  | p2
  | p3
deriving Repr, DecidableEq

def points : List Point := [.p0, .p1, .p2, .p3]

def step : Point → Point
  | .p0 => .p1
  | .p1 => .p2
  | .p2 => .p3
  | .p3 => .p0

def reading : Point → Int
  | .p0 => 3
  | .p1 => -1
  | .p2 => -1
  | .p3 => -1

def sumFrom : Nat → Point → Int
  | 0, _ => 0
  | n + 1, x => reading x + sumFrom n (step x)

def crossesAt (n : Nat) (x : Point) : Bool :=
  decide (1 ≤ n ∧ Int.ofNat n < 2 * sumFrom n x)

def crossesThrough (upper : Nat) (x : Point) : Bool :=
  (List.range (upper + 1)).any fun n => crossesAt n x

def crossesBetween (lower upper : Nat) (x : Point) : Bool :=
  (List.range (upper + 1)).any fun n =>
    decide (lower ≤ n) && crossesAt n x

def firstSixSums (x : Point) : List Int :=
  (List.range 6).map fun j => sumFrom (j + 1) x

#eval firstSixSums .p0
#eval firstSixSums .p3
#eval points.filter (crossesThrough 0)
#eval points.filter (crossesThrough 1)
#eval points.filter (crossesThrough 2)
#eval points.filter (crossesBetween 3 12)
#eval points.filter (crossesBetween 6 12)

example : firstSixSums .p0 = [3, 2, 1, 0, 3, 2] := by decide
example : firstSixSums .p3 = [-1, 2, 1, 0, -1, 2] := by decide
example : points.filter (crossesThrough 0) = [] := by decide
example : points.filter (crossesThrough 1) = [.p0] := by decide
example : points.filter (crossesThrough 2) = [.p0, .p3] := by decide
example : points.filter (crossesBetween 3 12) = [.p0] := by decide
example : points.filter (crossesBetween 6 12) = [] := by decide

end InfiniteHorizonExceedanceWorksheet

From that temporary directory, a human with the pinned Lean toolchain already installed can type:

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

The first two evaluations print the partial sums \([3,2,1,0,3,2]\) and \([-1,2,1,0,-1,2]\). The next three print the prefix events \(\varnothing\), \(\{x_0\}\), and \(\{x_0,x_3\}\). The last two search the displayed tail window: \(x_0\) still has its time-five witness when the lower bound is three, and no point has a witness from six through twelve. The paper bound \(S_n\le3\) proves the stronger statement for every \(n\ge6\); the finite program is not presented as a proof about infinitely many times. This exact worksheet was executed successfully with the pinned Lean 4.32.0 compiler; it imports only Std and does not load the project or Mathlib.

Try it in the repository

import NonlinearDynamics.Random.RandomCocycles.InfiniteHopfMaximal

open MeasureTheory Set Filter
open NonlinearDynamics.Random.RandomCocycles

#check birkhoffAverage
#check finiteBirkhoffAverageExceedanceSet
#check mem_finiteBirkhoffAverageExceedanceSet_iff
#check finiteBirkhoffAverageExceedanceSet_mono
#check birkhoffAverageExceedanceSet
#check mem_birkhoffAverageExceedanceSet_iff
#check birkhoffAverageExceedanceSet_eq_iUnion_finite
#check finiteBirkhoffAverageExceedanceSet_subset
#check measurableSet_birkhoffAverageExceedanceSet
#check nullMeasurableSet_birkhoffAverageExceedanceSet_of_integrable
#check tendsto_measure_finiteBirkhoffAverageExceedanceSet
#check tendsto_measureReal_finiteBirkhoffAverageExceedanceSet
#check birkhoffAverageExceedanceSet_posPart_bound
#check measureReal_birkhoffAverageExceedanceSet_le

#check MeasureTheory.tendsto_measure_iUnion_atTop
#check MeasureTheory.Measure.real
#check ENNReal.tendsto_toReal

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

Boundary cases and nonclaims

• Horizon zero: \(E_{0,a}(g)=\varnothing\) because no natural time satisfies \(1\le k\le0\).
• Equality: \(A_k g(\omega)=a\) is not a crossing. Replacing \(\lt\) by \(\le\) defines a different event.
• Zero observable: if \(g=0\) and \(a\ge0\), the event is empty. If \(a\lt0\), time one witnesses every point, so the event is all of \(\Omega\).
• Negative threshold: the multiplication estimate remains valid, but its left side is nonpositive and may convey little information. Division needs \(a\gt0\).
• Infinite mass: extended-measure continuity still works. Unconditional passage through Measure.real does not.
• Null measurability: this is agreement with a measurable set outside a null set, not automatically ordinary measurability.

Membership in \(E_a(g)\) does not assert:

• convergence of the Birkhoff averages;
• any value for their limit superior or limit inferior;
• arbitrarily late or infinitely many crossings;
• eventual crossing at every time;
• invariance of the event under \(T\);
• probability zero or one;
• ergodicity, mixing, or independence;
• injectivity, surjectivity, or invertibility of \(T\);
• existence of a real-valued maximum over all times;
• a strong \(L^p\) maximal inequality;
• the pointwise Birkhoff or Kingman ergodic theorem; or
• a Lyapunov exponent or an Oseledets splitting.

The weak estimate controls the measure of one event. It does not, by itself, prove a long-time convergence theorem.

Where to continue

The finite maximal ergodic inequality supplies the uniform finite-horizon bound that is passed through the exact increasing union. The Birkhoff convergence event asks whether the whole average sequence converges, which is a different predicate.

From Finite Maximal Bounds to an Infinite Weak Estimate develops the proof architecture as a textbook chapter. The matching checked implementation narrative is Infinite-Horizon Birkhoff-Average Exceedance Bounds in Lean.

Repository milestone 24 (RMT-24) is the current formalized scope: the event, its finite union, two measurability routes, extended and locally finite real measure limits, and the weak measure estimate. It does not include a pointwise ergodic theorem.

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. Their Theorem 2 gives the historical infinite-horizon maximal-ergodic setting. It is not claimed as the exact source of the repository’s increasing-union proof.

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. Pages 248-249 give a close primary precedent for passing from finite strict average events to an infinite maximal statement in a probability-space argument.

Mathlib contributors. Continuity from below for increasing sets and continuity of extended-nonnegative-real conversion away from infinity, Mathlib 4.32.0. These are the exact limit interfaces used by RMT-24.

Mathlib contributors. Definition of Measure.real, Mathlib 4.32.0. The source records explicitly that infinite measure is mapped to zero.

The exact upstream Lean source audited for this page is Mathlib commit 81a5d257, the revision pinned by formalization/lake-manifest.json.