Finite-Time Cocycle Norms in Lean: Row Sums, Extended Logs, and the Zero Boundary

This is the proof-to-prose companion for formalization/NonlinearDynamics/Random/RandomCocycles/NormObservables.lean. It covers all fourteen public declarations in exact source order. There are no private declarations in the module.

The immediate predecessor, One-Sided Discrete Matrix Cocycles in Lean, constructs \(\Phi(k,\omega)\), proves its later-block-left time split, and establishes ordinary measurability of every finite value. Reusable terminology is developed under one-sided discrete matrix cocycle , induced infinity operator norm , and extended log-norm observable . The parallel textbook treatment is Finite-Time Norm and Extended-Log-Norm Observables for Matrix Cocycles.

Choose a route up

Learning objectives

By the summit, a reader should be able to:

1. state the exact maximum absolute row-sum norm selected by the module;
2. explain why that norm is induced by the vector supremum norm;
3. distinguish it from the Frobenius, spectral, and entrywise supremum norms;
4. compute the norm of a small complex matrix from its rows;
5. explain what finite-time perturbation control the norm supplies;
6. identify the extra theorem needed before calling the cocycle a derivative or Jacobian cocycle;
7. state the norm observable at an arbitrary finite time;
8. explain why time-zero norm one requires a nonempty index type;
9. recover the generator norm at time one;
10. derive submultiplicativity from the exact RMT-13 cocycle identity;
11. keep the later shifted block on the left in that inequality;
12. reconstruct norm measurability from measurable matrix entries;
13. explain why the proof avoids an unproved Borel-space identification;
14. distinguish a nonnegative real norm from its extended nonnegative representation;
15. explain why ENNReal.log sends zero to extended-real bottom;
16. contrast that convention with Real.log 0 = 0 in Lean;
17. prove that bottom occurs exactly at a zero cocycle value;
18. understand why the extended logarithm product law is unconditional;
19. derive finite-time log subadditivity even when a factor vanishes;
20. distinguish measurability from integrability;
21. evaluate every exported observable when the matrix index type is empty;
22. read every typeclass assumption in the declaration ledger; and
23. list the missing hypotheses and theorems before any Lyapunov conclusion.

Lineage, contribution, and boundary

Norm growth in products of matrices is classical. Furstenberg and Kesten’s 1960 paper studies long products under probabilistic assumptions, while Kingman’s 1968 work supplies a general subadditive ergodic framework. Those sources explain why logarithmic norm observables matter historically, but RMT-14 proves neither result and imports neither theorem (Furstenberg and Kesten, 1960; Kingman, 1968).

The local contribution is narrower: a convention-complete, finite-time Lean layer above the already checked cocycle. It freezes one norm, makes its coordinate formula public, proves measurability without assuming a topological compatibility claim, selects an exact zero convention for the logarithm, proves the resulting subadditive inequality, and retains both positive- and zero-dimensional matrix spaces.

From a matrix action to one growth number

Suppose a state perturbation \(v\) is carried forward by the cocycle value \(\Phi(k,\omega)\). If vectors carry the supremum norm, then the induced operator norm gives

This is a finite-time upper bound. If \(N_k(\omega)\) is large, some direction may be strongly amplified. If it is small, every input vector is controlled in that norm. The single number forgets the direction of strongest action, the geometry of invariant subspaces, cancellations among entries, and the rest of the singular-value profile.

In nonlinear dynamics, a derivative cocycle can transport an infinitesimal perturbation along an orbit. That physical picture motivates norm growth, but the present Lean structure stores an arbitrary measurable complex matrix generator. No theorem here identifies it with a derivative, proves differentiability of a nonlinear map, or relates matrix dimension to a tangent space. The physics is an intended consumer, not a premise hidden in the API.

Figure: the checked pipeline first compresses a finite cocycle matrix to absolute row totals and then keeps the largest row. The extended logarithm has two explicit branches: a nonzero norm gives a finite extended-real value, while zero gives bottom. The plate shows no probability average, time normalization, limit, exponent, or invariant direction.

The maximum absolute row-sum formula

For a finite matrix \(M=(M_{ij})\), define

This is the operator norm induced by the supremum norm on coordinate vectors. For every row \(i\), the triangle inequality gives

Taking the maximum over rows bounds the output supremum norm. In a nonempty finite coordinate space, a suitable choice of phases reaches the largest row sum, so this formula agrees with the induced operator norm. Mathlib exposes that agreement in its matrix norm API (Mathlib matrix norm documentation).

A checkable complex example

Consider

The first absolute row sum is \(1+2=3\). The second is \(1+\tfrac12=\tfrac32\). Therefore

These are toy values for teaching, not measurements or empirical claims.

Declaration 1: normObservable

The first definition turns each finite cocycle value into a real number:

def normObservable (C : DiscreteMatrixCocycle (ι := ι) μ) (k : ℕ) : Ω → ℝ :=
  fun ω ↦ ‖C.value k ω‖

The output is a function of the initial outcome \(\omega\). Time \(k\) is a fixed natural-number parameter. Nothing is integrated, averaged, normalized by \(k\), or sent to a limit.

Declaration 2: normObservable_eq_rowSumSup

The second declaration publishes the exact coordinate meaning:

Lean represents each absolute entry by its nonnegative norm ‖…‖₊, forms a finite sum, then uses Finset.univ.sup over rows. The final nonnegative real is coerced to a real. The proof is exactly Mathlib’s Matrix.linfty_opNorm_def specialized to the cocycle value.

Publishing the formula serves two purposes. Readers can audit the norm convention without tracing scoped instances, and the later measurability proof has a finite coordinate expression it can rebuild from already checked measurable operations.

Time zero and one expose the normalization

Declaration 3: normObservable_zero

When \(\iota\) is nonempty, the time-zero cocycle value is the identity matrix, and its induced infinity norm is one:

The theorem is an equality of functions, not merely a pointwise statement. Lean uses function extensionality and simplifies the RMT-13 time-zero value. The signature includes [Nonempty ι]. That assumption is mathematical, not proof noise: it guarantees that the identity has at least one diagonal entry equal to one.

Declaration 4: normObservable_one

At time one, the cocycle value is the generator itself, so

This identity needs no positive-dimensional hypothesis. In empty dimension, both sides are the norm of the unique empty matrix and are therefore zero.

Submultiplicativity follows the cocycle split

RMT-13 proved the exact finite-time identity

The earlier \(m\)-step block acts first from the right. The later \(k\)-step block begins at the shifted base point \(T^m\omega\) and acts from the left. Applying matrix norm submultiplicativity gives

Declaration 5: normObservable_add_le

The Lean proof has two essential moves. It rewrites the cocycle value using C.value_add, then closes the goal with norm_mul_le. There is no induction in this module because RMT-13 already paid the algebraic cost of proving the cocycle identity.

The order still matters. The inequality is scalar and its final product is commutative, but each scalar norm must be attached to the correct matrix block and base point. Writing the later block at \(\omega\) instead of \(T^m\omega\) would be false for a changing environment.

At \(m=0\), the right factor is the time-zero norm. In positive dimension it is one. In empty dimension all three norms are zero, so the inequality remains valid without Nonempty. At \(k=0\), the later block is the identity at the shifted base point in positive dimension, while the same empty-dimensional convention again yields zero throughout.

Measurability is rebuilt entry by entry

The cocycle structure uses the project’s entrywise measurable space for complex matrices. The selected norm arrives through a scoped analytic instance. It would be tempting to say that every norm is continuous and hence measurable, but that shortcut would require a checked theorem identifying the project-owned matrix measurable space with the Borel measurable space induced by this particular norm topology.

RMT-14 makes no such identification. Instead, it proves measurability from the row-sum formula using operations whose compatibility with the project matrix measurable space is already explicit.

Declaration 6: measurable_normObservable

Fix \(k\). The proof climbs through five finite stages:

1. C.measurable_value k gives ordinary measurability of the complex matrix-valued function.
2. RandomMatrix.measurable_entry extracts every coordinate \(\omega\mapsto\Phi(k,\omega)_{ij}\) measurably.
3. .nnnorm turns each complex entry into a measurable nonnegative real magnitude.
4. Finset.measurable_sum builds each finite row sum.
5. An induction over a finite row set uses measurable binary maximum to build Finset.sup; coercion then returns a measurable real function.

The final convert step aligns that explicit finite supremum with Matrix.linfty_opNorm_def. This is a proof of ordinary measurability on \(\Omega\), stronger than an almost-everywhere statement and independent of the measure \(\mu\)’s total mass.

The empty finite supremum is part of the proof

The finite-supremum induction begins at the empty row set, where the nonnegative-real supremum is zero. This is not merely an implementation detail. It is exactly the boundary behavior later exported for empty matrix dimension. The measurability theorem therefore needs no Nonempty ι.

What is and is not measurable here

The theorem proves measurability of \(N_k:\Omega\to\mathbb R\) for each fixed natural \(k\). It does not put a measurable structure on the pair \((k,\omega)\), prove integrability of \(N_k\), prove measurability of a time supremum, or establish any uniform-in-time bound.

Why the logarithm lives in the extended reals

For a positive real \(x\), logarithms convert multiplication into addition:

Matrix products can vanish. A zero generator, a singular factor, or a product of nonzero matrices with incompatible image and kernel can produce the zero matrix. If \(N_k(\omega)=0\), the physically and analytically meaningful logarithmic endpoint is negative infinity.

Lean’s Real.log is a total function and simplifies Real.log 0 to zero. That convention is useful for a total real function, but it would collapse two opposite growth statements:

• norm one has logarithm zero;
• norm zero would also be assigned real logarithm zero.

RMT-14 instead uses Mathlib’s ENNReal.log. Its input is an extended nonnegative real and its output is an EReal, the real line completed with bottom and top. The official Mathlib API defines log 0 = ⊥, proves strict monotonicity, and makes the logarithm of a product an unconditional sum (extended logarithm documentation).

Declaration 7: logNormObservable

The definition is short because the convention is carried by the types:

def logNormObservable (C : DiscreteMatrixCocycle (ι := ι) μ) (k : ℕ) : Ω → EReal :=
  fun ω ↦ ENNReal.log ‖C.value k ω‖ₑ

The notation ‖M‖ₑ packages the nonnegative norm as an extended nonnegative real. For these finite matrices it does not invent an infinite matrix norm. It chooses the domain on which the extended logarithm has an exact zero endpoint.

Declaration 8: logNormObservable_eq_bot_iff

The next theorem identifies the boundary completely:

Mathlib first reduces extended log bottom to extended norm zero. The norm zero criterion then reduces the matrix to zero. This is pointwise and exact. It does not say that the zero event has measure zero, positive measure, or any particular probability.

Declaration 9: logNormObservable_zero

In positive dimension, time-zero norm is one, so time-zero log norm is zero:

Like its norm counterpart, the theorem needs [Nonempty ι]. In empty dimension the identity matrix is also the zero matrix, so its extended log norm is bottom instead.

Declaration 10: logNormObservable_one

At one step,

No nonvanishing hypothesis appears. A zero generator value produces bottom, exactly as the definition intends.

Extended-log measurability preserves bottom

Declaration 11: measurable_logNormObservable

The proof reuses declaration 6. A measurable real norm is mapped to an extended nonnegative real with ennreal_ofReal. Then Mathlib’s Measurable.ennreal_log proves the extended logarithm measurable (extended log and exponential documentation).

The simplifier theorem ofReal_norm connects the norm’s nonnegativity to the ‖M‖ₑ notation. Bottom remains an ordinary value of the codomain EReal, so zero matrices do not need to be removed from the domain before measurability can be stated.

This theorem is still not an integrability theorem. Extended-real functions that are measurable may take bottom, may have infinite positive or negative parts, and need not satisfy whichever integrability notion a future ergodic argument requires.

The logarithm turns finite products into a subadditive process

Combine the cocycle split and matrix norm inequality:

Monotonicity of ENNReal.log preserves the inequality. Its product law then gives a sum:

Declaration 12: logNormObservable_add_le

The proof mirrors that mathematics in three checked steps:

1. rewrite the total value with C.value_add;
2. lift nnnorm_mul_le through monotonicity of the extended logarithm;
3. rewrite the logarithm of the product with ENNReal.log_mul_add.

The theorem needs no assumption that either matrix block is nonzero. If one block is zero, the full product is zero, the left side is bottom, and the inequality remains valid in the extended arithmetic. This is the main reason to choose EReal before entering any asymptotic theory.

Positive and empty dimensions are different branches

For a nonempty index type, the identity matrix has one on its diagonal and operator norm one. For an empty index type, there are no rows and no entries. There is exactly one empty matrix. It is simultaneously the additive zero and the multiplicative identity because two functions on an empty domain are equal.

The maximum over an empty collection of nonnegative row sums is zero. Thus, for every \(k\) and \(\omega\),

This explains why the general definitions, measurability results, and subadditive inequalities need no positive-dimension assumption, while the two time-zero normalizations do.

Declaration 13: normObservable_eq_zero_of_isEmpty

Under [IsEmpty ι], the theorem proves equality of functions:

The proof first shows every cocycle value is the zero matrix by matrix extensionality. Any requested row index can be eliminated because the index type is empty. Simplifying the norm then gives zero.

Declaration 14: logNormObservable_eq_bot_of_isEmpty

The final theorem proves

for every finite time. Rather than recomputing the logarithm, it uses declaration 8 and proves that the cocycle matrix is zero by the same empty-index extensionality argument.

Why not ban dimension zero?

Keeping the empty type valid makes theorem assumptions match their actual dependencies. Results that only need finiteness should say so. Results that normalize the identity to one must say they need a coordinate. This prevents a global [Nonempty ι] assumption from hiding the exact logical location of positive dimension, and it lets downstream constructions choose their own dimension policy.

Assumption ledger

The module works inside one namespace and fixes the following shared context:

The scalar field is already \(\mathbb C\) in the inherited DiscreteMatrixCocycle. This module does not generalize the observable to arbitrary normed semirings. The pointwise norm inequality may have a broader algebraic life, but the present interface deliberately stays on the checked measurable complex matrix foundation.

Declaration-by-declaration assumption summary

No declaration adds a ProbabilityMeasure, an ergodicity hypothesis, an invertible base, or a nonzero-determinant hypothesis.

The complete declaration map

The table below follows the source exactly. Names are not grouped by topic at the expense of order.

Namespace and dot notation

All fourteen declarations live in NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle. Because the cocycle is the first explicit argument, Lean supports dot notation:

import NonlinearDynamics.Random.RandomCocycles.NormObservables

open Matrix MeasureTheory
open scoped Matrix.Norms.Operator

noncomputable section

#check NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.normObservable
#check NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.logNormObservable
#check NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.logNormObservable_add_le

This snippet is complete as a Lean file. It inspects the three declarations without constructing a concrete cocycle.

Run the checked module

From the repository root:

source "$HOME/.elan/env"
cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomCocycles/NormObservables.lean
lake build NonlinearDynamics.Random.RandomCocycles.NormObservables

The first command checks the source file directly and promotes warnings to errors. The second builds the named module through Lake’s dependency graph. Starting from the repository root, build the complete formalization and check the public teaching content:

source "$HOME/.elan/env"
cd formalization
lake build

cd ..
make content-hygiene
make site-check

The toolchain and Mathlib revision are pinned by formalization/lean-toolchain and formalization/lakefile.toml. The pinned local checkout is the API authority if current online documentation differs.

Failure modes this interface blocks

Physics and mathematics interpretation

Finite-time amplification

If the generator later becomes a Jacobian along a nonlinear orbit, the matrix product is the chain-rule candidate for tangent transport. Then \(N_k\) bounds how much an initial coordinatewise perturbation can grow after \(k\) steps. The logarithm converts multiplicative amplification into additive scale, which is why normalized logarithms appear in Lyapunov theory.

RMT-14 formalizes only the matrix side of that sentence. A later derivative bridge must define the nonlinear state space, differentiability assumptions, coordinate representation, chain rule, and equality between the derivative iterate and this generator-presented product. Without that bridge, calling C.generator a Jacobian would be an interpretation, not a theorem.

Contraction to zero

If a finite product annihilates every vector, its operator norm is zero. The extended log norm is bottom, representing the endpoint below every finite real number. This is stronger information than “very negative”: it records exact finite-time annihilation.

It does not tell us how often annihilation occurs. That question would require a probability measure or at least a raw measure query about the zero event. The structure’s measure-preserving base alone does not assign total mass one and does not force that event to be negligible.

Coordinate dependence

The maximum-row-sum norm depends on the chosen coordinate presentation. In a fixed finite dimension, many norms are equivalent for asymptotic exponential rates under suitable hypotheses, but RMT-14 neither proves such equivalence nor defines a rate. The advantage here is computational and formal clarity: the norm has a finite row-sum formula, is submultiplicative, and is measurable by the existing entrywise interface.

Bottom is a value, not a proof failure

EReal is the extended real line with bottom and top (Mathlib extended-real documentation). A bottom-valued observable is still a total measurable function. This design lets theorem statements include zero matrices rather than hiding them behind a partial logarithm or a nonzero side condition.

Strict finite-time nonclaims

RMT-14 does not prove or define:

• integrability of \(N_k\), \(L_k\), their positive parts, or their negative parts;
• almost-everywhere finiteness of \(L_k\) as an ordinary real number;
• that the cocycle value is nonzero or invertible at any time;
• that the zero event has measure zero, positive measure, or a probability;
• a probability measure on \(\Omega\) or a proof that \(\mu(\Omega)=1\);
• sigma-finiteness, finite measure, or any total-mass hypothesis;
• ergodicity, mixing, independence, identical distribution, stationarity in law, or a Bernoulli base;
• a two-sided cocycle, negative time, or invertibility of the base map;
• a normalized quantity \(k^{-1}L_k\), including a convention at \(k=0\);
• convergence in any mode as \(k\to\infty\);
• a deterministic or outcome-dependent Lyapunov exponent;
• a Furstenberg-Kesten theorem, Kingman subadditive ergodic theorem, or multiplicative ergodic theorem;
• an Oseledets filtration, splitting, invariant direction, stable bundle, unstable bundle, dominated splitting, or hyperbolicity;
• equality between the maximum-row-sum norm and the Euclidean spectral norm, Frobenius norm, spectral radius, or largest singular value;
• dimension-independent constants comparing different matrix norms;
• continuity in \(\omega\), continuity in a parameter, or differentiability;
• a Jacobian or derivative representation of the generator;
• a nonlinear map, flow, ordinary differential equation, stochastic differential equation, or chain-rule theorem;
• a law of the norm observable, expectation, moment, tail bound, concentration estimate, or large-deviation principle;
• any statement uniform in time, matrix dimension, environment, or cocycle; or
• any infinite-dimensional operator result.

The exact theorem is finite and sharp: two measurable observables, their normalizations and boundary values, and the pointwise inequalities inherited from the finite cocycle equation.

Exercises with solutions

Exercise 1: compute a row-sum norm

For

compute the selected norm.

Solution. The absolute row sums are \(3\) and \(4\), so the maximum absolute row-sum norm is \(4\).

Exercise 2: distinguish norms

Does declaration 2 identify \(N_k\) with the largest singular value?

Solution. No. It identifies the norm with the maximum absolute row sum, the operator norm induced by vector supremum norm. The Euclidean spectral norm is a different choice.

Exercise 3: read time one

If the generator is zero at \(\omega\), what are \(N_1(\omega)\) and \(L_1(\omega)\)?

Solution. The one-step matrix is zero, so the norm is zero and the extended log norm is bottom.

Exercise 4: preserve the base shift

Write the norm inequality at \(m=2\) and \(k=3\).

Solution. It is

The later three-step block begins after the first two base steps.

Exercise 5: identify the measurable building blocks

Why does the proof use nonnegative real entry norms before coercing back to real numbers?

Solution. Finite sums and finite suprema of nonnegative values match Mathlib’s exact row-sum formula directly. Their measurability can be built from entry measurability, and the final coercion to real numbers is measurable.

Exercise 6: reject a continuity shortcut

Why does the source not call a theorem saying norms are continuous?

Solution. The cocycle values use the project’s entrywise matrix measurable space, while the norm is installed by a scoped analytic instance. The module does not assume or prove that these structures form the relevant Borel pair, so it proves measurability from coordinates instead.

Exercise 7: compare two zeros

Why is Real.log 0 = 0 unsuitable for this observable?

Solution. Norm one also has logarithm zero. Using the total real logarithm would therefore make a zero matrix and a norm-preserving unit scale indistinguishable at the endpoint. ENNReal.log sends zero to bottom instead.

Exercise 8: inspect empty dimension

What is the time-zero cocycle value when \(\iota\) is empty?

Solution. It is the unique empty matrix. That matrix is both identity and zero. Its row-sum norm is zero, and its extended log norm is bottom.

Exercise 9: locate Nonempty

Which exported results require positive dimension?

Solution. Only normObservable_zero and logNormObservable_zero. The definitions, inequalities, measurability theorems, one-step identities, boundary criterion, and explicit empty-dimensional results do not.

Exercise 10: test a vanishing product

Can two nonzero square matrices have zero product, and does declaration 12 still apply?

Solution. Yes. The image of the right factor can lie in the kernel of the left factor. Declaration 12 is unconditional, so the full log norm becomes bottom and the inequality remains valid.

Exercise 11: separate measurability and integrability

Does measurable_logNormObservable prove the log norm has finite expectation?

Solution. No. The theorem assumes no probability normalization and proves no positive- or negative-part integral bound. It only proves ordinary measurability.

Exercise 12: locate the future theorem input

Which declaration resembles the subadditivity hypothesis of a subadditive ergodic theorem?

Solution. logNormObservable_add_le. A future application must still match the exact indexing convention and supply the theorem’s measure, stationarity, integrability, and other hypotheses.

Exercise 13: reject a derivative claim

Does the name “cocycle” prove that the generator is a Jacobian?

Solution. No. The structure stores an arbitrary measurable complex matrix generator. A derivative interpretation needs a separately formalized nonlinear map, differentiability, coordinate identification, and chain rule.

Exercise 14: inspect the top endpoint

Can the finite matrix norm itself be top?

Solution. The matrix norm is a real number and is therefore finite. It is embedded in the extended nonnegative reals to obtain the exact logarithmic zero endpoint. The module does not produce top from a finite matrix norm.

The next ridge

RMT-14 now supplies the finite-time algebra and measurability that a growth theory can consume. The next responsible layer must decide exactly which extended-real or real-valued process enters the limit theorem, what integrability condition controls its positive and negative parts, whether zero matrices are allowed with bottom values, and how the raw measure becomes a probability measure if the chosen theorem requires one.

A subadditive ergodic application must also match the shifted indexing \(L_{m+k}(\omega)\le L_k(T^m\omega)+L_m(\omega)\) to the theorem’s convention. If a deterministic almost-sure exponent is desired, ergodicity must be added explicitly. If an Oseledets splitting is desired, the project will need a substantially stronger multiplicative interface, often including invertibility or a carefully chosen noninvertible variant and appropriate log-integrability.

The derivative branch remains separate. It can later prove that Jacobians of a differentiable nonlinear system generate this cocycle and then import the finite-time estimates. Until that bridge is checked, RMT-14 should be read as abstract complex matrix dynamics.

The immediate successor, Finite-Horizon Log-Positive Cocycle Integrability in Lean, defines the real positive-log envelope, bounds each finite horizon by a sum of one-step costs along the measure-preserving base orbit, and propagates one explicit generator integrability hypothesis to every fixed finite time. It also makes the information loss explicit: contraction and singular collapse both map to zero, so the envelope is not the Lyapunov observable and supplies no asymptotic limit.

References

The links below were checked on 2026-07-21. The pinned local Mathlib 4.32.0 checkout remains the exact API authority for the Lean proof.

Mathlib contributors. Mathlib 4.32.0 release, 2026. This is the dependency release selected by formalization/lakefile.toml.

Mathlib contributors. Matrices as normed spaces, Mathlib 4 documentation. This official page defines the scoped maximum-row-sum matrix norm, states Matrix.linfty_opNorm_def, proves matrix submultiplicativity through its normed-ring instance, and identifies the norm with the operator norm on supremum-normed coordinate functions.

Mathlib contributors. Extended nonnegative real logarithm, Mathlib 4 documentation. This official page defines ENNReal.log : ENNReal → EReal, including log zero as bottom, monotonicity, the exact bottom criterion, and the unconditional product-to-sum law.

Mathlib contributors. Extended logarithm and exponential, Mathlib 4 documentation. This official page proves continuity and measurability of the extended logarithm and supplies Measurable.ennreal_log.

Mathlib contributors. The extended real numbers, Mathlib 4 documentation. This official page defines EReal as the real line completed with bottom and top and records its order and coercion infrastructure.

Harry Furstenberg and Harry Kesten. “Products of Random Matrices”, The Annals of Mathematical Statistics 31(2), 457-469, 1960. This original paper is cited as historical motivation for normalized logarithmic growth of random matrix products. RMT-14 proves no asymptotic result from it.

J. F. C. Kingman. “The Ergodic Theory of Subadditive Stochastic Processes”, Journal of the Royal Statistical Society: Series B 30(3), 499-510, 1968. This original paper is cited to locate the later subadditive-ergodic ridge. RMT-14 proves only the finite pointwise inequality that such a future layer may consume.