On a one-point probability space, let a one-by-one matrix cocycle use the constant generator \([e^{-1}]\). At horizon \(n\), its value is \([e^{-n}]\), its norm is \(e^{-n}\), and its signed log norm is \(-n\). Therefore

\[ \frac1n\int\log\lVert C_n(\omega)\rVert\,d\mu(\omega)=-1 \qquad(n\ge1). \]

The integrated real-log growth rate is the general version of that long-run signed number.

Definition

For a matrix cocycle \(C\), define

\[ a_n=\int \log\lVert C_n(\omega)\rVert\,d\mu(\omega). \]

Under pointwise invertibility and integrable forward and inverse one-step log-positive norms, RMT-35 proves that \(a_n\) is subadditive and that \(a_n/n\) has a finite lower bound. Its integrated real-log growth rate is

\[ \lambda_{\mathrm{real}} =\lim_{n\to\infty}\frac{a_n}{n} =\inf_{n\ge1}\frac{a_n}{n}. \]

The word integrated means that each finite-horizon signed observable is integrated before taking the long-run limit. The word real-log distinguishes the signed logarithm from the clipped nonnegative quantity \(\log^+x=\max(0,\log x)\). The word growth includes negative contraction rates, zero neutral rates, and positive expansion rates.

A sequence of normalized signed integrals a one over one, a two over two, and later a n over n stays above negative J and approaches lambda, which equals the infimum over all positive horizons.
FigureDefinition with its analytic gate: integrated subadditivity organizes \(a_n/n\), while the inverse-tail budget \(J\) gives the finite floor \(-J\). Fekete’s lemma then identifies the limit with the positive-horizon infimum.

Why an inverse tail appears

Forward log-positive control only sees expansion. For the running generator \([e^{-1}]\),

\[ \log^+\lVert[e^{-1}]\rVert=0 \]

even though the signed value is \(-1\). Its inverse is \([e]\), whose log-positive norm is \(1\). In general the integrated inverse budget

\[ J=\int\log^+\lVert A(\omega)^{-1}\rVert\,d\mu(\omega) \]

gives

\[ -J\le\frac{a_n}{n}. \]

That finite floor is what prevents the real-valued Fekete sequence from escaping toward negative infinity.

In Lean

One idea, three languages Read across, then read the syntax map
A human says
Package the finite long-run signed rate from the subadditive integrated sequence and its inverse-tail lower bound.
On paper
Define \(\lambda_{\mathrm{real}}\) as the Fekete limit of \(a_n=\int\log\lVert C_n\rVert\,d\mu\), with \(-J\le a_n/n\).
In Lean
def integratedRealLogGrowthRate\n+    (C : DiscreteMatrixCocycle (ι := ι) μ)\n+    (hC : C.HasIntegrableGeneratorLogTails) : ℝ :=\n+  hC.subadditive_integratedRealLogNorm.lim
Syntax map
C is the cocycle. hC stores pointwise invertibility and the integrable forward and inverse generator tails. The return type ℝ records that this is a finite real rate. .lim is Mathlib’s Fekete limit for the checked subadditive sequence.

The exact convergence and infimum declarations are HasIntegrableGeneratorLogTails.tendsto_normalizedIntegratedRealLogNorm and HasIntegrableGeneratorLogTails.integratedRealLogGrowthRate_eq_sInf. Under a pre-ergodic probability base, HasIntegrableGeneratorLogTails.ae_tendsto_normalizedRealLogNormObservable also identifies this deterministic rate with normalized sample growth almost everywhere.

Try it in the repository NonlinearDynamics/Random/RandomCocycles/RealLogNormKingman.lean
This full project command checks the Mathlib-backed definition and theorems. It may require substantial initial disk space and build time. For a lightweight scalar arithmetic introduction, use the standalone Std tutorial in the linked Deep Dive.
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.

Boundaries

  • At time zero, the normalized expression is totalized as zero. The infimum defining the Fekete rate ranges over \(n\ge1\).
  • In empty matrix dimension, the checked rate is zero.
  • Singular generators are outside this signed theorem; Real.log 0 = 0 is a total-function convention, not a replacement for invertibility.
  • If the integrated log-positive growth rate is strictly positive, RMT-35 proves that it equals the signed rate.
  • Almost-everywhere convergence does not imply \(L^1\) convergence or justify moving the limit through the integral.

Reference

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.