Finite Block Decomposition for Subadditive Processes

Begin with eleven weights and make both cuts

Take the finite state space

and advance one state cyclically:

Attach these nonnegative one-step weights:

Interpret these integers as real weights.

Starting at state \(s\), define the finite process

The zero-step sum is empty, so \(X_0(s)=0\). This process is additive:

Every additive process is subadditive because equality implies the required upper bound. We use additivity only to make the example’s arithmetic exact. The project theorem assumes the weaker inequality.

If this finite space is given its uniform probability measure, every displayed finite-horizon function is integrable and the cyclic base preserves the measure. Probability is convenient for this model, not an assumption of the pointwise block theorems.

Choose:

Natural-number division gives:

The arithmetic identity is

The eleven observed weights from state zero are

and their total is

Orientation one: complete blocks first

Cut the horizon as

The first block starts at state \(0\), the second at \(T^4(0)=4\), and the terminal remainder at \(T^8(0)=8\):

Thus

For a merely subadditive process, the checked theorem replaces this equality with \(\le\).

Orientation two: remainder first

The same natural number is also

Now the three-step remainder stays at the original state, and the complete blocks begin at \(T^3(0)=3\):

Again,

The same eleven times were partitioned differently. The real summands may be written in any arithmetic order, but their starting states cannot be moved freely.

The wrong shift fails numerically

Suppose we keep the two correct block sums \(12\) and \(18\) but evaluate the three-step terminal remainder back at the original state. That wrong term is \(X_3(0)=8\), not \(X_3(T^8 0)=10\). The proposed bound becomes

which is false.

The analogous wrong remainder-first calculation also fails. If the initial remainder is \(8\) but the two blocks incorrectly restart at states \(0\) and \(4\), the right side is

Moving a remainder from one end of the horizon to the other changes the starting state of every later term. Shifted subadditivity records exactly that temporal information.

Time-zero boundary: subadditive does not mean normalized

Consider the constant process

for every horizon and state. It is subadditive:

On the same finite space with its uniform probability measure, every \(Y_n\) is integrable, so this process also fits the public candidate package.

But \(Y_0(s)=5\), not zero. With zero complete blocks, an exact-block estimate without a normalization premise would say

or

That is false. This is why the uniform exact-block theorem takes \(X_0=0\). The two remainder theorems do not need that premise: when the block count is zero, the remainder is the whole horizon and the inequality becomes reflexive.

Zero block length: valid but degenerate

Lean’s natural-number operations are total:

At \(b=0\), the terminal quotient-and-remainder theorem reduces to

The statement remains true, but zero is not a useful coarse-graining scale. To claim that \(r=n\bmod b\) is strictly shorter than \(b\), one must add the separate premise \(b\gt0\).

Name the objects before climbing

Fix a measurable space \(\Omega\), a measure \(\mu\), a base map \(T:\Omega\to\Omega\), and a real process

The inherited structure

IsIntegrableSubadditiveProcessCandidate T μ X

stores exactly:

1. Integrable (X k) μ for every finite \(k\); and
2. the shifted subadditive inequality for every \(m,k,\omega\).

It does not store:

• that \(\mu\) is a probability measure ;
• that \(T\) preserves \(\mu\);
• that \(T\) is ergodic ;
• independence or mixing;
• uniform control as \(n\) varies; or
• any pointwise, almost-everywhere, or integrated limit.

The word “integrable” concerns each fixed finite function. It does not turn a finite family into an asymptotic theorem.

Choose a route up

Learning objectives

By the summit, you should be able to:

1. compute \(11/4=2\) and \(11\bmod4=3\);
2. reproduce both exact \(40\)-unit ledgers;
3. explain why their block starting states differ;
4. reject the false \(40\le38\) unshifted bound;
5. state shifted subadditivity with the later term at \(T^m\omega\);
6. expand a finite Birkhoff sum along the powered map \(T^b\);
7. derive the terminal-remainder inequality by induction on \(q\);
8. derive the remainder-first inequality by one outer split;
9. read both quotient-and-remainder identities;
10. distinguish the valid \(b=0\) statement from a short-remainder claim;
11. prove that subadditivity forces \(X_0\ge0\);
12. explain why it does not force \(X_0=0\);
13. identify which exact-block theorem avoids normalization by requiring \(q\ne0\);
14. identify which exact-block theorem accepts all \(q\) by assuming \(X_0=0\);
15. separate pointwise bounds from finite integrability;
16. explain why the generic integrability theorem asks only that \(T^b\) preserve \(\mu\);
17. distinguish measure preservation from probability and ergodicity;
18. run the exact local worksheet;
19. identify the three cocycle specializations and their assumptions; and
20. list every asymptotic conclusion still absent.

Camp one: read shifted subadditivity in the correct order

The process package stores:

add_le : ∀ m k ω, X (m + k) ω ≤ X k (T^[m] ω) + X m ω

The early \(m\)-step value is \(X_m(\omega)\). The later \(k\)-step value restarts at \(T^m\omega\).

In Lean: split an early block from a later block

hX.add_le m k ω

The source’s three private helpers read only this field. The public generic theorems are methods on the stronger package for convenience, but their pointwise proofs do not consume its integrable field.

Camp two: a Birkhoff sum is a finite container

Mathlib defines

In this chapter,

Therefore

The sum is finite. At \(q=0\), its index set is empty and its value is zero.

In Lean: sample one block observable along the powered base

birkhoffSum (T^[b]) (X b) q ω

Mathlib exposes two useful successor recurrences:

The private blocks-first induction uses the second orientation because it peels the first block and recurses from \(T^b\omega\).

Camp three: prove blocks first and leave the remainder last

The central private helper proves:

Base case: \(q=0\)

The horizon is \(r\). The Birkhoff sum is empty and \((T^b)^0\omega=\omega\), so the goal reduces to

No claim about \(X_0\) is needed.

Successor step

For \(q+1\) blocks, arithmetic rewrites

Shifted subadditivity peels the first full block:

Apply the induction hypothesis at \(T^b\omega\). Mathlib’s birkhoffSum_succ’ then packages the first block with the recursive sum, and the iterate successor identity moves the terminal remainder to the correct final state.

In Lean: invoke the terminal-remainder theorem

hX.le_birkhoffSum_blocks_add_remainder b q r ω

The opening example substitutes \(b=4,q=2,r=3,\omega=0\), producing the exact right side \(12+18+10\).

Camp four: let division choose q and r

For any naturals \(n,b\), the formal theorem states the total identity

Substituting \(q=n/b\) and \(r=n\bmod b\) into the terminal theorem gives:

In Lean: quotient form with the remainder last

hX.le_birkhoffSum_div_add_mod b n ω

Remainder first

Commutativity of natural addition also gives

But we cannot merely commute two real terms after proving the terminal formula. We must apply shifted subadditivity with the remainder as the early part. Complete blocks then start from \(T^{n\bmod b}\omega\).

In Lean: quotient form with the remainder first

hX.le_mod_add_birkhoffSum_div b n ω

The generic non-quotient declaration le_remainder_add_birkhoffSum_blocks takes explicit \(r,b,q\). The quotient declaration sets those values arithmetically.

Camp five: time zero needs its own ledger

Declaration 1: subadditivity forces nonnegativity

Set \(m=k=0\) in shifted subadditivity:

Subtracting \(X_0(\omega)\) gives

The theorem zero_nonneg records this pointwise fact.

Declaration 2: nonpositive is equivalent to zero

Because subadditivity already gives \(X_0\ge0\),

This is zero_eq_zero_iff_nonpos. The right-to-left direction combines the stored nonnegativity with the supplied nonpositivity.

Exact blocks with positive count

If \(q\ne0\), write \(q=q'+1\). The source proves

without assuming \(X_0=0\). A positive block count lets the helper represent an exact multiple using actual full blocks instead of an empty sum.

Exact blocks uniformly in \(q\)

To include \(q=0\), the source requires exact time-zero normalization.

In Lean: make the exact-block bound uniform

hX.le_birkhoffSum_blocks_of_zero hX0 b q ω

This is a good example of boundary-sensitive theorem design: expose a strong positive-count theorem and a convenient all-count theorem with the exact extra premise, rather than burdening every useful positive case.

Camp six: finite integrability needs the powered map

The pointwise inequalities above do not integrate anything. The generic integrability theorem starts from:

The \(j\)-th Birkhoff summand is

If \(T^b\) preserves \(\mu\), every iterate \((T^b)^j\) also preserves \(\mu\), so composition transports integrability. A finite sum of integrable functions is integrable.

In Lean: prove one finite block sum is integrable

hX.integrable_birkhoffSum_blocks b q hTb

Preservation, probability, and ergodicity are different

A measure-preserving map satisfies \(F_*\mu=\mu\). It allows integrability to be pulled along its iterates.

A probability measure additionally has total mass one. This normalization is irrelevant to a finite sum’s integrability.

Ergodicity says invariant measurable events are trivial up to null sets. It is an asymptotic rigidity property and is also irrelevant to the finite integrability proof.

Even if \(T\) is ergodic, \(T^b\) need not be ergodic. The source avoids that false inference entirely: it asks only for preservation of \(T^b\), and the cocycle specialization obtains it from preservation of \(T\).

Finite integrability is not uniform integrability

For every fixed \(q\), the \(q\)-term block sum is integrable. This does not give a bound uniform in \(q\), a uniformly integrable family , or permission to pass a limit through an integral.

The matrix-cocycle specialization

Let \(C\) be the project’s one-sided discrete complex matrix cocycle and set

RMT-15 already proved:

• the shifted subadditive inequality;
• \(X_0=0\), including empty matrix dimension; and
• finite-horizon integrability under the explicit one-step hypothesis HasIntegrableGeneratorLogPlus.

RMT-18 exports three cocycle declarations.

Exact block multiples

C.logPlusNormObservable (b * q) ω ≤
  birkhoffSum (C.base^[b])
    (C.logPlusNormObservable b) q ω

This pointwise inequality is uniform in \(q\), including zero, because the cocycle’s log-positive observable has the checked time-zero identity. It takes the cocycle directly and needs no integrability hypothesis.

Remainder-first quotient bound

C.logPlusNormObservable n ω ≤
  C.logPlusNormObservable (n % b) ω +
    birkhoffSum (C.base^[b])
      (C.logPlusNormObservable b) (n / b)
      (C.base^[n % b] ω)

This is also pointwise and hypothesis-free beyond the cocycle bundle. It uses the correct post-remainder starting sample.

Integrability of the finite block sum

hC.integrable_blockBirkhoffSum b q

Only this third declaration takes hC. It converts the finite log-positive family into the generic integrable subadditive candidate and uses

C.base_preserving.iterate b

to show that the powered block map preserves \(\mu\).

Empty matrix dimension

When the finite matrix index type is empty, every log-positive norm observable is zero. Both pointwise inequalities reduce to \(0\le0\), and the finite block sum is the zero function. No positive-dimension premise appears.

This is a genuine boundary theorem, not evidence about growth in a nonempty space.

Type the eleven-step ledger with Lean and Std

The exact project module uses Mathlib’s measurable spaces, integrability, function iterates, Birkhoff sums, and cocycles. The opening finite arithmetic can be checked without that dependency graph.

The worksheet below imports only Lean’s Std library. It implements the twelve-state base, the additive process, a finite block sum, both correct orientations, the wrong shift, the constant-five time-zero boundary, and Lean’s division-by-zero convention.

This is a bounded standalone tutorial. It is suitable for a normal macOS or Linux host and does not invoke Lake, Mathlib, or a project build.

Save the exact block below as /tmp/SubadditiveFiniteBlocksTutorial.lean:

import Std

namespace SubadditiveFiniteBlocksTutorial

def period : Nat := 12

def base (state : Nat) : Nat :=
  (state + 1) % period

def iterateBase : Nat → Nat → Nat
  | 0, state => state
  | steps + 1, state => iterateBase steps (base state)

def weight (state : Nat) : Nat :=
  match state % period with
  | 0 => 2
  | 1 => 5
  | 2 => 1
  | 3 => 4
  | 4 => 3
  | 5 => 6
  | 6 => 2
  | 7 => 7
  | 8 => 1
  | 9 => 5
  | 10 => 4
  | _ => 6

/-- An additive process, hence a concrete subadditive process. -/
def process : Nat → Nat → Nat
  | 0, _ => 0
  | steps + 1, state => weight state + process steps (base state)

/-- The finite Birkhoff sum of one block observable along the powered base. -/
def blockSum (X : Nat → Nat → Nat) (blockLength : Nat) :
    Nat → Nat → Nat
  | 0, _ => 0
  | blocks + 1, state =>
      X blockLength state +
        blockSum X blockLength blocks (iterateBase blockLength state)

def horizon : Nat := 11
def blockLength : Nat := 4
def blockCount : Nat := horizon / blockLength
def remainderLength : Nat := horizon % blockLength
def start : Nat := 0

def terminalRemainderTotal : Nat :=
  blockSum process blockLength blockCount start +
    process remainderLength
      (iterateBase (blockLength * blockCount) start)

def initialRemainderTotal : Nat :=
  process remainderLength start +
    blockSum process blockLength blockCount
      (iterateBase remainderLength start)

def wrongUnshiftedRemainderTotal : Nat :=
  blockSum process blockLength blockCount start +
    process remainderLength start

def constantProcess (_steps _state : Nat) : Nat := 5

#eval (blockCount, remainderLength,
  blockLength * blockCount + remainderLength)

#eval (List.range horizon).map fun t =>
  weight (iterateBase t start)

#eval [process horizon start,
  process blockLength start,
  process blockLength (iterateBase blockLength start),
  process remainderLength
    (iterateBase (blockLength * blockCount) start)]

#eval [process remainderLength start,
  process blockLength (iterateBase remainderLength start),
  process blockLength
    (iterateBase (remainderLength + blockLength) start)]

#eval [terminalRemainderTotal,
  initialRemainderTotal,
  wrongUnshiftedRemainderTotal]

#eval [decide (process horizon start ≤ terminalRemainderTotal),
  decide (process horizon start ≤ initialRemainderTotal),
  decide (process horizon start ≤ wrongUnshiftedRemainderTotal)]

#eval (process 0 start,
  constantProcess 0 start,
  decide (constantProcess (blockLength * 0) start ≤
    blockSum constantProcess blockLength 0 start))

#eval (horizon / 0, horizon % 0,
  decide (process horizon start ≤
    blockSum process 0 (horizon / 0) start +
      process (horizon % 0)
        (iterateBase (0 * (horizon / 0)) start)))

example : blockCount = 2 := by decide
example : remainderLength = 3 := by decide
example : process horizon start = 40 := by decide
example : terminalRemainderTotal = 40 := by decide
example : initialRemainderTotal = 40 := by decide
example : ¬ process horizon start ≤ wrongUnshiftedRemainderTotal := by decide
example : process 0 start = 0 := by decide
example : ¬ constantProcess (blockLength * 0) start ≤
    blockSum constantProcess blockLength 0 start := by decide

end SubadditiveFiniteBlocksTutorial

Type this command:

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

The exact worksheet above was executed successfully with Lean 4.32.0 while editing this chapter. Its output was:

(2, 3, 11)
[2, 5, 1, 4, 3, 6, 2, 7, 1, 5, 4]
[40, 12, 18, 10]
[8, 15, 17]
[40, 40, 38]
[true, true, false]
(0, 5, false)
(0, 11, true)

Read the lines in order:

1. quotient \(2\), remainder \(3\), and reconstructed horizon \(11\);
2. the eleven one-step weights;
3. total \(40\), two blocks \(12,18\), and terminal remainder \(10\);
4. initial remainder \(8\) and shifted blocks \(15,17\);
5. both correct totals \(40\) and the wrong-shift total \(38\);
6. the two true upper bounds and the false \(40\le38\) proposal;
7. the normalized additive process has \(X_0=0\), while the constant process has \(Y_0=5\) and fails the zero-count exact-block test; and
8. at \(b=0\), quotient zero and remainder eleven produce a true reflexive bound.

The silent example declarations are kernel-checked proofs of the same finite facts.

This worksheet is a finite model, not the project theorem. It uses natural weights, one twelve-state cyclic base, hand-written recursion, and decidable concrete inequalities. It proves no result about arbitrary real processes, Mathlib Birkhoff sums, measurable spaces, integrability, preservation, matrix cocycles, or limits.

The complete twelve-declaration map

The module exposes twelve public declarations. Three private helpers support them but are not part of the public API.

The three private helpers are:

Assumption ledger

The generic pointwise methods have a receiver that stores integrability, but their proof bodies use only add_le. The page states that proof dependency explicitly while retaining the stronger receiver type of the public method.

Common wrong turns

Removing the base shift

The later \(k\)-step value starts at \(T^m\omega\). The opening \(40\le38\) failure shows that replacing it by the original sample can destroy the bound.

Using \(T\) instead of \(T^b\) in the block sum

Successive block observations are \(b\) one-step updates apart. The correct finite sum advances by the powered map.

Reversing function-iterate roles

(T^[b])^[q] means apply the \(b\)-step map \(q\) times. It reaches the same point as \(T^{bq}\), not \(T^{b+q}\).

Treating two orientations as one commutative rewrite

Real addition commutes, but sample points do not move with it. Remainder first requires shifting the block orbit by \(r\).

Requiring \(X_0=0\) for every remainder theorem

At \(q=0\), the remainder is the entire horizon. Both remainder bounds become reflexive without normalization.

Deleting \(X_0=0\) from the all-count exact-block theorem

The constant-five process is a counterexample at \(q=0\).

Saying \(n\bmod b\lt b\) at \(b=0\)

The strict remainder theorem needs \(b\gt0\). The project inequalities are total and valid at zero without claiming strict shortness.

Calling the remainder a uniformly bounded error

It has a shorter time length when \(b\gt0\). The module proves no numerical bound uniform over samples or block scales.

Pulling integrability through an arbitrary map

The composition step uses measure preservation of the powered map. Without a suitable nonsingularity or preservation hypothesis, an integrable observable can become nonintegrable after composition.

Assuming ergodicity passes to powers

Preservation passes from \(T\) to every \(T^b\). Ergodicity need not. The finite theorem asks only for the property it actually uses.

Reading finite integrability as convergence

An integrable sum for every fixed finite \(q\) is not a theorem about \(q\to\infty\), samplewise convergence, or exchange of limit and integral.

Calling log-positive blocking a Lyapunov theorem

The cocycle observable uses \(\log^+\), which erases contraction and singular collapse. Its finite block upper bound is not a signed growth exponent.

Exercises from first cut to theorem design

Trailhead

1. Recompute the eleven weights from the cyclic base.
2. Verify the blocks-first sums \(12,18,10\).
3. Verify the remainder-first sums \(8,15,17\).
4. Explain why the starting states are \(0,4,8\) in one orientation and \(0,3,7\) in the other.
5. Reproduce both false \(38\)-unit calculations.
6. Compute \(23/5\) and \(23\bmod5\), then sketch both temporal cuts.

Mid-mountain

7. Expand birkhoffSum (T^[4]) (X 4) 2 0 term by term.
8. Prove \((T^b)^q=T^{bq}\) on paper using function iteration.
9. Derive the blocks-first helper by induction on \(q\).
10. Derive the remainder-first helper by splitting \(r+bq\) once.
11. Show that \(X_0\ge0\) follows from subadditivity.
12. Give another subadditive process with \(X_0\gt0\).
13. Explain why positive \(q\) avoids the empty-sum obstruction.
14. Evaluate both quotient theorems at \(b=0\).

Summit

15. Rewrite declaration 9 as an explicit finite sum and identify the integrability proof for each summand.
16. Give a finite example where \(T^b\) preserves a measure even if no premise about \(T\) was supplied to the theorem.
17. Explain why probability mass one is irrelevant to finite-sum integrability.
18. Find an ergodic measure-preserving map whose square is not ergodic.
19. State a uniform-integrability claim that declaration 9 does not prove.
20. Design a later theorem that averages the block inequality over phases. List every new horizon-counting obligation.
21. State a candidate almost-everywhere limit theorem and list the probability, preservation, ergodicity, and integrability assumptions separately.
22. Explain why a signed Lyapunov exponent needs information discarded by \(\log^+\).

Inspect and check the exact project interfaces

import NonlinearDynamics.Random.RandomCocycles.SubadditiveFiniteBlocks

open MeasureTheory
open NonlinearDynamics.Random.RandomCocycles

#check IsIntegrableSubadditiveProcessCandidate.zero_nonneg
#check IsIntegrableSubadditiveProcessCandidate.zero_eq_zero_iff_nonpos
#check IsIntegrableSubadditiveProcessCandidate.le_birkhoffSum_blocks_add_remainder
#check IsIntegrableSubadditiveProcessCandidate.le_birkhoffSum_div_add_mod
#check IsIntegrableSubadditiveProcessCandidate.le_birkhoffSum_blocks_of_ne_zero
#check IsIntegrableSubadditiveProcessCandidate.le_birkhoffSum_blocks_of_zero
#check IsIntegrableSubadditiveProcessCandidate.le_remainder_add_birkhoffSum_blocks
#check IsIntegrableSubadditiveProcessCandidate.le_mod_add_birkhoffSum_div
#check IsIntegrableSubadditiveProcessCandidate.integrable_birkhoffSum_blocks
#check DiscreteMatrixCocycle.logPlusNormObservable_nat_mul_le_birkhoffSum
#check DiscreteMatrixCocycle.logPlusNormObservable_le_mod_add_blockBirkhoffSum
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.integrable_blockBirkhoffSum

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

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

Passing either technical gate would not complete the pending human or Pro review.

What is established and what remains outside

The exact achievement is finite:

A long shifted-subadditive process value can be upper-bounded by repeated observations at one block scale plus one correctly shifted remainder. With preservation of the powered map, each fixed finite block sum is integrable.

No limit appears in that statement.

Where to continue

The Birkhoff sum glossary entry is the compact definition and powered-orbit reference for the finite sum used here.

Probability Normalization and Ergodic Rigidity Before Kingman is the immediate predecessor. It keeps probability and ergodicity separate from the finite process candidate.

Integrated Log-Positive Cocycle Growth and Its Deterministic Fekete Limit explains a distinct deterministic limit taken only after integrating out the sample variable.

Finite Blocks Before Limits: Birkhoff Bounds for Subadditive Cocycles in Lean is the paired Development Notebook entry.

Orbit-Majorant Centering for Subadditive Processes is the immediate finite successor.

Finite Phase Averaging for Nonpositive Subadditive Processes later combines residue phases into a sliding finite base-orbit sum. That chapter must audit its own horizon and summand counts; the present module does not contain a phase average.

References

Nonlinear Dynamics in Lean. SubadditiveFiniteBlocks.lean. This is the authoritative twelve-declaration source described here.

Mathlib contributors. Birkhoff sums, Mathlib 4 documentation. The pinned source defines the finite sum and its zero, successor, and addition identities.

Mathlib contributors. Function iteration, Mathlib 4 documentation. This official source provides zeroth, successor, added, and multiplied iterate identities.

Lean and Mathlib contributors. Natural-number division, Lean and Mathlib documentation. This is the upstream interface for Nat.div_add_mod, Nat.mod_add_div, and the total zero-divisor conventions.

Mathlib contributors. Measure-preserving maps, Mathlib 4 documentation. This source defines preservation and proves it is stable under natural iteration.

Mathlib contributors. Integrable functions, Mathlib 4 documentation. This source provides composition with a measure-preserving map and closure under finite sums.

J. F. C. Kingman. The ergodic theory of subadditive stochastic processes, Journal of the Royal Statistical Society: Series B 30(3), 499–510, 1968. This primary source supplies the asymptotic context. The current module proves only finite block infrastructure.

J. Michael Steele. Kingman’s subadditive ergodic theorem, Annales de l’Institut Henri Poincaré, Probabilités et Statistiques 25(1), 93–98, 1989. This proof-lineage reference organizes a full argument through finite interval decompositions; it is not an upstream Lean theorem used here.

Harry Furstenberg and Harry Kesten. Products of Random Matrices, The Annals of Mathematical Statistics 31(2), 457–469, 1960. This primary source motivates the random-matrix destination. No samplewise conclusion from that work is claimed here.

The exact upstream Lean revision audited for this chapter is Mathlib commit 81a5d257, the revision pinned by formalization/lake-manifest.json. The project source file audited during this rebuild had SHA-256 07a4e6d99893d26e888d5799d15660cfd2b0c931bfdbabd6879f1d773ada2775.