Signed Real-Log Kingman Convergence in Lean

Start with the exact scalar boundary

Fix a real number \(r\). On the one-point probability space, use the identity base map and the one-by-one generator

\[ A=\begin{bmatrix}e^r\end{bmatrix}. \]

At horizon \(n\), the cocycle value is \(A^n=[e^{nr}]\). Its selected operator norm is \(e^{nr}\), so

\[ \frac{\log\lVert A^n\rVert}{n}=r \qquad(n\ge1). \]

Thus \(r=-1\) gives exact contraction, \(r=0\) gives neutral growth, and \(r=1\) gives exact expansion. These are not numerical experiments. The private Lean atlas checks the matrix power, its norm, the real logarithm, the integrability package, and the resulting Fekete rate for an arbitrary real \(r\), then instantiates all three signs.

Three one-dimensional constant cocycles have generator entries exp negative one, one, and exp one. Their horizon-n signed log norms are negative n, zero, and n, so their normalized signed rates are negative one, zero, and one. — FigureExact boundary atlas: a constant scalar generator \(e^r\) has \(C_n=e^{nr}\) and normalized signed log \(r\) at every positive horizon. The three displayed choices check contraction, neutral growth, and expansion. They exhibit the sign range of the theorem; they do not establish the general result.

The signed observable matters because the older positive-log observable clips contraction:

\[ \log^+ \lVert [e^{-n}]\rVert=0, \qquad \log \lVert [e^{-n}]\rVert=-n. \]

RMT-35 therefore uses the real-valued family

\[ X_n(\omega)=\log\lVert C_n(\omega)\rVert \]

constructed in RMT-34. Pointwise invertibility prevents a finite product from being zero, while integrable forward and inverse one-step tails control the positive and negative sides.

The deterministic ledger

Define the signed integral and its normalized version by

\[ a_n=\int X_n\,d\mu, \qquad \bar a_n=\frac{a_n}{n}. \]

The Lean names are integratedRealLogNorm and normalizedIntegratedRealLogNorm. Time zero is totalized as zero, but the Fekete infimum uses only positive horizons. The lemmas integratedRealLogNorm_zero, integratedRealLogNorm_eq_zero_of_isEmpty, normalizedIntegratedRealLogNorm_zero, and normalizedIntegratedRealLogNorm_eq_zero_of_isEmpty record those boundary values.

Measure preservation removes a shifted base iterate from an integral through integral_realLogNormObservable_at_base_iterate_eq. RMT-34 supplies signed pointwise subadditivity and finite-horizon integrability. Their integrated form is HasIntegrableGeneratorLogTails.integratedRealLogNorm_add_le; the packaged sequence result is HasIntegrableGeneratorLogTails.subadditive_integratedRealLogNorm.

The lower budget is the one-step integral integratedInverseGeneratorLogPlusNorm. Its nonnegativity is integratedInverseGeneratorLogPlusNorm_nonneg. The definitional bridge birkhoffSum_inverseGeneratorLogPlusNormObservable_eq identifies the abstract Birkhoff sum with the cocycle’s inverse-orbit sum, while integral_inverseOrbitLogPlusSum_eq evaluates its integral as \(n\) times the one-step integral.

Consequently, HasIntegrableGeneratorLogTails.neg_nat_mul_integratedInverseGeneratorLogPlusNorm_le_integratedRealLogNorm gives

\[ -n\int\log^+\lVert A(\omega)^{-1}\rVert\,d\mu(\omega) \le a_n. \]

The upper comparisons are HasIntegrableGeneratorLogTails.integratedRealLogNorm_le_integratedLogPlusNorm and HasIntegrableGeneratorLogTails.integratedRealLogNorm_le_nat_mul. After division by \(n\), the lower result becomes HasIntegrableGeneratorLogTails.neg_integratedInverseGeneratorLogPlusNorm_le_normalizedIntegratedRealLogNorm; HasIntegrableGeneratorLogTails.bddBelow_normalizedIntegratedRealLogNorm packages boundedness below.

The finite real number integratedRealLogGrowthRate is Mathlib’s Fekete limit for this subadditive sequence. The convergence theorem is HasIntegrableGeneratorLogTails.tendsto_normalizedIntegratedRealLogNorm, and HasIntegrableGeneratorLogTails.integratedRealLogGrowthRate_eq_sInf identifies the rate with the infimum of \(\bar a_n\) over \(n\ge1\). The comparison API consists of HasIntegrableGeneratorLogTails.integratedRealLogGrowthRate_le_normalized, HasIntegrableGeneratorLogTails.integratedRealLogGrowthRate_le_oneStep, HasIntegrableGeneratorLogTails.neg_integratedInverseGeneratorLogPlusNorm_le_integratedRealLogGrowthRate, and HasIntegrableGeneratorLogTails.integratedRealLogGrowthRate_le_integratedLogPlusGrowthRate.

One idea, three languages Read across, then read the syntax map

A human says

The long-run signed integrated rate is finite, is approached by normalized signed integrals, and is no larger than any positive-horizon normalized integral.

On paper

If \(a_{m+n}\le a_m+a_n\) and \(a_n/n\) is bounded below, then \(\lambda=\lim_n a_n/n=\inf_{n\ge1}a_n/n\), so \(\lambda\le a_k/k\) for \(k\ge1\).

In Lean

hC.tendsto_normalizedIntegratedRealLogNorm\nhC.integratedRealLogGrowthRate_eq_sInf\nhC.integratedRealLogGrowthRate_le_normalized hk

Syntax map

hC stores pointwise invertibility and both integrable one-step tails. Tendsto ... atTop (𝓝 λ) is ordinary sequence convergence to the neighborhood filter of λ. sInf is the greatest lower bound. The argument hk : k ≠ 0 excludes the totalized time-zero quotient.

The two samplewise rails

The deterministic rate must next be compared with each normalized sample path. The lower rail uses the centered lower-deviation theorem. Its exact input is HasIntegrableGeneratorLogTails.centeredRealLogFeketeOffset_le_normalizedIntegral; its endpoint is HasIntegrableGeneratorLogTails.ae_integratedRealLogGrowthRate_le_liminf_normalized. In symbols, for almost every \(\omega\),

\[ \lambda\le\liminf_{n\to\infty}\frac{X_n(\omega)}n. \]

The upper rail cannot assume nonnegativity: contraction makes that false. IsPointwiseInvertible.neg_birkhoffAverage_inverseGenerator_le_normalizedRealLogNorm instead places the negative inverse-tail average below normalized signed growth. Ordinary pointwise Birkhoff convergence makes that lower comparison eventually bounded; the packaged statement is IsPointwiseInvertible.ae_isBoundedUnder_ge_normalizedRealLogNormObservable. That hypothesis is exactly what the generalized RMT-29 phase-averaging theorem requires. The resulting endpoint is HasIntegrableGeneratorLogTails.ae_limsup_normalized_le_integratedRealLogGrowthRate:

\[ \limsup_{n\to\infty}\frac{X_n(\omega)}n\le\lambda \quad\text{almost everywhere}. \]

The squeeze is visual rather than an extra assumption:

A lower-liminf rail places the finite signed Fekete rate below the sample-path liminf. An upper-limsup rail places the limsup below the same rate. Since liminf never exceeds limsup, all three values coincide almost everywhere. — FigureTwo rails, one limit: centered lower deviations give \(\lambda\le\liminf X_n/n\). Phase averaging, enabled by the inverse-tail eventual lower bound, gives \(\limsup X_n/n\le\lambda\). Together with \(\liminf\le\limsup\), they force convergence almost everywhere.

The principal theorem is HasIntegrableGeneratorLogTails.ae_tendsto_normalizedRealLogNormObservable. It assumes IsProbabilityMeasure μ and PreErgodic C.base μ; preservation is already part of the cocycle. It concludes almost-everywhere convergence to C.integratedRealLogGrowthRate hC.

HasIntegrableGeneratorLogTails.integratedRealLogGrowthRate_eq_zero_of_isEmpty records that empty matrix dimension has rate zero. Finally, HasIntegrableGeneratorLogTails.integratedRealLogGrowthRate_eq_integratedLogPlusGrowthRate_of_pos identifies the signed and positive-log deterministic rates when the latter is strictly positive. That proof uses uniqueness of the two almost-everywhere sample limits, not an exchange of a limit with an integral.

A lightweight standalone tutorial

This small file imports only Std. It checks the arithmetic shape of the scalar atlas without matrices or measure theory:

import Std

def signedPrefix (rate : Int) (n : Nat) : Int :=
  (n : Int) * rate

example (n : Nat) : signedPrefix (-1) n = -(n : Int) := by
  simp [signedPrefix]

example (n : Nat) : signedPrefix 0 n = 0 := by
  simp [signedPrefix]

example (n : Nat) : signedPrefix 1 n = n := by
  simp [signedPrefix]

Save it as SignedRateTutorial.lean, then run on macOS or Linux:

lean SignedRateTutorial.lean

This standalone tutorial checks integer identities only. It does not import the repository definitions or establish any probabilistic convergence claim.

Try it in the repository NonlinearDynamics/Random/RandomCocycles/RealLogNormKingman.lean

This full project check elaborates the exact matrix, measure-theoretic, Fekete, and almost-everywhere statements. Lean’s elaborator constructs candidate proof terms and the kernel checks them against the formal declarations. That does not by itself audit whether those declarations match an intended application. The displayed command uses lake env lean with the repository’s pinned toolchain and dependency manifest.

Full project check, from the repository root

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

Resource note: this exact file uses the repository's pinned Lean and Mathlib dependencies. Initial project setup can require substantial disk space and build time. For a lightweight first step on macOS or Linux, use the page's standalone Lean-core or Std tutorial.

Complete public declaration map

Layer	Public declarations
Signed integrals	`integratedRealLogNorm`; `integratedRealLogNorm_zero`; `integratedRealLogNorm_eq_zero_of_isEmpty`; `integral_realLogNormObservable_at_base_iterate_eq`; `HasIntegrableGeneratorLogTails.integratedRealLogNorm_add_le`; `HasIntegrableGeneratorLogTails.subadditive_integratedRealLogNorm`
Inverse and forward controls	`integratedInverseGeneratorLogPlusNorm`; `integratedInverseGeneratorLogPlusNorm_nonneg`; `birkhoffSum_inverseGeneratorLogPlusNormObservable_eq`; `integral_inverseOrbitLogPlusSum_eq`; `HasIntegrableGeneratorLogTails.neg_nat_mul_integratedInverseGeneratorLogPlusNorm_le_integratedRealLogNorm`; `HasIntegrableGeneratorLogTails.integratedRealLogNorm_le_integratedLogPlusNorm`; `HasIntegrableGeneratorLogTails.integratedRealLogNorm_le_nat_mul`
Normalization and Fekete rate	`normalizedIntegratedRealLogNorm`; `normalizedIntegratedRealLogNorm_zero`; `normalizedIntegratedRealLogNorm_eq_zero_of_isEmpty`; `HasIntegrableGeneratorLogTails.neg_integratedInverseGeneratorLogPlusNorm_le_normalizedIntegratedRealLogNorm`; `HasIntegrableGeneratorLogTails.bddBelow_normalizedIntegratedRealLogNorm`; `integratedRealLogGrowthRate`; `HasIntegrableGeneratorLogTails.tendsto_normalizedIntegratedRealLogNorm`; `HasIntegrableGeneratorLogTails.integratedRealLogGrowthRate_eq_sInf`; `HasIntegrableGeneratorLogTails.integratedRealLogGrowthRate_le_normalized`; `HasIntegrableGeneratorLogTails.integratedRealLogGrowthRate_le_oneStep`; `HasIntegrableGeneratorLogTails.neg_integratedInverseGeneratorLogPlusNorm_le_integratedRealLogGrowthRate`; `HasIntegrableGeneratorLogTails.integratedRealLogGrowthRate_le_integratedLogPlusGrowthRate`
Kingman rails	`HasIntegrableGeneratorLogTails.centeredRealLogFeketeOffset_le_normalizedIntegral`; `IsPointwiseInvertible.neg_birkhoffAverage_inverseGenerator_le_normalizedRealLogNorm`; `IsPointwiseInvertible.ae_isBoundedUnder_ge_normalizedRealLogNormObservable`; `HasIntegrableGeneratorLogTails.ae_integratedRealLogGrowthRate_le_liminf_normalized`; `HasIntegrableGeneratorLogTails.ae_limsup_normalized_le_integratedRealLogGrowthRate`; `HasIntegrableGeneratorLogTails.ae_tendsto_normalizedRealLogNormObservable`
Boundary and rate comparison	`HasIntegrableGeneratorLogTails.integratedRealLogGrowthRate_eq_zero_of_isEmpty`; `HasIntegrableGeneratorLogTails.integratedRealLogGrowthRate_eq_integratedLogPlusGrowthRate_of_pos`

Exact nonclaims

RMT-35 proves pointwise almost-everywhere convergence. It does not prove \(L^1\) convergence, uniform integrability of the normalized signed family, interchange of limit and integral, a quantitative convergence rate, a concentration inequality, a conorm or singular-value limit, a Lyapunov spectrum, invariant subspaces, an Oseledets splitting, a derivative-cocycle bridge, or a stable-manifold theorem. It also does not claim that the deterministic rate equals an individual sample rate without the probability and pre-ergodicity assumptions in the endpoint.

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.
RMT-34: Real Log-Norm Integrability from Forward and Inverse Tails in Lean.
RMT-29: Subadditive Upper Limsup from Phase Averaging in Lean.
Integrated real-log growth rate.
Integrated Real-Log Growth and Signed Kingman Convergence.