From Finite Centered Bad-Block Bounds to All-Positive-Length Control

Begin with two atoms and one first witness

Let

carry the uniform probability measure, so each atom has mass \(1/2\). Let the base map be the identity. This system preserves the measure but is not ergodic: each singleton is invariant and has nonzero, nonfull mass.

Use the centered process

Natural-number subtraction is truncated, so \(Y_0(\text{amber})=0\), and \(Y_1=0\) at both atoms. Choose the slope

A positive length \(n\) is a strict bad-block witness at \(x\) when

For blue this never happens: \(0\) cannot lie below the negative number \(-3n/4\). For amber, the complete first ledger is:

The algebra isolates the same boundary:

If \(B_m(c)\) searches only lengths \(1,\ldots,m\), then

while

Removing the cap does not create an infinite witness. It merely permits the finite witness \(n=5\):

See the rate premise numerically

Uniform integration gives, for every positive \(n\),

After normalization,

Set

Then \(\delta\) is a lower bound for every positive normalized integral, and

The generic RMT-31 conclusion becomes

The theorem does not need ergodicity, and this identity model is explicitly nonergodic. It also does not need probability normalization; the uniform probability is used here only because it makes every number transparent.

Let equality fail first and strictness succeed later

Set the slope to zero while keeping the same process. At length one,

so the strict comparison fails. At length two,

so amber enters. Therefore

This nearby boundary prevents two common mistakes: replacing strict \(\lt\) by non-strict \(\le\), or deciding the uncapped event from length one alone.

Separate one bad length from recurrence and invariance

Now use a different two-atom model. Let the base map collapse both atoms to blue:

The Dirac measure at blue is preserved. Define a one-shot centered process by

for every \(n\), and

Choose \(c=-2/5\). Amber is strict at exactly one positive length:

For \(n\ge3\), the line keeps moving downward while the one-shot value stays at \(-1\), so there are no arbitrarily late witnesses. Nevertheless,

because the raw event asks for one witness. The collapse map never lands at amber, hence

The two models serve different purposes. The identity model checks nested caps, the first strict witness, the uniform rate premise, and the \(1/2\le2/3\) ratio. The collapse model checks that a one-witness union can be setwise noninvariant even for a preserved finite measure and a valid shifted-subadditive process.

RMT-30 fixes a natural-number cap \(m\) and controls the points at which some centered block of length at most \(m\) falls strictly below a line. RMT-31 removes the cap. Three operations must remain separate:

1. identify the all-length event exactly as a nested union;
2. take the limit in the native extended measure type; and
3. project to real measure only after ruling out an infinite target.

The last operation is where finite mass enters. It is not needed for the set identity, null measurability, or extended-measure continuity. Once the real limit is justified, the same upper bound that RMT-30 proves for every cap passes to the union by closedness of an upper interval.

This is one measure-theoretic bridge inside Kingman’s much stronger subadditive ergodic theorem (Kingman 1968). The finite interval-decomposition perspective is also visible in Steele’s exposition (Steele 1989); neither source is claimed to contain this repository’s Lean interface.

This chapter is the textbook companion to the RMT-31 Development Notebook. Its input comes from Finite Bad-Block Measure Bounds Before Kingman Lower Liminf. Useful compact references are orbit-majorant centering , finite orbit-visit count , and integrated log-positive growth rate .

Choose a route up

Common setup and notation

Let \(\Omega\) be a type, \(\mu\) a measure, and \(T:\Omega\to\Omega\) a map. An integrable shifted-subadditive candidate is a family \(X_n:\Omega\to\mathbb R\) satisfying

The repository centers it by subtracting the one-step orbit sum:

This is pointwise orbit-majorant centering , not expectation centering. It gives \(Y_1=0\), preserves shifted subadditivity, and makes \(Y_n\le0\) for positive \(n\). A block is bad at \(\omega\) when \(Y_n(\omega)\lt cn\). Equality is not a witness.

Start with finite caps

For \(m\in\mathbb N\), RMT-30 defines

The cap-zero set is empty. At a positive cap, membership means at least one allowed length works, not that every length works. RMT-31 defines

The infinity symbol describes the search range. Every actual witness is finite. The checked membership theorem is

This is a once-bad event. It does not mean failures occur infinitely often, eventually, or along an unbounded sequence.

The compiled two-point process calibrates strictness. It has \(Y_1=0\) at both points, while one point has \(Y_2=-1\). At slope \(c=0\), equality at time one contributes nothing but time two is a strict witness. The all-length event can therefore be nonempty when the cap-one event is empty.

Nest the caps

If \(m\le M\), every witness with \(1\le n\le m\) also satisfies \(1\le n\le M\). Thus \(B_m(c)\subseteq B_M(c)\). This is monotonicity of the search window, not a claim that \(Y_m(\omega)\le Y_M(\omega)\).

The all-length definition is already the union, so centeredAllLengthBadBlockSet_eq_iUnion_finite is proved by rfl. The theorem finiteCenteredBadBlockSet_subset_allLength packages inclusion of any cap. Conversely, given an uncapped witness \(n\), choose cap \(m=n\). No compactness, limiting witness, supremum, or infinite maximizing time is involved.

Take the countable null-measurable union

Assume \(X\) is an integrable shifted-subadditive candidate and \(T\) preserves \(\mu\). RMT-30 proves every \(B_m(c)\) null measurable. RMT-31 uses Mathlib’s closure under countable null-measurable unions to prove

Integrability supplies almost-everywhere measurability; it need not make the chosen representatives ordinarily measurable. The theorem does not claim an ordinary MeasurableSet certificate. Finite total mass, probability, and ergodicity are absent. Preservation transports integrability through the dynamics; it does not make this raw union invariant.

Use extended measure first

Lean measures take values in \(\mathbb R_{\ge0\infty}\). Since the caps increase and their union is exact, continuity from below gives

tendsto_measure_finiteCenteredBadBlockSet needs no measurability of the events, integrability, subadditivity, preservation, finite mass, probability, or ergodicity. Mathlib’s tendsto_measure_iUnion_atTop consumes only the increasing-set geometry and permits an infinite target.

Cross the real-projection cliff

Mathlib’s real-valued measure view is

At infinity, \(\operatorname{toReal}(\infty)=0\), so this projection is not continuous there. RMT-31 therefore assumes the local gate

before composing ENNReal.tendsto_toReal with extended continuity. The result is

The gate concerns one event, not all of \(\Omega\). A finite measure space is a convenient stronger interface because every subset has measure at most the finite total mass; Lean discharges the target by finiteness.

Transport the uniform RMT-30 ratio

Assume \(\mu\) is finite, \(T\) preserves \(\mu\), and \(X\) is an integrable shifted-subadditive candidate. Suppose

and choose \(c\lt\delta\). RMT-30 proves for every cap \(m\) that

The right side is independent of \(m\). Finite mass gives real convergence of the cap measures. Lean’s le_of_tendsto’ then says that the limit of values below one fixed ceiling remains below that ceiling:

The limit passage loses no factor and introduces no error term. It does not repeat interval packing. RMT-30 has done the finite combinatorics; RMT-31 transports the cap-uniform conclusion. Since \(Y_1=0\), the rate premise forces \(\delta\le0\), and \(c\lt\delta\) forces \(c\lt0\).

Finite mass need not mean probability

The theorem uses IsFiniteMeasure μ, not probability. The source checks a measure of total mass two. Under rescaling, event mass and raw integrals scale, so a compatible \(\delta\) scales too. A two-atom identity example is nonergodic, has bad set exactly one atom of mass \(1/2\), and satisfies the displayed estimate \(1/2\le2/3\).

Specialize to log-positive cocycles

For a discrete matrix cocycle \(C\), take \(X_n(\omega)=\log^+\lVert C(n,\omega)\rVert_\infty\). The named event is DiscreteMatrixCocycle.centeredLogPlusAllLengthBadBlockSet. The hypothesis C.HasIntegrableGeneratorLogPlus packages the generic candidate and one-step integrability. Define

where \(\gamma^+_\mu(C)\) is the integrated log-positive growth rate . The deterministic Fekete interface supplies the uniform rate premise. For every \(c\lt\delta_C\),

The theorem assumes no ergodicity and no positive-dimension premise; it compiles with an empty finite matrix index. It concerns log-positive norm, not signed logarithmic growth or a Lyapunov exponent.

The raw event need not be invariant

An all-length union is not automatically invariant. It records one bad block starting now, and moving the origin can erase that witness.

The source compiles a countermodel on Bool:

• the base map sends both points to true;
• the Dirac mass at true is preserved;
• the one-shot process is zero at true;
• at false, it is zero before length two and \(-1\) thereafter;
• at slope \(-2/5\), the bad event is exactly {false}.

The preimage of that singleton is empty, so

The source checks the integrable shifted-subadditive candidate and preservation before proving non-invariance.

Null measurability does not imply invariance. Measure preservation does not make every dynamically defined set invariant. A subunit bound cannot become a zero-one conclusion until the right event is invariant or almost invariant and the matching ergodic hypothesis is present.

RMT-32 now supplies the event layer

RMT-32 does not merely add ergodicity to \(B_\infty(c)\). It replaces one positive witness by an asymptotic statement: an intersection over starting cutoffs of unions over later positive lengths. To represent strict lower deviation with a durable strict gap, it chooses one rational margin \(q\lt c\).

The checked change is from

to a statement like

The strict rational slack matters. A sequence can lie below \(c\) infinitely often while approaching \(c\), so those witnesses alone do not prove that its lower liminf is strictly below \(c\).

The new Rational-Slack Lower-Deviation Events and Ergodic Null Selection chapter follows the completed proof. RMT-32 establishes countable null measurability, a threshold-relaxed fixed-slope preimage inclusion, rational density at the target, and almost-invariance under preservation plus finite mass. Finite-measure ergodicity yields an almost-empty or almost-full dichotomy. Probability is not needed for that fork; probability normalization and RMT-31’s strict subunit ratio select the null branch.

The exact equivalence with a library-level real lower limit remains RMT-33’s job. RMT-31 supplies the quantitative once-bad ceiling used in branch selection, while RMT-32 supplies the distinct asymptotic event and rigidity layer.

Seven bridges from the two-atom ledgers to Lean

The finite tables used lists of atoms and exact rational comparisons. The project module states the same architecture for arbitrary sets, measures, and centered subadditive processes. Each bridge aligns ordinary language, paper mathematics, exact Lean syntax, and the tokens that carry the proof.

Bridge 1: remove the cap without inventing an infinite witness

mem_centeredAllLengthBadBlockSet_iff

Bridge 2: enlarge only the search window

finiteCenteredBadBlockSet_mono hmM c

Bridge 3: take the countable null-measurable union

hX.nullMeasurableSet_centeredAllLengthBadBlockSet hT c

Bridge 4: take continuity in extended measure first

tendsto_measure_finiteCenteredBadBlockSet (T := T) (μ := μ) X c

Bridge 5: cross to Measure.real only at a finite target

tendsto_measureReal_finiteCenteredBadBlockSet (T := T) (μ := μ) X c hfinite

Bridge 6: preserve the finite-cap ratio at the union

hX.measureReal_centeredAllLengthBadBlockSet_le_rateRatio hT δ c hδ hc

Bridge 7: specialize the generic bridge to a matrix cocycle

hC.measureReal_centeredLogPlusAllLengthBadBlockSet_le_rateRatio c hc

Type-check the exact project interface

import NonlinearDynamics.Random.RandomCocycles.SubadditiveAllLengthBadBlockMeasure

open NonlinearDynamics.Random.RandomCocycles

#check centeredAllLengthBadBlockSet
#check mem_centeredAllLengthBadBlockSet_iff
#check finiteCenteredBadBlockSet_mono
#check centeredAllLengthBadBlockSet_eq_iUnion_finite
#check finiteCenteredBadBlockSet_subset_allLength
#check IsIntegrableSubadditiveProcessCandidate.nullMeasurableSet_centeredAllLengthBadBlockSet
#check tendsto_measure_finiteCenteredBadBlockSet
#check tendsto_measureReal_finiteCenteredBadBlockSet
#check IsIntegrableSubadditiveProcessCandidate.measureReal_centeredAllLengthBadBlockSet_le_rateRatio
#check DiscreteMatrixCocycle.centeredLogPlusAllLengthBadBlockSet
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.measureReal_centeredLogPlusAllLengthBadBlockSet_le_rateRatio

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

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

Run both two-atom ledgers with Std

The following file imports only Lean’s Std library. It computes the nested caps, first witness, union mass, ratio, slope-zero strictness boundary, and collapse-map preimage with exact rational arithmetic. It neither imports Mathlib nor opens this project. Save the block byte for byte as /tmp/AllLengthBadBlockDeepDiveTutorial.lean:

import Std

namespace AllLengthBadBlockDeepDiveTutorial

inductive Atom where
  | amber
  | blue
  deriving Repr, DecidableEq

def atoms : List Atom := [.amber, .blue]

def atomName : Atom → String
  | .amber => "amber"
  | .blue => "blue"

def centered (n : Nat) : Atom → Rat
  | .amber => -((n - 1 : Nat) : Rat)
  | .blue => 0

def slope : Rat := -(3 : Rat) / 4

def strictBadAt (n : Nat) (x : Atom) : Bool :=
  decide (0 < n ∧ centered n x < slope * (n : Rat))

def capEvent (cap : Nat) : List Atom :=
  atoms.filter fun x =>
    (List.range (cap + 1)).any fun n => strictBadAt n x

def firstWitness (x : Atom) : Option Nat :=
  ((List.range 12).map (· + 1)).find? fun n => strictBadAt n x

def eventMass (event : List Atom) : Rat :=
  (event.length : Rat) / 2

structure CapRow where
  cap : Nat
  event : List String
  mass : Rat
  deriving Repr, DecidableEq

def capRow (cap : Nat) : CapRow :=
  let event := capEvent cap
  { cap := cap
    event := event.map atomName
    mass := eventMass event }

def strictAtSlope (c : Rat) (n : Nat) (x : Atom) : Bool :=
  decide (0 < n ∧ centered n x < c * (n : Rat))

def capEventAtSlope (c : Rat) (cap : Nat) : List Atom :=
  atoms.filter fun x =>
    (List.range (cap + 1)).any fun n => strictAtSlope c n x

def collapse : Atom → Atom
  | .amber => .blue
  | .blue => .blue

def oneShotCentered (n : Nat) : Atom → Rat
  | .amber => if 2 ≤ n then -1 else 0
  | .blue => 0

def oneShotBadAt (n : Nat) (x : Atom) : Bool :=
  decide (0 < n ∧
    oneShotCentered n x < (-(2 : Rat) / 5) * (n : Rat))

def oneShotEvent (cap : Nat) : List Atom :=
  atoms.filter fun x =>
    (List.range (cap + 1)).any fun n => oneShotBadAt n x

def oneShotPreimage (cap : Nat) : List Atom :=
  atoms.filter fun x => (oneShotEvent cap).contains (collapse x)

#eval (List.range 9).map capRow
#eval atoms.map fun x => (atomName x, firstWitness x)
#eval (capEvent 12).map atomName
#eval (eventMass (capEvent 12), (-(1 : Rat) / 2) / slope)
#eval ((capEventAtSlope 0 1).map atomName,
  (capEventAtSlope 0 2).map atomName)
#eval ((oneShotEvent 12).map atomName,
  (oneShotPreimage 12).map atomName)

example : ((List.range 8).map fun n => strictBadAt n .amber) =
    [false, false, false, false, false, true, true, true] := by
  native_decide

example : capEvent 4 = [] := by native_decide
example : capEvent 5 = [.amber] := by native_decide
example : eventMass (capEvent 12) = (1 : Rat) / 2 := by
  native_decide
example : eventMass (capEvent 12) ≤ (-(1 : Rat) / 2) / slope := by
  native_decide
example : capEventAtSlope 0 1 = [] := by native_decide
example : capEventAtSlope 0 2 = [.amber] := by native_decide
example : oneShotEvent 12 = [.amber] := by native_decide
example : oneShotPreimage 12 = [] := by native_decide

end AllLengthBadBlockDeepDiveTutorial

Important syntax:

• inductive Atom creates exactly the two named atoms;
• Rat keeps the slopes, masses, and ratio exact;
• List.range (cap + 1) searches lengths zero through the cap, while strictBadAt separately requires positive length;
• List.any implements existence of one witness;
• List.filter materializes the finite event;
• find? returns some 5 for amber and none for blue; and
• each native_decide example supplies a kernel-checked proof of a displayed boundary or inequality.

With the pinned compiler installed, a human types:

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

This is a standalone tutorial suitable for a normal macOS or Linux host. It imports only Std, enumerates two atoms, and does not compile Mathlib or this project. Successful execution prints exactly:

[{ cap := 0, event := [], mass := 0 },
 { cap := 1, event := [], mass := 0 },
 { cap := 2, event := [], mass := 0 },
 { cap := 3, event := [], mass := 0 },
 { cap := 4, event := [], mass := 0 },
 { cap := 5, event := ["amber"], mass := (1 : Rat)/2 },
 { cap := 6, event := ["amber"], mass := (1 : Rat)/2 },
 { cap := 7, event := ["amber"], mass := (1 : Rat)/2 },
 { cap := 8, event := ["amber"], mass := (1 : Rat)/2 }]
[("amber", some 5), ("blue", none)]
["amber"]
((1 : Rat)/2, (2 : Rat)/3)
([], ["amber"])
(["amber"], [])

The first output is the increasing cap sequence. The next three outputs identify the first witness, union, mass, and ratio. The final two certify the slope-zero strictness boundary and the collapse model’s unequal raw event and preimage. These finite computations do not model extended nonnegative real measure, Measure.real, null measurability, or filter convergence; those are the responsibilities of the project module.

The eleven-declaration interface

The frozen 481-line source exposes exactly eleven public declarations in source order. Its SHA-256 is 53438522344c078d64473316a594570993d694ada909a33184579cec6a996fb7.

Fifteen private support items

These source-local declarations build boundary models without enlarging the public API:

Ten anonymous compiled examples

The examples are checked propositions but do not create public names:

Seven axiom reports

The source prints the axiom footprints of:

1. mem_centeredAllLengthBadBlockSet_iff;
2. finiteCenteredBadBlockSet_mono;
3. IsIntegrableSubadditiveProcessCandidate.nullMeasurableSet_centeredAllLengthBadBlockSet;
4. tendsto_measure_finiteCenteredBadBlockSet;
5. tendsto_measureReal_finiteCenteredBadBlockSet;
6. IsIntegrableSubadditiveProcessCandidate.measureReal_centeredAllLengthBadBlockSet_le_rateRatio; and
7. DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.measureReal_centeredLogPlusAllLengthBadBlockSet_le_rateRatio.

Assumption and nonclaim ledger

The module proves no lower-liminf inequality, almost-everywhere convergence, \(L^1\) convergence, signed logarithmic growth, Lyapunov exponent, or Oseledets splitting.

Thirty solved exercises

Exercise 1: unpack membership

What does \(\omega\in B_\infty(c)\) mean?

Solution. One finite \(n\) satisfies \(0\lt n\) and \(Y_n(\omega)\lt cn\). There is no predetermined cap.

Exercise 2: reject recurrence

Does membership imply infinitely many bad lengths?

Solution. No. A single existential witness suffices.

Exercise 3: compute cap zero

What is \(B_0(c)\)?

Solution. It is empty because no positive length is at most zero.

Exercise 4: recover a cap

Given an uncapped witness \(n\), which cap works?

Solution. Choose \(m=n\); then \(n\le m\) by reflexivity.

Exercise 5: prove finite inclusion

Why is \(B_m(c)\subseteq B_\infty(c)\)?

Solution. It is one term of the defining union.

Exercise 6: prove monotonicity

Why does \(m\le M\) imply \(B_m(c)\subseteq B_M(c)\)?

Solution. Reuse the witness and compose \(n\le m\) with \(m\le M\).

Exercise 7: reject process monotonicity

Does Exercise 6 prove \(Y_m(\omega)\le Y_M(\omega)\)?

Solution. No. Search windows grow; terminal process values need not.

Exercise 8: test equality

If \(Y_n(\omega)=cn\), is \(n\) a bad witness?

Solution. No. The definition requires strict inequality.

Exercise 9: use a later witness

Can equality at time one coexist with all-length membership?

Solution. Yes. A later length can be strictly bad; the compiled example uses time two at slope zero.

Exercise 10: classify the union

Is equality with the cap union only almost everywhere?

Solution. No. It is exact set equality and is definitional.

Exercise 11: build null measurability

Why is the all-length event null measurable?

Solution. Every cap is null measurable and countable unions preserve that property.

Exercise 12: avoid stronger regularity

May this be restated as ordinary measurability?

Solution. Not generally. Null measurability permits a null-set difference from a measurable representative.

Exercise 13: remove finite mass

Where is finite mass used in Exercise 11?

Solution. Nowhere. Countable-union closure has no finiteness premise.

Exercise 14: state native continuity

Which limit is unconditional?

Solution. \(\mu(B_m(c))\to\mu(B_\infty(c))\) in extended measure, even at an infinite target.

Exercise 15: locate set measurability

Does that continuity theorem require measurable caps?

Solution. No. The Mathlib theorem used here accepts increasing sets without that premise.

Exercise 16: compute the cliff

What is \(\operatorname{toReal}(\infty)\)?

Solution. Zero. The projection loses the extended infinity information.

Exercise 17: state the local gate

What permits real-measure convergence?

Solution. The target event’s extended measure must differ from infinity.

Exercise 18: compare finiteness notions

Can the real theorem apply when \(\mu(\Omega)=\infty\)?

Solution. Yes, if this particular union event has finite measure.

Exercise 19: discharge the gate

Why does a finite measure instance suffice?

Solution. The event measure is bounded by the finite total mass.

Exercise 20: transfer a ceiling

If \(x_m\to x\) and \(x_m\le C\), why is \(x\le C\)?

Solution. The closed interval ending at \(C\) contains every term and therefore its limit. Lean uses le_of_tendsto’.

Exercise 21: locate the finite input

What does RMT-30 contribute?

Solution. It proves the same ratio ceiling for every finite cap.

Exercise 22: avoid new packing

Why is interval packing absent from RMT-31?

Solution. Packing already proved the uniform finite theorem; RMT-31 only transports it through a limit.

Exercise 23: force the rate sign

Why is \(\delta\le0\)?

Solution. Apply the rate premise at time one, where \(Y_1=0\).

Exercise 24: force the slope sign

Why is \(c\lt0\)?

Solution. Combine \(c\lt\delta\) with \(\delta\le0\).

Exercise 25: remove probability

Does the generic theorem require total mass one?

Solution. No. It requires finite mass and compiles for mass two.

Exercise 26: remove ergodicity

What does the two-atom identity model show?

Solution. A nonergodic system has a half-mass bad event satisfying \(1/2\le2/3\).

Exercise 27: identify the cocycle rate

What plays the role of \(\delta\)?

Solution. The integrated log-positive Fekete rate minus the one-step log-positive integral.

Exercise 28: permit an empty index

Why can the matrix index be empty?

Solution. The proof uses a bundled norm-process interface and never chooses a coordinate.

Exercise 29: diagnose non-invariance

Why is the singleton event not invariant?

Solution. The collapse map sends both points to true, so the preimage of {false} is empty.

Exercise 30: design RMT-32

What must replace one-witness membership?

Solution. Arbitrarily late witnesses with suitable rational slack, a lower-liminf interpretation, a proved one-sided preimage inclusion, and an almost-invariance upgrade using preservation plus finite mass.

Choose the appropriate runnable path

There are two deliberately separate runnable paths.

• The Std worksheet is a tiny two-atom arithmetic tutorial suitable for an ordinary macOS or Linux host.
• The exact project import, extended-measure API, Measure.real, filter limits, candidate interface, and source check use the full project command in Type-check the exact project interface.

The distinction is about resource use, not pedagogy. Readers should type, run, and modify the standalone tutorial. The Mathlib-backed proof remains fully visible; checking it may require substantial disk space and memory.

The paired Development Notebook gives the implementation ledger and review history.

Continue the learning path

Finite Bad-Block Measure Bounds Before Kingman Lower Liminf derives the uniform finite-cap ratio.

From Finite Maximal Bounds to an Infinite Weak Estimate develops the analogous increasing-union and real-projection bridge.

Infinite-horizon Birkhoff-average exceedance event is a comparison for another one-witness event. Birkhoff sum and almost everywhere review language used in the regularity and future asymptotic layers.

References

These primary sources and library references use Mathlib 4.32.0 at pinned commit 81a5d257c8e410db227a6665ed08f64fea08e997.

J. F. C. Kingman. The ergodic theory of subadditive stochastic processes, JRSS Series B 30(3), 499-510, 1968, doi:10.1111/j.2517-6161.1968.tb00749.x. This is the primary source for the full theorem RMT-31 does not claim.

J. Michael Steele. Kingman’s subadditive ergodic theorem, Annales de l’Institut Henri Poincare 25(1), 93-98, 1989. Its interval decomposition motivates the finite machinery; RMT-31 isolates the union step.

Mathlib contributors. Continuity from below, Mathlib 4.32.0. It supplies the unconditional extended-measure limit.

Mathlib contributors. Continuity of ENNReal.toReal away from infinity, Mathlib 4.32.0. RMT-31 uses it only at a finite target.

Mathlib contributors. Definition of Measure.real, Mathlib 4.32.0. The definition totalizes infinite mass to zero.

Mathlib contributors. Null-measurable sets, Mathlib 4.32.0. The proof uses countable-union closure here.

Mathlib contributors. Closed-order limit lemmas, Mathlib 4.32.0. The ratio proof uses le_of_tendsto’ to retain a common upper bound at the real-measure limit.