Subadditive Upper Limsup Bounds Before Kingman Convergence

Base camp: a fixed block computes the exact upper edge

Take the two-point probability space

and let \(T\) swap the points. Define a small potential

Now define a real process by

This is not an invented sequence of unrelated rows. The endpoint terms telescope across a split:

The only inequality is \(\lceil(m+n)/2\rceil\le\lceil m/2\rceil+\lceil n/2\rceil\). Thus \(X\) is a genuine shifted-subadditive process.

Compute both paths before generalizing

Because \(T^n\) is the identity at even \(n\) and the swap at odd \(n\),

Every entry is nonnegative. The first nine horizons are:

Lean totalizes division by zero, so the displayed \(n=0\) normalized values are zero. The asymptotic claim concerns positive horizons.

At \(a\), the odd normalized values are

at \(b\), they are

The even values are exactly \(1/2\). Hence both paths converge to \(1/2\), and in particular

Now choose the fixed block \(b=2\). The two block values are both one, so

The RMT-29 inequality is sharp:

The direction matters. It says the eventual upper edge of the sample path cannot exceed the block integral ratio. It does not say that every finite normalized value is at most \(1/2\): the table contains \(2\), \(1\), and \(4/5\).

See the centered proof inside the same numbers

The one-step observable is

Along either alternating orbit, its Birkhoff averages converge to the uniform integral \(1\). Subtract its orbit sum:

For both starting points,

The centered integral identity at block two is now visible without symbols hiding the arithmetic:

The limiting centered contribution is

and adding the one-step Birkhoff limit gives

For phase averaging, write \(n=2a+r\) with \(r=0\) or \(1\). The proof keeps the prefix \(2(a-1)\), one block shorter than the target. Its coefficient is

Both residue lanes therefore use Birkhoff averages under the original flip \(T\). This is essential: \(T\) is ergodic, while \(T^2\) is the identity and is not ergodic.

The measure vocabulary is concrete here. A probability measure has total mass one. A measure-preserving transformation keeps event masses unchanged under preimage. A statement holds almost everywhere if it may fail only on a null set . On this uniform two-point space, the empty set is the only null set, so an almost-everywhere statement holds at both points.

Let \((\Omega,\mu,T)\) be an ergodic probability-preserving system and let

be an integrable subadditive process. Its defining inequality has the form

The asymptotic quantity of interest is the normalized samplewise process

Kingman’s theorem gives far more than this chapter: under its hypotheses it identifies an almost-sure limit (Kingman 1968). The RMT-29 layer stops at a precise earlier summit. Its generalized theorem assumes that the normalized path is eventually bounded below almost everywhere. For each positive block size \(b\), it proves

Pointwise nonnegativity is a sufficient, simpler way to discharge that lower-bound gate, and the module retains it as a compatibility wrapper. The log-positive cocycle process uses that wrapper.

For the cocycle log-positive process, intersecting these full-measure events over all blocks and taking the deterministic infimum gives

Here \(\gamma^+_\mu(C)\) is the integrated Fekete rate formalized earlier. This is a samplewise upper estimate. It is not convergence, a lower bound, a signed Lyapunov exponent, or an Oseledets theorem.

The immediate formal predecessors are Finite Phase Averaging for Nonpositive Subadditive Processes, Ergodic Birkhoff Limits and Normalized Space Averages, and the glossary entries on phase averaging , limit superior , and integrated log-positive growth rates . For broader proof lineage, Steele gives a conceptually algorithmic full proof that begins with a Birkhoff-based centering reduction and then uses an interval-decomposition argument (Steele 1989).

Learning objectives

By the end, a reader should be able to:

1. explain why a fixed-block proof must control all residue classes;
2. derive the centered process and reconstruct the normalized original process;
3. explain why ordinary \(T\)-Birkhoff averages replace powered-map averages;
4. calculate the coefficient left by phase averaging;
5. identify where probability and the eventual-lower-bound gate enter, and explain why pointwise nonnegativity is only one sufficient wrapper;
6. distinguish a limsup upper bound from a convergence theorem;
7. optimize a countable family of block bounds using a deterministic Fekete rate;
8. read the RMT-29 public theorem surface and its proof obligations; and
9. audit examples that prevent stronger interpretations.

The two obstacles

Subadditivity is not additivity

For an observable \(f\), the Birkhoff sum

satisfies an exact addition law. A subadditive process supplies only an upper comparison. Its future block begins at the shifted point \(T^m\omega\), and repeated decomposition leaves boundaries whose signs matter.

The one-step case nevertheless provides a universal majorant:

This controls the sequence from above and later supplies the boundedness needed by a real-valued limsup lemma.

Ergodicity need not pass to powers

A tempting block proof studies \(X_b\) along

and invokes Birkhoff for \(T^b\). That route silently needs \(T^b\) to be ergodic. It can fail even when \(T\) is ergodic. On the two-point probability space, the flip is ergodic but its square is the identity, so the square has nontrivial invariant events.

Finite phase averaging repairs the proof. It combines the \(b\) starting phases before taking limits and rewrites the result as an ordinary Birkhoff sum under \(T\). The asymptotic theorem is therefore applied only to the map whose ergodicity is actually assumed. Lalley’s teaching notes motivate this ordinary-map route (Lalley notes); the limiting input is the checked modern form of Birkhoff’s theorem (Birkhoff 1931).

Center before taking blocks

Define the one-step-centered process

The one-step majorant gives \(Y_n\le0\) for positive \(n\). This sign is the entry ticket to the finite phase-averaging theorem. Centering does not claim that \(Y\) is zero, additive, or nonnegative.

The original process is recovered exactly:

where \(A_n\) is the ordinary Birkhoff average. The proof will bound the first term by block averages of \(Y_b\), then let the second term converge by RMT-28.

Integration respects this decomposition. Measure preservation and integrability imply

and hence

The second identity is the cancellation mechanism at the end of the limit calculation.

Residues recover the full sequence

Fix a positive block size \(b\). Every natural time has a unique residue modulo \(b\), so it is enough to prove an eventual estimate along every arithmetic progression

For large \(a\), set

The finite phase theorem gives the pointwise estimate

The lost block is deliberate. It absorbs the phase boundaries that cannot be discarded merely from subadditivity. Dividing by \(ba+r\gt0\) yields

There are now two independent limits:

and

The first uses ergodic Birkhoff convergence for the original map \(T\). The second is elementary real asymptotics. Meanwhile,

Adding the limits and inserting the centered integral identity gives

Because there are only finitely many residues, an eventual estimate on each progression becomes an eventual estimate on all sufficiently large natural times. In Lean, Eventually.atTop_of_arithmetic packages this passage (pinned Mathlib source).

From eventual estimates to limsup

The limsup is an order-theoretic tail operator. In \(\mathbb R\), applying limsup_le_iff requires enough boundedness to keep the result in the conditionally complete order (pinned Mathlib source).

The upper bound comes from the one-step majorant:

and the Birkhoff average converges almost everywhere. The lower bound in the generalized public theorem is supplied directly:

In Lean this is the IsBoundedUnder (· ≥ ·) atTop premise. The relation is written with \(\ge\) because a lower bound \(L\) satisfies \(X_n(\omega)/n\ge L\) eventually. The nonnegative wrapper chooses \(L=0\). The generalized theorem also accepts signed processes whose normalized paths have some other almost-everywhere lower bound.

The nearby countermodel: \(Z_n=-n^2\)

The lower-bound premise is not proof bureaucracy. On the one-point probability system, set

This process is integrable and subadditive because

and its normalized ledger begins

For any proposed real lower bound \(L\) and any proposed tail threshold \(N\), choose a natural

Then \(-n\lt L\). Thus every tail contains a value below \(L\), so no tail is bounded below.

In the extended real numbers the traditional limsup is \(-\infty\). Mathlib’s Filter.limsup in the conditionally complete order \(\mathbb R\) is deliberately total. Here every real number is eventually an upper bound for \(-n\), so its definition becomes

under the pinned real instance. But the block-one integral target is

Deleting the lower-bound gate would therefore demand the false real inequality \(0\le-1\). The generalized theorem rejects the model exactly where it should: its hXlower argument cannot be constructed. The nonnegative wrapper rejects it earlier.

The cocycle specialization needs no extra signed lower-bound proof because \(\log^+\) is pointwise nonnegative by definition; it enters through the nonnegative wrapper.

Why probability appears

The Birkhoff endpoint used in the block proof identifies a time average with the ordinary integral. That exact statement is appropriate on a probability space. For a finite measure of positive mass \(q\), with \(q\ne1\), the time average converges to the normalized space average

not the raw integral. Consequently the clean block target \((\int X_b)/b\) is a probability-normalized theorem.

This is separate from measure preservation. Preservation proves that every shifted copy of an integrable function has the same integral. Probability turns the invariant constant into the raw integral rather than an integral divided by total mass.

Optimize over every block

For the cocycle process

the generic theorem gives, for every positive \(b\),

outside a block-dependent null set. Natural numbers are countable, so the intersection of these full-measure events is still full measure. At every point in that intersection, \(L(\omega)\) is below every positive-block normalized integral.

The earlier deterministic Fekete theorem identifies their infimum with

The order step is le_csInf: exhibit one member of the set, then prove that the limsup lies below each member. The witness \(b=1\) proves nonemptiness. The resulting theorem compares a samplewise limsup with a deterministic integrated rate, but it does not exchange a limit and an integral.

In Lean: seven bridges from the finite ledger to the upper limsup

The two-state calculation used integer and rational tables. The project source works with arbitrary real integrable shifted-subadditive processes. Read each bridge across: spoken mathematics, paper notation, exact Lean, and then the syntax tokens that carry the hypothesis.

Bridge 1: split the normalized process exactly

normalized_eq_centered_add_birkhoffAverage n ω

Bridge 2: integrate a finite orbit sum

integral_birkhoffSum_eq_nat_mul hT hf n

Bridge 3: integrate the center

hX.integral_centeredProcess hT b

Bridge 4: keep every residue lane under one ordinary-map sum

hX.centeredProcess_le_birkhoffSum_phase_average_div b q r hb ω

Bridge 5: state the generalized fixed-block theorem

hX.ae_limsup_normalized_le_blockIntegral_of_ae_isBoundedUnder_ge hT hXlower b hb

Bridge 6: discharge the gate with nonnegativity

hX.ae_limsup_normalized_le_blockIntegral hT hXnonneg b hb

Bridge 7: optimize the cocycle bounds over every block

hC.ae_limsup_normalized_le_integratedLogPlusGrowthRate hT

Try the exact declarations in the repository

import NonlinearDynamics.Random.RandomCocycles.SubadditiveUpperLimsup

open MeasureTheory Set Filter Topology Finset Function
open NonlinearDynamics.Random.RandomCocycles

-- Imported finite bridges used by RMT-29.
#check normalized_eq_centered_add_birkhoffAverage
#check IsIntegrableSubadditiveProcessCandidate.centeredProcess_le_birkhoffSum_phase_average_div

-- The five RMT-29 public declarations, in source order.
#check integral_birkhoffSum_eq_nat_mul
#check IsIntegrableSubadditiveProcessCandidate.integral_centeredProcess
#check IsIntegrableSubadditiveProcessCandidate.ae_limsup_normalized_le_blockIntegral_of_ae_isBoundedUnder_ge
#check IsIntegrableSubadditiveProcessCandidate.ae_limsup_normalized_le_blockIntegral
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.ae_limsup_normalized_le_integratedLogPlusGrowthRate

cd formalization
lake env lean NonlinearDynamics/SubadditiveUpperLimsupChecks.lean

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

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

Type the finite process and lower-bound ledgers with Lean and Std

The next worksheet uses exact integers and rationals. It computes both paths of the two-state process through horizon eight, its centered values, block ratios, and phase coefficients. It also computes the negative-square ledger and concrete witnesses defeating several proposed lower bounds.

The finite Boolean checks test subadditivity and nonnegativity through horizon twelve; they illustrate the formula but are not the general Mathlib proof. The worksheet does not define a measure, a filter, or an infinite limsup. Save this exact text as /tmp/SubadditiveUpperLimsupTutorial.lean:

import Std

namespace SubadditiveUpperLimsupTutorial

inductive Point where
  | a
  | b
  deriving Repr, DecidableEq

def step : Point → Point
  | .a => .b
  | .b => .a

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

def phi : Point → Int
  | .a => 0
  | .b => 1

def ceilHalf (n : Nat) : Nat := (n + 1) / 2

def process (n : Nat) (p : Point) : Int :=
  (ceilHalf n : Int) + phi (iterate n p) - phi p

def oneStep : Point → Int := process 1

def orbitSum (n : Nat) (f : Point → Int) (p : Point) : Int :=
  ((List.range n).map fun j => f (iterate j p)).sum

def centered (n : Nat) (p : Point) : Int :=
  process n p - orbitSum n oneStep p

def normalize (z : Int) (n : Nat) : Rat :=
  if n = 0 then 0 else (z : Rat) / (n : Rat)

def integralTwo (f : Point → Int) : Rat :=
  ((f .a : Rat) + (f .b : Rat)) / 2

def processIntegral (n : Nat) : Rat := integralTwo (process n)

def centeredIntegral (n : Nat) : Rat := integralTwo (centered n)

def blockTarget (b : Nat) : Rat :=
  if b = 0 then 0 else processIntegral b / (b : Rat)

def processLedger (n : Nat) :=
  (n, process n .a, process n .b,
    normalize (process n .a) n, normalize (process n .b) n,
    processIntegral n, blockTarget n)

def blockPrefix (b a : Nat) : Nat := b * (a - 1)

def blockCoefficient (b r a : Nat) : Rat :=
  (blockPrefix b a : Rat) / ((b : Rat) * (b * a + r : Rat))

def subadditiveThrough (bound : Nat) : Bool :=
  (List.range (bound + 1)).all fun m =>
    (List.range (bound + 1)).all fun n =>
      [.a, .b].all fun p =>
        process (m + n) p ≤ process m p + process n (iterate m p)

def nonnegativeThrough (bound : Nat) : Bool :=
  (List.range (bound + 1)).all fun n =>
    [.a, .b].all fun p => 0 ≤ process n p

def negativeProcess (n : Nat) : Int := -((n * n : Nat) : Int)

def normalizedNegative (n : Nat) : Rat := normalize (negativeProcess n) n

def lowerWitness (lower : Int) : Nat := lower.natAbs + 1

def lowerWitnessRow (lower : Int) :=
  let n := lowerWitness lower
  (lower, n, normalizedNegative n,
    decide (normalizedNegative n < (lower : Rat)))

#eval (List.range 9).map processLedger
#eval (List.range 9).map fun n => (n, centered n .a, centered n .b)
#eval (centeredIntegral 2, processIntegral 1,
  centeredIntegral 2 / 2 + processIntegral 1, blockTarget 2)
#eval (List.range 6).map fun b => (b + 1, blockTarget (b + 1))
#eval [2, 3, 4, 5, 6].map fun a =>
  (a, blockCoefficient 2 0 a, blockCoefficient 2 1 a)
#eval (List.range 7).map fun n => (n, negativeProcess n, normalizedNegative n)
#eval [0, -1, -5, -20].map lowerWitnessRow
#eval (0 : Rat) ≤ (-1 : Rat)

example : subadditiveThrough 12 = true := by native_decide
example : nonnegativeThrough 12 = true := by native_decide
example :
    (List.range 9).map (fun n => centered n .a) =
      [0, 0, -1, -1, -2, -2, -3, -3, -4] := by
  native_decide
example : blockTarget 1 = 1 := by native_decide
example : blockTarget 2 = 1 / 2 := by native_decide
example :
    [0, -1, -5, -20].all (fun lower =>
      let n := lowerWitness lower
      normalizedNegative n < (lower : Rat)) = true := by
  native_decide

end SubadditiveUpperLimsupTutorial

From any directory, type:

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

The byte-for-byte standard output emitted by Lean is:

[(0, 0, 0, 0, 0, 0, 0),
 (1, 2, 0, 2, 0, 1, 1),
 (2, 1, 1, (1 : Rat)/2, (1 : Rat)/2, 1, (1 : Rat)/2),
 (3, 3, 1, 1, (1 : Rat)/3, 2, (2 : Rat)/3),
 (4, 2, 2, (1 : Rat)/2, (1 : Rat)/2, 2, (1 : Rat)/2),
 (5, 4, 2, (4 : Rat)/5, (2 : Rat)/5, 3, (3 : Rat)/5),
 (6, 3, 3, (1 : Rat)/2, (1 : Rat)/2, 3, (1 : Rat)/2),
 (7, 5, 3, (5 : Rat)/7, (3 : Rat)/7, 4, (4 : Rat)/7),
 (8, 4, 4, (1 : Rat)/2, (1 : Rat)/2, 4, (1 : Rat)/2)]
[(0, 0, 0), (1, 0, 0), (2, -1, -1), (3, -1, -1), (4, -2, -2), (5, -2, -2), (6, -3, -3), (7, -3, -3), (8, -4, -4)]
(-1, 1, (1 : Rat)/2, (1 : Rat)/2)
[(1, 1), (2, (1 : Rat)/2), (3, (2 : Rat)/3), (4, (1 : Rat)/2), (5, (3 : Rat)/5), (6, (1 : Rat)/2)]
[(2, (1 : Rat)/4, (1 : Rat)/5),
 (3, (1 : Rat)/3, (2 : Rat)/7),
 (4, (3 : Rat)/8, (1 : Rat)/3),
 (5, (2 : Rat)/5, (4 : Rat)/11),
 (6, (5 : Rat)/12, (5 : Rat)/13)]
[(0, 0, 0), (1, -1, -1), (2, -4, -2), (3, -9, -3), (4, -16, -4), (5, -25, -5), (6, -36, -6)]
[(0, 1, -1, true), (-1, 2, -2, true), (-5, 6, -6, true), (-20, 21, -21, true)]
false

The first ledger columns are \((n,X_n(a),X_n(b),X_n(a)/n,X_n(b)/n,\int X_n,\int X_n/n)\). The second is the centered ledger. The four-tuple \((-1,1,1/2,1/2)\) is the block-two cancellation. The next outputs list the block ratios and the two residue coefficients. Each true in the negative-square witness list says that the displayed horizon falls below the proposed lower bound. The final false is the invalid conclusion \(0\le-1\).

Standalone tutorial, suitable for a normal macOS or Linux machine. It imports only Std and never opens the project’s Mathlib dependency graph. This exact file and output were checked with the pinned Lean 4.32.0 toolchain. The exact project module uses the full project commands above.

Complete source-order declaration, private-helper, and probe map

The checked source is 428 lines and has SHA-256 c39c8b3547ab0cfe949a8859d76ad226c1bef71d3648fc61c76487bb825bf1b9. It contains five public declarations, fourteen private support items, three anonymous compiled probes, and five axiom queries. The full sequence is:

The proof of item 7 first combines the supplied lower bound with the one-step-Birkhoff upper bound so limsup_le_iff is legal in \(\mathbb R\). It then enters every arithmetic lane, composes the two Birkhoff limits with private items 3 and 4, multiplies by the coefficient from private item 5, applies finite phase averaging, and recombines the lanes. Item 8 does only one new thing: it constructs lower bound zero and invokes item 7.

Boundary models

Negative-square process and the real-limsup gate

Status: explanatory countermodel for the generalized signature, not one of the three anonymous compiled probes.

The earlier \(Z_n=-n^2\) ledger is subadditive and integrable but has no eventual real lower bound after normalization. It therefore explains why item 7 exposes hXlower. The module’s compiled probes test totalized zero and powered-map behavior; they do not compile this negative process.

Positive additive one-point model

Status: explanatory sharpness model, not one of the three compiled anonymous examples in the RMT-29 module.

On a one-point probability space let \(X_n=cn\) with \(c\ge0\). The process is additive, every normalized value is \(c\), and

The theorem is sharp at every block size.

Zero process and time zero

Status: represented by compiled boundary support and an anonymous example.

If \(X_n=0\), every conclusion is equality. The normalized expression at time zero is also totalized by Lean’s real division, but the asymptotic proof works eventually at positive times. No growth interpretation is assigned to division by a zero horizon.

The flip blocks powered-map reasoning

Status: represented by the compiled Bool boundary and block-two example.

Let \(T\) swap two equally weighted points. Then \(T\) is ergodic while \(T^2\) is the identity and is not ergodic. A proof that assumes Birkhoff convergence for \(T^2\) from ergodicity of \(T\) is invalid. The RMT-29 proof uses phase averaging and Birkhoff only for \(T\).

Empty matrix index

Status: explanatory signature audit, not one of the three compiled anonymous examples in the RMT-29 module.

The cocycle theorem does not need a positive matrix dimension. With an empty finite index type, matrix definitions and nonnegativity remain total. This boundary demonstrates that no hidden inhabitant is required.

What is proved, and what is not

The checked layer proves:

• exact finite Birkhoff-sum integration under measure preservation;
• exact centered-block integration;
• a generic almost-everywhere upper limsup bound for integrable subadditive candidates whose normalized paths are eventually bounded below almost everywhere on an ergodic probability system;
• a pointwise-nonnegative compatibility wrapper for that theorem; and
• the corresponding integrated-rate bound for log-positive matrix cocycles.

It does not prove:

• a matching lower liminf bound;
• convergence of \(X_n/n\);
• the full subadditive ergodic theorem;
• equality with the integrated rate;
• convergence in \(L^1\);
• an interchange of limit and integral;
• a signed logarithmic growth theorem;
• existence of Lyapunov exponents in the usual signed sense;
• an Oseledets splitting;
• mixing, independence, or powered-map ergodicity; or
• any quantitative rate of convergence.

Thirty-two solved exercises

Exercise 1: check the one-step majorant

Why is \(X_n\le S_n(X_1)\) a natural induction?

Solution. Split the successor horizon as \(n\) followed by \(1\). Subadditivity gives \(X_{n+1}\le X_n+X_1\circ T^n\); the induction hypothesis appends this last shifted one-step term to \(S_n(X_1)\). The positive-horizon induction starts at \(n=1\), where equality holds.

Exercise 2: determine the sign of the center

What sign does \(Y_n=X_n-S_n(X_1)\) have for positive \(n\)?

Solution. The one-step majorant gives \(Y_n\le0\).

Exercise 3: reconstruct the process

Solve the definition of \(Y_n\) for \(X_n/n\).

Solution. Divide \(X_n=Y_n+S_n(X_1)\) by \(n\gt0\) to obtain \(X_n/n=Y_n/n+A_n(X_1)\).

Exercise 4: integrate an orbit sum

Why is \(\int S_bf=b\int f\)?

Solution. Integrate the finite sum termwise. Each iterate preserves the measure, so every pullback term has integral \(\int f\). There are \(b\) terms.

Exercise 5: integrate the center

Compute \(\int Y_b\).

Solution. Linearity and Exercise 4 give \(\int Y_b=\int X_b-b\int X_1\).

Exercise 6: find the missing block

For \(n=ba+r\), why use \(m=b(a-1)\) rather than \(ba\)?

Solution. The finite phase theorem must retain boundary corrections. One complete block is sacrificed so every phase row fits the common horizon.

Exercise 7: calculate the coefficient

Evaluate \(b(a-1)/(b(ba+r))\) as \(a\to\infty\).

Solution. Divide numerator and denominator by \(a\). The limit is \(b/(b^2)=1/b\) because \(b\gt0\).

Exercise 8: explain the residue bound

Why require \(0\le r\lt b\)?

Solution. Those are exactly the finitely many residues modulo \(b\), so their arithmetic progressions cover every natural time.

Exercise 9: prove the arithmetic map diverges

Why does \(a\mapsto ba+r\) tend to infinity?

Solution. Since \(b\ge1\), one has \(a\le ba\le ba+r\).

Exercise 10: prove the prefix diverges

Why does \(a\mapsto b(a-1)\) tend to infinity?

Solution. Beyond any finite prefix, \(a-1\) tends to infinity, and multiplication by the positive integer \(b\) preserves divergence.

Exercise 11: identify the Birkhoff map

Which transformation appears in the limiting averages?

Solution. The original map \(T\), both for \(Y_b\) and for \(X_1\).

Exercise 12: reject the powered-map shortcut

Why is Ergodic T insufficient for a direct \(T^b\) Birkhoff call?

Solution. Ergodicity need not pass to powers. The two-point flip with \(b=2\) is a counterexample.

Exercise 13: combine the limiting constants

Simplify \((\int Y_b)/b+\int X_1\).

Solution. Substitute the centered integral formula. The one-step terms cancel, leaving \((\int X_b)/b\).

Exercise 14: locate probability

Where does mass one matter?

Solution. It identifies the ergodic Birkhoff constant with the raw integral rather than the integral divided by total mass.

Exercise 15: locate measure preservation

Where is preservation used before the limit theorem?

Solution. It makes every shifted pullback of an integrable observable have the same integral, yielding the finite Birkhoff-sum integral identity.

Exercise 16: locate the generalized lower-bound gate

Where does eventual lower-boundedness enter the generalized proof?

Solution. Together with the one-step-Birkhoff upper bound, it supplies the two order bounds needed to use limsup_le_iff in the conditionally complete real order. Pointwise nonnegativity is used only by the wrapper to choose the lower bound zero.

Exercise 17: test a negative process

Show that \(X_n=-n^2\) is subadditive.

Solution. Since \((m+n)^2\ge m^2+n^2\), negation reverses the inequality.

Exercise 18: normalize the negative process

What is \(X_n/n\) for positive \(n\)?

Solution. It is \(-n\), which is not bounded below in \(\mathbb R\).

Exercise 19: test the zero process

What does the block theorem say for \(X_n=0\)?

Solution. Both limsup and block integral ratio are zero, so the inequality is equality.

Exercise 20: test a sharp positive process

What does the theorem say for \(X_n=cn\) with \(c\ge0\) on one point?

Solution. Every normalized term and every normalized block integral is \(c\), so the estimate is sharp.

Exercise 21: separate limsup from limit

Does \(\limsup a_n\le L\) imply \(a_n\to L\)?

Solution. No. The sequence alternating between \(0\) and \(1\) has limsup \(1\) but does not converge.

Exercise 22: identify the missing half

What kind of inequality would complement the upper bound?

Solution. A lower estimate of the form \(\liminf X_n/n\ge\gamma\), together with the reverse comparison needed to identify both quantities.

Exercise 23: take the block infimum

If \(L\le a_b\) for every \(b\ge1\), what follows?

Solution. Nonemptiness plus the inequalities \(L\le a_b\) lets le_csInf conclude \(L\le\inf_{b\ge1}a_b\).

Exercise 24: witness nonemptiness

Which block is the simplest witness for the Fekete set?

Solution. Block \(b=1\).

Exercise 25: intersect the events

Why can the proof enforce every positive-block inequality simultaneously?

Solution. Positive natural numbers are countable, and a countable intersection of full-measure events has full measure.

Exercise 26: inspect time zero

Why is \(X_0/0\) not an analytic premise?

Solution. Lean’s real division is total, but the proof eventually works only at positive times and the Fekete infimum ranges over positive blocks.

Exercise 27: explain log-positive nonnegativity

Why does the cocycle endpoint inherit the generic lower bound?

Solution. By definition \(\log^+x=\max(\log x,0)\), so the observable is pointwise nonnegative at every horizon.

Exercise 28: reject a signed exponent claim

Why is the endpoint not a signed Lyapunov exponent theorem?

Solution. Positive clipping erases contraction. A negative logarithmic growth rate can produce the identically zero log-positive process.

Exercise 29: reject independence

Where are independent orbit samples assumed?

Solution. Nowhere. The proof uses deterministic subadditivity, measure preservation, ergodicity, integrability, and finite phase averaging.

Exercise 30: reject a limit-integral exchange

Does the cocycle endpoint prove \(\int\lim X_n/n=\lim\int X_n/n\)?

Solution. No. It compares a pointwise limsup to an independently defined deterministic infimum of finite-horizon integrals.

Exercise 31: audit the empty index

Why need no Nonempty ι hypothesis in the cocycle theorem?

Solution. The finite-dimensional matrix and norm interfaces used by the theorem are total for an empty finite index. The proof never chooses an index.

Exercise 32: state the exact summit

Give the strongest justified one-sentence conclusion.

Solution. For an ergodic probability-base discrete matrix cocycle with an integrable one-step log-positive envelope, the samplewise normalized log-positive norm has limsup at most the integrated log-positive Fekete rate almost everywhere.

Continue to the finite lower-bound bridge

Finite Bad-Block Measure Bounds Before Kingman’s Lower Liminf develops the next checked layer. It turns visits to strict centered short-block failures into a finite real-measure ratio through ordered interval packing. That chapter still stops before the ergodic lower-liminf conclusion.

The Guarded Real-Liminf Bridge to Log-Positive Kingman Convergence continues through the later rational null-event layer, exposes Mathlib’s exact real-boundedness gates, and completes the log-positive convergence assembly. This later result does not change the one-sided scope of RMT-29 itself.

Full project check

After installing the repository’s pinned dependencies, run this from the repository root:

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

This command may compile substantial parts of the pinned Mathlib graph and therefore may require substantial disk space and memory. The Standalone tutorial above remains the lighter route for following the arithmetic interactively.

References

J. F. C. Kingman. The ergodic theory of subadditive stochastic processes, Journal of the Royal Statistical Society: Series B 30(3), 499-510, 1968, doi:10.1111/j.2517-6161.1968.tb00749.x. This is the primary source for the full asymptotic theorem. RMT-29 formalizes only the upper-limsup component described above.

J. Michael Steele. Kingman’s subadditive ergodic theorem, Annales de l’Institut Henri Poincaré, Probabilités et Statistiques 25(1), 93-98, 1989. Steele gives a conceptually algorithmic full proof, beginning with a Birkhoff-based centering reduction and then using an interval-decomposition argument. It is proof-lineage context, not a Lean dependency.

Steven P. Lalley. Kingman’s Subadditive Ergodic Theorem, University of Chicago lecture notes, undated, accessed 2026-07-22. The notes explain why \(T^b\) need not be ergodic and motivate averaging all phases so ordinary \(T\)-Birkhoff convergence applies. They are a pedagogical source, not a primary theorem source; RMT-20 separately audits a finite boundary inconsistency in their displayed rows.

George D. Birkhoff. Proof of the Ergodic Theorem, Proceedings of the National Academy of Sciences 17(12), 656-660, 1931. This is the historical source for the individual ergodic theorem used only through the repository’s checked RMT-28 interface.

Mathlib contributors. Liminf and limsup, Mathlib commit 81a5d257. The pinned source supplies limsup_le_iff.

Mathlib contributors. Arithmetic progressions at atTop, Mathlib commit 81a5d257. The pinned source supplies Eventually.atTop_of_arithmetic.