Start with an exact scalar perturbation

Let the probability space contain one point, let the base map be the identity, and choose one-by-one generators

\[ G_j=[e^{r_j}],\qquad G_0=[e^r], \qquad r_j\longrightarrow r. \]

At horizon \(k\),

\[ G_j^k=[e^{kr_j}], \qquad \frac1k\log\lVert G_j^k\rVert=r_j. \]

Thus the signed integrated growth rate is exactly \(\lambda(G_j)=r_j\), and these rates converge to \(\lambda(G_0)=r\). If all \(r_j\) lie in a bounded interval, then both \(\lVert G_j\rVert\) and \(\lVert G_j^{-1}\rVert\) have common bounds.

This family establishes that the assumptions are compatible with contraction, neutrality, and expansion. It also exhibits full continuity in one commuting scalar family. It does not establish continuity for arbitrary matrix cocycles.

The scalar generators exp r j converge to exp r and have exact rates r j converging to r. Beside them, a general finite-horizon curve has one selected horizon k whose normalized integral lies below the limiting rate plus a chosen tolerance. Convergence at that horizon transfers the upper bound to perturbed rates.
FigureOne finite horizon carries the upper estimate: the scalar family has equality at every horizon. In the general proof, the limiting Fekete infimum supplies one positive horizon \(k\) near \(\lambda(G_0)\). Fixed-horizon convergence transfers that witness to \(G_j\), and every perturbed rate lies below its own horizon-\(k\) value.

The selected meaning of stochastic stability

The phrase stochastic stability is used for several different questions. RMT-36 makes one precise choice:

Sequential upper semicontinuity of the signed integrated real-log growth rate as the matrix generator varies uniformly over a fixed probability-preserving base.

The base map \(T\), probability measure \(\mu\), matrix dimension, and norm are fixed. For real constants \(M,K\), every generator in the sequence satisfies

\[ \lVert G_j(\omega)\rVert\le M,\qquad \lVert G_j(\omega)^{-1}\rVert\le K \]

at every sample point, and every \(G_j(\omega)\) is invertible. Uniform convergence means

\[ \sup_\omega\lVert G_j(\omega)-G_0(\omega)\rVert\longrightarrow0. \]

The conclusion is

\[ \forall\varepsilon\gt0,\quad \lambda(G_j)\le\lambda(G_0)+\varepsilon \quad\text{for all sufficiently large }j. \]

Equivalently, \(\limsup_j\lambda(G_j)\le\lambda(G_0)\). This is an upper bound on perturbed rates. It is not a matching lower bound.

Why fixed horizons converge

The cocycle product at horizon \(k\) is

\[ C_j^k(\omega)= G_j(T^{k-1}\omega)\cdots G_j(T\omega)G_j(\omega). \]

For a fixed \(k\), uniform generator convergence gives convergence of each factor at each of the finitely many orbit points. Continuity of matrix multiplication then gives

\[ C_j^k(\omega)\longrightarrow C_0^k(\omega). \]

This is UniformlyBoundedInvertibleGenerator.tendsto_value_of_tendstoUniformly. Pointwise invertibility makes every finite product nonzero, so continuity of the real logarithm yields

\[ \log\lVert C_j^k(\omega)\rVert \longrightarrow \log\lVert C_0^k(\omega)\rVert. \]

The Lean declaration is UniformlyBoundedInvertibleGenerator.tendsto_realLogNormObservable_of_tendstoUniformly.

Pointwise convergence is not enough to move through the integral. The common two-sided generator bounds give the horizon-\(k\) estimate

\[ \left|\log\lVert C_j^k(\omega)\rVert\right| \le k\bigl(\log^+M+\log^+K\bigr). \]

This is UniformlyBoundedInvertibleGenerator.abs_realLogNormObservable_le. The right side is a constant integrable function on a finite measure space. Dominated convergence therefore gives

\[ \int\log\lVert C_j^k\rVert\,d\mu \longrightarrow \int\log\lVert C_0^k\rVert\,d\mu, \]

formalized as UniformlyBoundedInvertibleGenerator.tendsto_integratedRealLogNorm_of_tendstoUniformly.

One idea, three languages Read across, then read the syntax map
A human says
Uniform generator convergence transfers each fixed finite product, and shared forward and inverse bounds provide one integrable absolute bound for its signed log norm.
On paper
For fixed \(k\), \(C_j^k(\omega)\to C_0^k(\omega)\) and \(\lvert\log\lVert C_j^k(\omega)\rVert\rvert\le k(\log^+M+\log^+K)\), hence \(\int\log\lVert C_j^k\rVert\,d\mu\to\int\log\lVert C_0^k\rVert\,d\mu\).
In Lean
tendsto_integratedRealLogNorm_of_tendstoUniformly\n    (hT : MeasurePreserving T μ μ)\n    (hG : TendstoUniformly\n      (fun n ↦ (G n : Ω → Matrix ι ι ℂ)) G₀ atTop)\n    (k : ℕ)
Syntax map
TendstoUniformly is convergence uniform in ω. k is fixed before the limit in the perturbation index n is taken. The common constants M and K are parameters of the generator bundle, so the dominator does not depend on n.

Why an infimum gives only the upper half

RMT-35 identifies the signed rate with a positive-horizon Fekete infimum:

\[ \lambda(G)=\inf_{k\ge1} \frac1k\int\log\lVert C_G^k(\omega)\rVert\,d\mu(\omega). \]

Given a real \(y\gt\lambda(G_0)\), convergence of the normalized finite-horizon sequence for \(G_0\) supplies some positive \(k\) with

\[ \frac1k\int\log\lVert C_0^k\rVert\,d\mu\lt y. \]

Fixed-horizon dominated convergence makes the same strict inequality true for \(G_j\) once \(j\) is large. Since an infimum is no larger than any one of its terms,

\[ \lambda(G_j) \le \frac1k\int\log\lVert C_j^k\rVert\,d\mu \lt y. \]

That argument is UniformlyBoundedInvertibleGenerator.eventually_integratedRealLogGrowthRate_lt. Choosing \(y=\lambda(G_0)+\varepsilon\) gives UniformlyBoundedInvertibleGenerator.eventually_integratedRealLogGrowthRate_le_add.

A horizontal roof at lambda zero plus epsilon blocks the eventually perturbed rates from above. Several rates may remain well below the limiting rate, illustrating that the theorem does not give a lower bound or full continuity.
FigureUpper does not mean two-sided: every sufficiently late perturbed rate stays below the \(\lambda(G_0)+\varepsilon\) roof. The proof permits downward displacement because an infimum transfers upper witnesses but does not provide a common lower witness.

The formal interface

UniformlyBoundedInvertibleGenerator packages a measurable generator, pointwise matrix invertibility, the bound by M, and the inverse bound by K. Its coercion lets the bundle be used as a function.

UniformlyBoundedInvertibleGenerator.toCocycle installs the generator over a fixed measure-preserving base. UniformlyBoundedInvertibleGenerator.hasIntegrableGeneratorLogTails derives the RMT-35 two-sided one-step integrability package on a finite measure space. UniformlyBoundedInvertibleGenerator.integratedRealLogGrowthRate then names the signed integrated Fekete rate of the resulting cocycle.

One idea, three languages Read across, then read the syntax map
A human says
Every positive tolerance eventually bounds the perturbed signed rates by the limiting signed rate plus that tolerance.
On paper
If \(G_j\to G_0\) uniformly within one shared two-sided bounded invertible class, then \(\forall\varepsilon>0,\ \lambda(G_j)\le\lambda(G_0)+\varepsilon\) eventually.
In Lean
theorem eventually_integratedRealLogGrowthRate_le_add\n    [IsProbabilityMeasure μ]\n    (hT : MeasurePreserving T μ μ)\n    (hG : TendstoUniformly\n      (fun n ↦ (G n : Ω → Matrix ι ι ℂ)) G₀ atTop)\n    {ε : ℝ} (hε : 0 < ε) :\n    ∀ᶠ n in atTop,\n      (G n).integratedRealLogGrowthRate hT ≤\n        G₀.integratedRealLogGrowthRate hT + ε
Syntax map
∀ᶠ n in atTop means that the property holds for every sufficiently large natural number n. The theorem is sequential because perturbations are indexed by ℕ. IsProbabilityMeasure μ fixes total mass one.

A lightweight standalone tutorial

The following Std file checks the scalar perturbation arithmetic without matrices, topology, or measure theory:

import Std

def scalarRate (r : Int) : Int := r

example (j : Nat) : scalarRate (5 - (j : Int)) = 5 - (j : Int) := by
  rfl

example (ε : Nat) (hε : 0 < ε) :
    scalarRate 2 ≤ scalarRate 2 + (ε : Int) := by
  simp [scalarRate, Int.ofNat_pos.mpr hε]

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

lean UpperStabilityTutorial.lean

This standalone tutorial checks only integer identities modeling an exact scalar rate and a positive upper tolerance. It does not establish uniform matrix convergence, dominated convergence, or a Fekete-rate theorem.

Try it in the repository NonlinearDynamics/Random/RandomCocycles/GrowthRateStability.lean
This full project command checks the exact Mathlib-backed matrix-cocycle module. It may require substantial initial disk space and build time. Lean’s elaborator constructs candidate proof terms and the kernel checks them against the formal declarations. That check does not by itself audit whether the formal statement matches a proposed scientific application. The displayed portable command runs lake env lean from the repository’s formalization directory with warnings treated as errors.
Full project check, from the repository root
cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomCocycles/GrowthRateStability.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

LayerPublic declarations
Perturbation bundleUniformlyBoundedInvertibleGenerator; UniformlyBoundedInvertibleGenerator.toCocycle; UniformlyBoundedInvertibleGenerator.hasIntegrableGeneratorLogTails; UniformlyBoundedInvertibleGenerator.integratedRealLogGrowthRate
Fixed products and observablesUniformlyBoundedInvertibleGenerator.tendsto_value_of_tendstoUniformly; UniformlyBoundedInvertibleGenerator.tendsto_realLogNormObservable_of_tendstoUniformly; UniformlyBoundedInvertibleGenerator.abs_realLogNormObservable_le; UniformlyBoundedInvertibleGenerator.tendsto_integratedRealLogNorm_of_tendstoUniformly
Upper stabilityUniformlyBoundedInvertibleGenerator.eventually_integratedRealLogGrowthRate_lt; UniformlyBoundedInvertibleGenerator.eventually_integratedRealLogGrowthRate_le_add

Decision ledger and exact nonclaims

The selected theorem concerns the growth-rate functional of a random matrix cocycle under perturbation of its generator. It does not formalize the zero-noise convergence of stationary measures sometimes called stochastic stability. It also does not formalize upper semicontinuity of random attractors in a set distance. Those are different state spaces, outputs, and hypotheses.

Within the selected cocycle setting, RMT-36 supplies no lower semicontinuity, full continuity, quantitative modulus, convergence rate, varying base map, varying probability measure, singular generator limit, infinite-dimensional operator result, Lyapunov spectrum, Oseledets splitting, invariant subspace stability, or random-attractor statement.

The shared inverse bound is not decorative. It prevents finite products from approaching singular collapse without control and supplies the negative half of the dominated-convergence envelope. Pointwise invertibility is still recorded separately because Lean’s total matrix inverse is defined even for a singular matrix.

References

  1. 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.
  2. J. Bochi, “Genericity of zero Lyapunov exponents,” Ergodic Theory and Dynamical Systems 22(6), 1667–1696 (2002), doi:10.1017/S0143385702001165. The paper provides a continuous-cocycle setting in which integrated top exponents are treated as an upper-semicontinuous functional.
  3. L. Backes, A. Brown, and C. Butler, “Continuity of Lyapunov exponents for cocycles with invariant holonomies,” Journal of Modern Dynamics 12, 223–260 (2018), doi:10.3934/jmd.2018009.
  4. M. Viana and J. Yang, “Continuity of Lyapunov exponents in the \(C^0\) topology,” Israel Journal of Mathematics 229, 461–485 (2019), doi:10.1007/s11856-018-1809-7. References 3 and 4 illustrate that stronger continuity conclusions require additional dynamical structure or hypotheses absent from RMT-36.
  5. J. F. Alves, V. Araújo, and C. H. Vásquez, “Stochastic stability of diffeomorphisms with dominated splitting,” arXiv:math/0404160. This is a primary-source example of the distinct zero-noise stationary-measure usage.
  6. J. C. Robinson, “Stability of random attractors under perturbation and approximation,” Journal of Differential Equations 186(2), 652–669 (2002), doi:10.1016/S0022-0396(02)00038-4. This reference represents a distinct attractor upper-semicontinuity setting, not the cocycle-rate theorem formalized here.
  7. Upper semicontinuity.
  8. Upper Stability of Signed Integrated Cocycle Growth.