Orbit-majorant centering

Start with a three-state orbit

Take the finite state space \(\Omega=\{a,b,c\}\). Let one time step move cyclically,

and attach the one-step readings

Starting at \(a\), the readings are \(3,-1,2,3,\ldots\). Their first \(n\)-term orbit sum is

Now subtract the triangular penalty

and define a finite-time process

This is a real, checkable example of a shifted-subadditive process. That phrase means that the value over a combined time interval is at most the value over the first interval plus the value over the shifted second interval:

Indeed, orbit sums split exactly, while

Therefore

The nonnegative number \(mn\) is the visible slack in the inequality. No measure, probability, limit, or integrability argument is hiding in this calculation.

Compute the majorant and remainder

The one-step value of this process is

So the orbit sum of \(X_1\) is exactly \(S_n\). It is a majorant, or pointwise upper bound, because

Orbit-majorant centering subtracts that upper bound:

At the starting state \(a\), every term can be checked by hand:

The normalized column checks the identity

at several positive horizons. The last summand is the finite Birkhoff average of the one-step observable. The identity is arithmetic; it does not say that any term has a limit.

Why this is not expectation centering

Put the uniform probability measure on the three states, so each state has probability \(1/3\). An expectation is then the ordinary average of the three values. At horizon two,

and hence

Expectation centering subtracts this one scalar from every sample:

Those three values average to zero, but one is positive. Orbit-majorant centering subtracts the sample-dependent orbit sums \(S_2(a)=2\), \(S_2(b)=1\), and \(S_2(c)=5\), giving

These values are pointwise nonpositive, but their expectation is \(-1\), not zero. The two operations solve different problems:

Expectation centering requires a measure and enough integrability to define the expectation. Orbit-majorant centering is finite pointwise algebra and needs neither. Merely subtracting a different expected value at each horizon also does not preserve the original pointwise subadditive inequality automatically.

The general construction

Let \(\Omega\) be any state space, let \(T:\Omega\to\Omega\) advance the state by one time step, and let \(X:\mathbb N\to\Omega\to\mathbb R\) be a process. Its one-step orbit sum is

Mathlib’s finite definition and its exact addition law supply this algebra (official documentation, pinned source).

The project defines

The name orbit-majorant centering is project terminology. It records both the orbit sum being subtracted and the theorem that this sum bounds a shifted-subadditive process at positive horizons. In Lean, the definition itself is more neutrally named centeredProcess.

In Lean: define the centered process

centeredProcess T X n ω

The exact project definition is:

def centeredProcess {Ω : Type uΩ} (T : Ω → Ω) (X : ℕ → Ω → ℝ)
    (n : ℕ) (ω : Ω) : ℝ :=
  X n ω - birkhoffSum T (X 1) n ω

In Lean: use the one-step majorant

hX.oneStepBirkhoffMajorant_of_ne_zero n hn ω

Subtracting the upper bound proves centeredProcess T X n ω ≤ 0 for n ≠ 0. The additive splitting law for birkhoffSum also proves that the centered family remains shifted-subadditive.

In Lean: split the normalized value

normalized_eq_centered_add_birkhoffAverage n ω

A tiny standalone Lean/Std worksheet

Standalone tutorial. This complete file reproduces the three-state arithmetic with integers and exact rational numbers. It imports Std, not Mathlib or this repository. Save it as OrbitMajorantTutorial.lean in a scratch directory.

import Std

namespace OrbitMajorantTutorial

inductive State where
  | a | b | c
deriving Repr, DecidableEq

def step : State → State
  | .a => .b
  | .b => .c
  | .c => .a

def reading : State → Int
  | .a => 3
  | .b => -1
  | .c => 2

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

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

def penalty : Nat → Nat
  | 0 => 0
  | n + 1 => penalty n + n

def process (n : Nat) (x : State) : Int :=
  orbitSum n x - Int.ofNat (penalty n)

def centered (n : Nat) (x : State) : Int :=
  process n x - orbitSum n x

def normalized (z : Int) (n : Nat) : Rat :=
  (z : Rat) / (n : Rat)

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

def processMean (n : Nat) : Rat :=
  let total : Int := states.foldl (fun s x => s + process n x) 0
  (total : Rat) / 3

def expectationCentered (n : Nat) (x : State) : Rat :=
  (process n x : Rat) - processMean n

def subadditiveSlack (m n : Nat) (x : State) : Int :=
  process m x + process n (iterate m x) - process (m + n) x

#eval (List.range 5).map (fun n => orbitSum n .a)
#eval (List.range 5).map (fun n => process n .a)
#eval (List.range 5).map (fun n => centered n .a)
#eval states.map (fun x => process 2 x)
#eval states.map (expectationCentered 2)

example : (List.range 5).map (fun n => orbitSum n .a) =
    [0, 3, 2, 4, 7] := by decide

example : (List.range 5).map (fun n => centered n .a) =
    [0, 0, -1, -3, -6] := by decide

example : subadditiveSlack 2 3 .b = 6 := by decide

example : normalized (process 4 .a) 4 = (1 : Rat) / 4 := by native_decide

example : normalized (process 4 .a) 4 =
    normalized (centered 4 .a) 4 + normalized (orbitSum 4 .a) 4 := by
  native_decide

example : states.map (expectationCentered 2) =
    [(-2 : Rat) / 3, (-5 : Rat) / 3, (7 : Rat) / 3] := by native_decide

end OrbitMajorantTutorial

From the directory containing the file, a human types:

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

This exact worksheet was executed successfully with Lean 4.32.0 while editing this page. Its first three outputs were [0, 3, 2, 4, 7], [0, 3, 1, 1, 1], and [0, 0, -1, -3, -6]. The next output was [1, 0, 4]; the final output displayed [(-2 : Rat)/3, (-5 : Rat)/3, (7 : Rat)/3]. The integer examples use decide, while the rational equalities deliberately use native_decide so Lean evaluates normalized rational arithmetic. This bounded worksheet is suitable for an ordinary Mac or Linux machine.

Try the exact declarations in the project

import NonlinearDynamics.Random.RandomCocycles.SubadditiveCentering

open NonlinearDynamics.Random.RandomCocycles

#check centeredProcess
#check centeredProcess_zero
#check centeredProcess_one
#check IsIntegrableSubadditiveProcessCandidate.oneStepBirkhoffMajorant_of_ne_zero
#check IsIntegrableSubadditiveProcessCandidate.oneStepBirkhoffMajorant
#check IsIntegrableSubadditiveProcessCandidate.centeredProcess_nonpos_of_ne_zero
#check IsIntegrableSubadditiveProcessCandidate.centeredProcess_nonpos
#check IsIntegrableSubadditiveProcessCandidate.centeredProcess_add_le
#check IsIntegrableSubadditiveProcessCandidate.integrable_centeredProcess
#check IsIntegrableSubadditiveProcessCandidate.centeredProcess_candidate
#check normalized_eq_centered_add_birkhoffAverage
#check DiscreteMatrixCocycle.centeredLogPlusNormObservable
#check DiscreteMatrixCocycle.centeredLogPlusNormObservable_nonpos
#check DiscreteMatrixCocycle.centeredLogPlusNormObservable_add_le

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

Boundary cases and assumption ledger

The time-zero premise is genuinely necessary for a uniform sign theorem. The constant process \(X_n(\omega)=1\) is shifted-subadditive because \(1\le1+1\), but its centered time-zero value is \(Y_0(\omega)=X_0(\omega)=1\). At one step, by contrast, \(Y_1=X_1-X_1=0\) for every process.

The word majorant is also narrow. It says that the orbit sum lies above \(X_n\) at the same sample and horizon. It does not say the bound is close, least possible, or bounded away from \(-\infty\) after subtraction. In the worked example the negative gap grows quadratically.

Matrix-cocycle specialization

For a discrete matrix cocycle, the project applies the same construction to the finite-time log-positive norm observable. Its one-step Birkhoff sum is the already defined orbitLogPlusSum. The resulting centeredLogPlusNormObservable is pointwise nonpositive and remains shifted-subadditive. The hypothesis HasIntegrableGeneratorLogPlus enters only when the result promises an integrable process candidate.

This specialization still uses a log-positive envelope. It records expansion above norm one and deliberately discards signed contraction. A centered log-positive remainder is not a signed Lyapunov exponent.

What this term does not claim

Orbit-majorant centering establishes finite algebra. By itself it does not establish:

• expectation zero or statistical unbiasedness;
• a lower bound or absolute-value bound for the centered process;
• convergence pointwise, almost everywhere, in probability, in distribution, or in \(L^1\);
• convergence of the Birkhoff average in the normalized identity;
• Birkhoff’s pointwise ergodic theorem or Kingman’s subadditive ergodic theorem;
• equality between a samplewise limit and an integrated growth rate;
• permission to exchange a limit and an integral;
• probability normalization, ergodicity, independence, mixing, or decay of correlations; or
• a signed logarithmic growth rate, Lyapunov exponent, or Oseledets splitting.

The finite reduction is one ingredient in standard routes toward subadditive ergodic theorems. The later limit arguments require their own hypotheses and proofs (Karlsson and Margulis, Lalley).

Where to continue

The Birkhoff sum entry develops the finite sum, its indexing, and its addition law. The phase averaging entry uses the centered remainder in the next finite block estimate.

The Development Notebook maps the declarations to their checked proof architecture. The full Deep Dive develops the longer route toward subadditive ergodic theory. Both are public working notes and remain distinct from this glossary definition.

References

Mathlib contributors. Birkhoff sums, Mathlib 4 documentation. This official page defines the finite orbit sum and states its zero, one, successor, and addition laws.

Mathlib contributors. Pinned Birkhoff-sum source, Mathlib commit 81a5d257. These lines define birkhoffSum and prove the finite identities used by the project.

Mathlib contributors. Pinned Birkhoff-average source, Mathlib commit 81a5d257. The source defines normalization by the inverse natural-number cast and proves that the zero-time average is zero.

Anders Karlsson and Gregory A. Margulis. A Multiplicative Ergodic Theorem and Nonpositively Curved Spaces, Communications in Mathematical Physics 208(1), 107-123, 1999, doi:10.1007/s002200050750. On printed page 117, the proof subtracts the additive one-step orbit cocycle from a general subadditive cocycle before later ergodic arguments.

Steven P. Lalley. Kingman’s Subadditive Ergodic Theorem, lecture notes, 3 pages, accessed 2026-07-21. Page 1 writes the same one-step subtractive reduction and uses Birkhoff’s theorem only later.

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