Finite Bad-Block Measure Bounds Before Kingman Lower Liminf

Begin with two atoms and five possible block lengths

We will first calculate everything on a probability space with only two outcomes:

An outcome is one possible state of this finite world. A measurable subset of outcomes is an event . Its probability is the total mass assigned by \(\mu\).

Let the dynamics be the identity map:

Every orbit therefore stays on its starting atom. This map is measure preserving because moving an event backward through \(T\) does not change the event or its mass. It is not ergodic: the singleton event \(\{\text{amber}\}\) is invariant and has mass \(1/2\).

Define a real process by

Natural-number subtraction is truncated at zero, so \(Y_0=0\). On amber the first values are

on blue they are all zero. This is the exact private two-point model compiled in SubadditiveBadBlockMeasure.lean. In the source it is first packaged as a subadditive candidate \(X\). Since \(X_1=0\) and \(T\) is the identity, the repository’s orbit-majorant centered process

is exactly \(Y_n(\omega)\) in this model.

Three properties follow directly from the displayed formulas:

1. every \(Y_n\) is integrable because the probability space has two atoms;

2. \(Y_n\le0\) for every positive \(n\); and

3. the shifted subadditive inequality holds:

   \[ Y_{a+b}(\omega) \le Y_b(T^a\omega)+Y_a(\omega). \]

On blue this is \(0\le0\). On amber, when \(a,b\gt0\), the left side is \(-(a+b-1)\) and the right side is \(-(a+b-2)\). Zero-length cases reduce to equality.

Mark blocks below one negative line

Fix the block-length cap and strict threshold

A block of length \(n\) is bad at \(\omega\) when

Here is the complete finite search:

Write

The rows give

The finite bad-block event is their union:

Its exact probability is

Two boundary tests before any theorem

If the cap is zero, there are no positive candidate lengths:

Threshold zero needs more care. At cap one,

because \(Y_1=0\) and the event uses a strict inequality. It is false that threshold zero always makes the bad event empty. With the same process and cap five,

because \(Y_2(\text{amber})=-1\lt0\). The cap, strictness, and sign must all be read together.

Count twelve visits, then pack three witnesses

Choose a counting horizon

The finite orbit-visit count is

The amber orbit remains in the bad event at all twelve starts, while the blue orbit never enters it:

At each marked amber start, length five is a witness because

Starting from the left, a greedy disjoint cover can retain

These three intervals cover every marked start \(0,\ldots,11\). Their total covered length is \(15\), and they fit in the safe buffered horizon

The selected interval costs add to

The full amber chain is therefore

The final comparison uses both \(15\ge12\) and \(c\le0\). Multiplication by a nonpositive coefficient reverses the usual length comparison. The blue orbit has no marks and gives \(Y_{17}(\text{blue})=0\le0\).

Thus both atoms satisfy the pointwise theorem’s conclusion:

Integrate atom by atom

On this two-atom probability space, integrating a function means averaging its two values. For the visit count,

This is the finite identity

made completely explicit.

For the buffered centered process,

The integrated right side is

The pointwise inequality therefore integrates to the true finite comparison

Nothing was averaged over time here. We integrated two finite atom values after proving a finite pointwise inequality.

Compute the lower-rate witness and the ratio

Let

For every positive \(n\),

Consequently,

Choose

This is a lower bound for every positive normalized centered integral. It is not a statement about samplewise convergence. It is one deterministic inequality for the scalar sequence \(I_n/n\).

At the displayed buffered horizon,

For an arbitrary positive \(H\), the same proof gives

Only the elementary scalar factor moves toward a limit:

Hence

Because

division by \(c\) reverses the inequality:

In the running example,

This is the requested finite measure ratio.

The sign-reversal near miss

If one divides \(\delta\le cq\) by the negative number \(c\) without reversing the order, one obtains the wrong proposal

Our exact values refute it:

This error is not a minor notation issue. It changes a useful upper bound into a false lower bound.

Climb from the finite ledger to the general definitions

Now let \((\Omega,\mu)\) be any measurable space with finite total measure, let \(T:\Omega\to\Omega\) preserve \(\mu\), and let \(X_n:\Omega\to\mathbb R\) be an integrable shifted-subadditive process:

Define the orbit-majorant-centered process

[ Y_n(\omega) := X_n(\omega)

\sum_{j=0}^{n-1}X_1(T^j\omega). ]

The word centered here does not mean expectation centering. The subtracted quantity depends on \(\omega\). Shifted subadditivity gives

and \(Y\) is again shifted subadditive.

In Lean: define the finite strict bad-block event

finiteCenteredBadBlockSet T X m c

The exact source definition is:

def finiteCenteredBadBlockSet {Ω : Type uΩ} (T : Ω → Ω)
    (X : ℕ → Ω → ℝ) (m : ℕ) (c : ℝ) : Set Ω :=
  ⋃ n ∈ Finset.Icc 1 m,
    {ω | centeredProcess T X n ω < c * (n : ℝ)}

Candidate integrability and preservation are introduced only when the source proves that this finite union is null measurable. A null set has measure zero. A null measurable set may differ from an ordinary measurable set by a null set. That weaker regularity is exactly what the integration interface needs.

Turn visits into an indicator Birkhoff sum

For a set \(s\subseteq\Omega\), define

The corresponding Birkhoff sum is finite:

The symbol \(\mathbf 1_s\) is the indicator of \(s\): it is one on \(s\) and zero outside.

In Lean: cast the count to the exact finite sum

natCast_finiteOrbitVisitCount_eq_birkhoffSum_indicator T s H ω

At \(H=0\), both sides are zero. No separate positivity premise is required.

In Lean: integrate the finite visit count

integral_finiteOrbitVisitCount hT hs H

Probability normalization is absent. If the total mass were two, the two sides would both scale by two.

From one witness per visit to a pointwise cost bound

At every marked start \(j\lt H\), membership in \(B_m(c)\) supplies at least one witness length

The source uses classical choice to select one such \(\ell(j)\). It does not choose a shortest, longest, or globally optimal witness. RMT-21’s greedy interval theorem then extracts disjoint intervals that cover every marked start.

Positive-time nonpositivity lets the proof discard uncovered gaps from an upper bound. Shifted subadditivity concatenates the retained interval costs. Because \(c\le0\), covered length at least the number of marks implies the marked-cardinality estimate in the required direction.

In Lean: obtain the buffered pointwise inequality

hX.centeredProcess_le_badBlockVisitCount H m hHm c hc ω

The corner \(H=m=0\) cannot be erased. Then the right side is zero while

may be positive. If \(H=0\) but \(m\gt0\), the theorem reduces to \(Y_m\le0\), which is valid. If \(m=0\) but \(H\gt0\), the bad set is empty and the theorem reduces to \(Y_H\le0\).

Integrate first, then remove only the finite buffer

Assume a scalar \(\delta\) satisfies

Applying this at \(H+m\), integrating the pointwise packing bound, and using the exact count identity gives

At time one, \(Y_1=0\), so the premise forces \(\delta\le0\). The additional assumption \(c\lt\delta\) gives \(c\lt0\). The elementary coefficient tends to one as \(H\) grows. Therefore

Negative division finally yields the finite ratio.

In Lean: invoke the generic finite-measure ratio

hX.measureReal_finiteCenteredBadBlockSet_le_rateRatio hT m δ c hδ hc

The stronger strict comparison \(c\lt\delta\) also makes

That subunit ceiling is useful to a later probability-and-ergodicity argument. This module does not perform that later argument.

Specialize the lower-rate witness to matrix cocycles

For a discrete matrix cocycle \(C\), let

The one-step log-positive integrability package produces an integrable subadditive candidate. Define the deterministic offset

[ \delta_C := \gamma_\mu^+(C)

\int_\Omega X_1,d\mu, ]

where \(\gamma_\mu^+(C)\) is the integrated log-positive Fekete rate.

In Lean: prove the cocycle offset is a lower bound

hC.centeredFeketeOffset_le_normalizedIntegral n hn

In Lean: obtain the cocycle finite bad-set ratio

hC.measureReal_centeredLogPlusBadBlockSet_le_rateRatio m c hc

Assumption ledger: keep the layers separate

The opening example uses a probability measure to make atomwise averaging explicit. The generic theorem needs only a finite measure. Neither the generic theorem nor its cocycle specialization needs ergodicity.

Exact declaration map

The source exposes ten public declarations in dependency order:

The previous version of this chapter counted nine and omitted declaration 9. The table above matches the checked 506-line source.

All eleven private support declarations

All nine compiled anonymous boundary examples

1. A zero cap makes the candidate-length window empty.
2. Horizon zero is valid when the cap is positive.
3. The zero process has no bad blocks at a negative threshold.
4. The joint corner \(H=m=0\) fails for the positive-at-zero candidate.
5. Zero measure gives every bad set real measure zero.
6. The nonergodic two-point identity model has exact bad mass \(1/2\) and satisfies \(1/2\le2/3\).
7. Equality with the time-one zero threshold is not marked.
8. A mass-two finite measure is accepted without probability normalization.
9. The cocycle endpoint accepts an empty matrix-index type.

All seven axiom reports

The file prints axiom footprints for:

1. natCast_finiteOrbitVisitCount_eq_birkhoffSum_indicator;
2. integral_finiteOrbitVisitCount;
3. nullMeasurableSet_finiteCenteredBadBlockSet;
4. centeredProcess_le_badBlockVisitCount;
5. measureReal_finiteCenteredBadBlockSet_le_rateRatio;
6. centeredFeketeOffset_le_normalizedIntegral; and
7. measureReal_centeredLogPlusBadBlockSet_le_rateRatio.

The source’s recorded project validation found the expected Mathlib logical footprint.

A bounded executable model using only Std

The next worksheet reproduces the complete two-atom ledger without importing Mathlib or this project. It is a standalone tutorial suitable for a normal macOS or Linux machine. It is not a proof of the general measure theorem.

Save this exact block as /tmp/SubadditiveBadBlockMeasureTutorial.lean:

import Std

namespace SubadditiveBadBlockMeasureTutorial

inductive Atom where
  | amber
  | blue
  deriving Repr, DecidableEq

open Atom

def cap : Nat := 5
def countingHorizon : Nat := 12
def bufferedHorizon : Nat := countingHorizon + cap
def slope : Rat := -(3 : Rat) / 4
def lowerRate : Rat := -(1 : Rat) / 2

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

def candidateLengths (m : Nat) : List Nat :=
  (List.range m).map Nat.succ

def badAtLength (c : Rat) (n : Nat) (ω : Atom) : Bool :=
  decide (centered n ω < c * (n : Rat))

def badAtCap (m : Nat) (c : Rat) (ω : Atom) : Bool :=
  (candidateLengths m).any fun n => badAtLength c n ω

def shortRows : List (Nat × Rat × Rat × Bool × Bool) :=
  (candidateLengths cap).map fun n =>
    (n, centered n amber, slope * (n : Rat),
      badAtLength slope n amber, badAtLength slope n blue)

def badSet : List Atom :=
  [amber, blue].filter fun ω => badAtCap cap slope ω

def visitCount (H : Nat) (ω : Atom) : Nat :=
  ((List.range H).filter fun _ => badAtCap cap slope ω).length

def packedStarts : List Nat := [0, 5, 10]

def packedIntervals : List (Nat × Nat) :=
  packedStarts.map fun start => (start, start + cap)

def allMarkedStartsCovered : Bool :=
  (List.range countingHorizon).all fun j =>
    packedStarts.any fun start =>
      decide (start ≤ j ∧ j < start + cap)

def packedCost : Rat :=
  (packedStarts.map fun _ => centered cap amber).sum

def coveredLength : Nat :=
  packedStarts.length * cap

def integral (f : Atom → Rat) : Rat :=
  (f amber + f blue) / 2

def badMass : Rat :=
  ((badSet.length : Rat) / 2)

def visitIntegral : Rat :=
  integral fun ω => (visitCount countingHorizon ω : Rat)

def bufferedIntegral : Rat :=
  integral fun ω => centered bufferedHorizon ω

def packingChain : List Bool :=
  [decide (centered bufferedHorizon amber ≤ packedCost),
   decide (packedCost ≤ slope * (coveredLength : Rat)),
   decide (slope * (coveredLength : Rat) ≤
     slope * (visitCount countingHorizon amber : Rat))]

def ratio : Rat :=
  lowerRate / slope

def zeroThresholdBoundary : Bool × Bool × Bool :=
  (badAtCap 0 slope amber,
   badAtCap 1 0 amber,
   badAtCap cap 0 amber)

#eval shortRows
#eval badSet
#eval [visitCount countingHorizon amber, visitCount countingHorizon blue]
#eval packedIntervals
#eval (allMarkedStartsCovered, packedCost, coveredLength, packingChain)
#eval (visitIntegral,
  (countingHorizon : Rat) * badMass,
  bufferedIntegral,
  slope * visitIntegral)
#eval (badMass, ratio,
  decide (badMass ≤ ratio),
  decide (badMass ≥ ratio))
#eval zeroThresholdBoundary

example : shortRows =
    [(1, 0, -(3 : Rat) / 4, false, false),
     (2, -1, -(3 : Rat) / 2, false, false),
     (3, -2, -(9 : Rat) / 4, false, false),
     (4, -3, -3, false, false),
     (5, -4, -(15 : Rat) / 4, true, false)] := by
  native_decide

example : badSet = [amber] := by native_decide
example : packedIntervals = [(0, 5), (5, 10), (10, 15)] := by native_decide
example : allMarkedStartsCovered := by native_decide
example : packingChain = [true, true, true] := by native_decide
example : visitIntegral = 6 := by native_decide
example : bufferedIntegral = -8 := by native_decide
example : badMass = (1 : Rat) / 2 := by native_decide
example : ratio = (2 : Rat) / 3 := by native_decide
example : badMass ≤ ratio := by native_decide
example : ¬ badMass ≥ ratio := by native_decide
example : zeroThresholdBoundary = (false, false, true) := by native_decide

end SubadditiveBadBlockMeasureTutorial

Type:

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

The exact worksheet above was run successfully under Lean 4.32.0. Its exact transcript is:

[(1, 0, (-3 : Rat)/4, false, false),
 (2, -1, (-3 : Rat)/2, false, false),
 (3, -2, (-9 : Rat)/4, false, false),
 (4, -3, -3, false, false),
 (5, -4, (-15 : Rat)/4, true, false)]
[SubadditiveBadBlockMeasureTutorial.Atom.amber]
[12, 0]
[(0, 5), (5, 10), (10, 15)]
(true, -12, 15, [true, true, true])
(6, 6, -8, (-9 : Rat)/2)
((1 : Rat)/2, (2 : Rat)/3, true, false)
(false, false, true)

Read the last two lines carefully:

• the actual mass is \(1/2\);
• the ratio ceiling is \(2/3\);
• true certifies \(1/2\le2/3\);
• false refutes the unreversed proposal \(1/2\ge2/3\); and
• the final triple says cap zero is empty, cap one at threshold zero is empty, but cap five at threshold zero is not empty.

Inspect and check the exact project interfaces

import NonlinearDynamics.Random.RandomCocycles.SubadditiveBadBlockMeasure

open MeasureTheory
open NonlinearDynamics.Random.RandomCocycles

#check finiteOrbitVisitCount
#check natCast_finiteOrbitVisitCount_eq_birkhoffSum_indicator
#check integral_finiteOrbitVisitCount
#check finiteCenteredBadBlockSet
#check IsIntegrableSubadditiveProcessCandidate.nullMeasurableSet_finiteCenteredBadBlockSet
#check IsIntegrableSubadditiveProcessCandidate.centeredProcess_le_badBlockVisitCount
#check IsIntegrableSubadditiveProcessCandidate.measureReal_finiteCenteredBadBlockSet_le_rateRatio
#check DiscreteMatrixCocycle.centeredLogPlusBadBlockSet
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.centeredFeketeOffset_le_normalizedIntegral
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.measureReal_centeredLogPlusBadBlockSet_le_rateRatio

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

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

Neither command changes pro_reviewed: false; technical validation and human review are separate gates.

Common wrong turns

Treating the bad event as a long-time event

\(B_m(c)\) asks whether one witness exists among finitely many lengths. It does not mean:

• bad blocks occur infinitely often;
• witnesses occur after every cutoff;
• a normalized lower limit is below \(c\); or
• the process converges.

Those are different events with different quantifiers.

Replacing strict inequality by a weak one

At length four in the running example,

The block is not marked. Replacing \(\lt\) by \(\le\) changes the event.

Forgetting the orbit shift

At a marked start \(j\), the witness cost is

not \(Y_{\ell(j)}(\omega)\) unless the base happens to be the identity. The running example uses identity dynamics for arithmetic clarity. The theorem does not.

Calling the pointwise packing theorem measure theoretic

The public method is attached to an integrable candidate, but its proof body uses shifted subadditivity and positive-time nonpositivity. The integration field is consumed later, when the inequality is integrated.

Calling a finite measure a probability measure

The generic theorem assumes finite total mass, not total mass one. The source compiles a mass-two boundary. Probability normalization becomes important only when a later argument interprets a strict subunit ratio canonically.

Claiming that the auxiliary limit is Kingman’s theorem

The proof sends the elementary number \(H/(H+m)\) to one. It does not prove that \(Y_n(\omega)/n\), \(X_n(\omega)/n\), or any matrix growth observable converges.

What this module proves

It proves:

• a natural-valued finite orbit-visit count;
• the exact equality between its real cast and an indicator Birkhoff sum;
• exact finite visit-count integration under finite measure and preservation;
• null measurability of the finite centered strict bad-block event;
• a pointwise greedy-packing estimate on the buffered horizon;
• a generic finite-measure ratio with negative division made explicit;
• the integrated Fekete-offset lower-bound bridge; and
• the finite log-positive matrix-cocycle specialization.

It proves neither lower liminf nor Kingman convergence. It also proves no:

• almost-everywhere convergence;
• equality of a sample rate with the integrated Fekete rate;
• \(L^1\) convergence;
• limit-integral interchange;
• ergodicity of \(T\) or a powered map;
• signed logarithmic growth theorem;
• Lyapunov exponent;
• Oseledets filtration or splitting; or
• quantitative rate or concentration inequality.

The next chapters first pass from fixed finite caps to the union over all positive lengths, then build an arbitrarily-late rational-threshold event. Only later does an ergodic probability argument connect such events to a lower liminf.

Exercises with answers

1. Which candidate length is bad on amber? Only \(n=5\). At \(n=4\) the value equals the threshold, and strictness excludes it.
2. What is the bad event? \(B_5(-3/4)=\{\text{amber}\}\).
3. What is its probability? \(1/2\).
4. Why does blue contribute no visits? Its orbit remains blue and every centered value is zero, while all five thresholds are negative.
5. Why do twelve amber marks need only three retained intervals? The intervals \([0,5)\), \([5,10)\), and \([10,15)\) cover all starts \(0,\ldots,11\).
6. What is their total cost? Three copies of \(-4\), hence \(-12\).
7. Why is \(-45/4\le-9\)? Covered length \(15\) is at least marked count \(12\), and multiplying by \(-3/4\) reverses the comparison.
8. Compute the visit integral. \((12+0)/2=6\).
9. Compute the buffered-process integral. \((-16+0)/2=-8\).
10. Why is \(\delta=-1/2\) valid for every positive \(n\)? Because \(I_n/n=-1/2+1/(2n)\ge-1/2\).
11. Compute the theorem’s ceiling. \(\delta/c=(-1/2)/(-3/4)=2/3\).
12. What does the wrong sign rule predict? \(1/2\ge2/3\), which is false.
13. Is \(B_1(0)\) empty? Yes, because \(Y_1=0\) and the test is strict.
14. Is \(B_5(0)\) empty in this model? No. Amber is already bad at length two.
15. Where is probability normalization used in the generic theorem? Nowhere. The example uses it for a simple atomwise calculation.
16. Where is ergodicity used? Nowhere in this module.
17. What limit is taken? Only \(H/(H+m)\to1\) for fixed \(m\).
18. What major theorem is still absent? Any lower-liminf conclusion and Kingman’s samplewise convergence theorem.

Continue the dependency-ordered climb

The immediate predecessor is Finite Ordered Interval Packing for Nonpositive Subadditive Processes. The next textbook step is From Finite Centered Bad-Block Bounds to All-Positive-Length Control. The paired Development Notebook records the proof construction and source history. The finite orbit-visit count glossary chapter isolates the counting primitive.

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 theorem that this finite module does not yet prove.

J. Michael Steele. Kingman’s subadditive ergodic theorem, Annales de l’Institut Henri Poincare, Probabilites et Statistiques 25(1), 93-98, 1989. Steele gives an interval-decomposition proof of the full theorem. RMT-30 isolates and checks one finite bad-block measure bridge from that proof lineage.

Mathlib contributors. Indicator integration, Mathlib commit 81a5d257. The pinned library supplies the null-measurable indicator integration interface used by the checked proof.

Mathlib contributors. Elementary limits at infinity, Mathlib commit 81a5d257. The source uses tendsto_natCast_div_add_atTop only for the auxiliary finite-buffer coefficient.

The audited Lean source SHA-256 for this chapter is a8aee618a10f8434c1c33d8e433fd77e98ed3e5c8dee399e7d6fa323c5079b28.