Finite-Time Norm and Extended-Log-Norm Observables for Matrix Cocycles

Begin with two base points and two exact products

A matrix cocycle is a rule that reads a base state, applies the matrix stored there, moves the base state, and repeats. To make every symbol concrete, take the four-point base

Let the base map \(T:\Omega\to\Omega\) swap \(p_0\) with \(p_1\) and swap \(z_0\) with \(z_1\). Give each point mass \(1/4\). This uniform probability measure is preserved because \(T\) is a permutation, and every function on this finite discrete space is measurable.

The probability weights make the bundled cocycle legitimate, but none of the following pointwise arithmetic uses them. At the four base points, let the generator be

Regard these integer entries as complex numbers through the standard embedding. No genuinely complex arithmetic is needed for this example.

For a generator-presented cocycle, the two-step value is

The matrix at the starting state acts first and therefore appears on the right.

The positive-norm sample

Starting from \(p_0\), the shear acts before the stretch:

The two absolute row sums are \(2\) and \(2\). Hence its induced infinity operator norm, the maximum absolute row sum, is

Each factor has norm \(2\), so the submultiplicative theorem gives the valid but non-sharp budget \(2\leq2\cdot2=4\).

The exact-collapse sample

Starting from \(z_0\), the first factor keeps only the first coordinate and the second keeps only the second coordinate:

Both \(B_0\) and \(B_1\) are nonzero and have norm \(1\), yet their product is zero. Thus

This is the boundary that decides which logarithm the formalization needs.

Four finite-time values with different jobs

The target module defines the real norm observable

and the extended-real logarithm

Here \(\overline{\mathbb R}\), Lean’s EReal, is the real line with bottom \(\bot=-\infty\) and top \(\top=+\infty\). The subscript \(e\) only records the embedding of the nonnegative norm into the extended nonnegative reals before taking the logarithm.

The immediate successor module defines a different real-valued function,

This positive logarithm is an integrability envelope. It keeps expansion above one and clips contraction, neutral norm, and exact collapse to zero (Mathlib contributors).

At a positive horizon, one can also inspect finite quotients

The second quotient is extended-real arithmetic; dividing bottom by a positive finite number leaves bottom (Mathlib contributors). Neither quotient is defined by NormObservables.lean, and one fixed quotient is not a limit.

For the two running samples at horizon two, the entire ledger is

The agreement on the positive path does not identify the two logarithms. Their zero policies are intentionally different.

Controlled near-misses

Using the ordinary real logarithm at zero

Lean’s total real logarithm satisfies \(\operatorname{Real.log}(0)=0=\operatorname{Real.log}(1)\). Defining the collapse-sensitive observable with Real.log would make the zero matrix look indistinguishable from norm one. The target module therefore uses ENNReal.log into EReal.

Calling the positive logarithm a signed growth rate

\(\log^+(1/2)=0\), \(\log^+(1)=0\), and \(\log^+(0)=0\). That loss is useful when proving integrability of a nonnegative upper envelope, but it cannot represent contraction or collapse. The later log-positive observable does not replace \(L_k\).

Dividing by the final factor index

Horizon two contains the factors with indices zero and one. Its normalizing factor is \(2\), not the last index \(1\). Dividing by one would double the positive path’s finite normalized value and would divide by zero at horizon one.

Treating time-zero totalization as growth information

Classically, \(X_0/0\) is not a normalized growth rate. Much later, the generic real normalizedProcess defines the time-zero quotient to be zero because Lean’s real division is total. Its own theorem says that this value forgets \(X_0\) completely. Positive-time asymptotics may ignore that finite prefix; this page must not reinterpret it as a meaningful zero-step rate.

Keep the formal layers separate

The module NonlinearDynamics.Random.RandomCocycles.NormObservables contains fourteen public declarations. It proves finite pointwise algebra and measurability only. Probability normalization, integrability, normalized limits, Lyapunov exponents, and invariant splittings are separate later decisions.

Choose a route up

Learning objectives

By the summit, you should be able to reproduce both two-step products and every row-sum norm; distinguish \(N_k\), \(G_k\), \(L_k\), and their positive-time quotients by codomain and zero policy; explain why two nonzero factors may produce bottom; read seven Lean bridges token by token; run the bounded Std worksheet; reconstruct norm and log-norm measurability; follow the zero-safe subadditivity proof; audit all fourteen target declarations; and state precisely which integrability, law-level, normalized, ergodic, and Lyapunov conclusions remain outside this module.

In Lean: seven bridges from finite matrices to later normalization

The first five bridges belong to the target module. Bridge six is the real-valued positive-log successor, and bridge seven is a much later generic normalization utility. Their separate homes are part of the lesson.

Bridge one: the finite norm is an ordinary real

C.normObservable k ω : ℝ

Bridge two: cocycle splitting gives a norm budget

C.normObservable_add_le m k ω

Bridge three: the collapse-sensitive logarithm changes codomain

C.logNormObservable k ω : EReal

Bridge four: bottom means exact matrix collapse

C.logNormObservable_eq_bot_iff k ω

Bridge five: extended log norms are zero-safe subadditive

C.logNormObservable_add_le m k ω

Bridge six: the later positive logarithm is a real upper envelope

C.logPlusNormObservable_nonneg k ω

Bridge seven: normalization is a later real-process operation

NonlinearDynamics.Random.RandomCocycles.normalizedProcess X k ω

Try the exact target interfaces

import NonlinearDynamics.Random.RandomCocycles.NormObservables

open Matrix MeasureTheory
open scoped Matrix.Norms.Operator
open NonlinearDynamics.Random.RandomCocycles

#print DiscreteMatrixCocycle.normObservable
#check DiscreteMatrixCocycle.normObservable_eq_rowSumSup
#check DiscreteMatrixCocycle.normObservable_zero
#check DiscreteMatrixCocycle.normObservable_one
#check DiscreteMatrixCocycle.normObservable_add_le
#check DiscreteMatrixCocycle.measurable_normObservable
#print DiscreteMatrixCocycle.logNormObservable
#check DiscreteMatrixCocycle.logNormObservable_eq_bot_iff
#check DiscreteMatrixCocycle.logNormObservable_zero
#check DiscreteMatrixCocycle.logNormObservable_one
#check DiscreteMatrixCocycle.measurable_logNormObservable
#check DiscreteMatrixCocycle.logNormObservable_add_le
#check DiscreteMatrixCocycle.normObservable_eq_zero_of_isEmpty
#check DiscreteMatrixCocycle.logNormObservable_eq_bot_of_isEmpty

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

Inspect the separate positive-log and integrability successor

import NonlinearDynamics.Random.RandomCocycles.LogPlusIntegrability

open NonlinearDynamics.Random.RandomCocycles

#print DiscreteMatrixCocycle.logPlusNormObservable
#check DiscreteMatrixCocycle.logPlusNormObservable_nonneg
#check DiscreteMatrixCocycle.measurable_logPlusNormObservable
#check DiscreteMatrixCocycle.logPlusNormObservable_add_le
#print DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.integrable_logPlusNormObservable

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

Inspect the much later real normalization boundary

import NonlinearDynamics.Random.RandomCocycles.SubadditiveKingman

open NonlinearDynamics.Random.RandomCocycles

#print normalizedProcess
#check normalizedProcess_zero
#check normalizedProcess_update_zero

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

The analytic pipeline in one picture

The picture separates three structures that are often conflated:

• the base map decides where the later cocycle block begins;
• matrix multiplication decides how the blocks compose; and
• the norm and logarithm decide how to summarize the size of that composition.

Each layer has its own assumptions and its own failure modes.

Base camp: the checked cocycle input

The preceding random-matrix-theory milestone 13 (RMT-13) fixes a type \(\Omega\) of base states with a measurable-space structure, a finite matrix index type \(\iota\) with decidable equality, and a measure \(\mu\) on \(\Omega\). A bundled DiscreteMatrixCocycle μ stores:

• a base map \(T:\Omega\to\Omega\);
• a complex matrix generator \(A:\Omega\to M_\iota(\mathbb C)\);
• evidence that \(T\) preserves \(\mu\); and
• ordinary measurability of \(A\).

The measure-preserving field gives ordinary measurability of \(T\). RMT-13 therefore proves that every finite value

is measurable.

Random-matrix-theory milestone 14 (RMT-14), the target of this chapter, consumes exactly that interface. It does not add a probability instance for \(\mu\), and none of its finite-time pointwise inequalities uses measure preservation. The stored measurable structure matters for the two observable measurability theorems; the algebraic inequalities follow pointwise from the cocycle law and matrix norm.

That separation is useful. A theorem about one fixed \(\omega\) should not quietly depend on probability or ergodicity.

Camp one: why this particular matrix norm

For a finite complex matrix \(B=(B_{ij})\), define

For each row, add the absolute values of all entries. Then keep the largest row total. This is the maximum absolute row-sum norm.

Why does it control column-vector evolution? Give \(x=(x_j)\) the supremum norm

For the \(i\)-th output coordinate,

Taking the maximum over \(i\) yields

Mathlib proves that the row-sum formula agrees with the operator norm of the associated continuous linear map between finite function spaces carrying the supremum norm (Mathlib contributors).

This norm is not the Frobenius norm

and it is not the Euclidean spectral operator norm. It is chosen because Mathlib already gives it a submultiplicative normed-ring interface and because it naturally controls supremum-norm vector evolution.

The Lean scope is semantic

Finite matrices admit several useful norms. Mathlib therefore does not install one matrix norm globally as the only possible interpretation. The module opens

open scoped Matrix.Norms.Operator

before using ‖B‖. Under that scope, the notation means the maximum absolute row-sum norm. The theorem normObservable_eq_rowSumSup then exposes the precise finite formula in the public interface.

Camp two: define the finite-time norm observable

The first declaration is

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

Write

The result is a real-valued function on base states. It is nonnegative because it is a norm, but the definition does not package that fact into a nonnegative real codomain. The later logarithm deliberately takes the extended norm notation instead.

The second declaration states the exact formula

In Lean, the maximum is a Finset.sup in the nonnegative real type, and the final value is coerced to an ordinary real. This representation has a defined empty-family supremum, which will matter at the dimension boundary.

Camp three: zero time, one step, and a split

The RMT-13 value equations immediately give two normalization identities.

At time one,

because the one-step cocycle value is the generator. This theorem needs no positive-dimension assumption.

At time zero, the value is the identity matrix. In nonempty dimension,

This is normObservable_zero, and its Nonempty ι hypothesis is essential. In empty dimension the row maximum is taken over no rows and equals zero.

For a split into \(m\) early steps and \(k\) shifted later steps, substitute the cocycle law into the norm:

The theorem normObservable_add_le is pointwise and needs no Nonempty ι. Matrix norm submultiplicativity remains true on the trivial empty matrix space.

The order of terms mirrors matrix action. The shifted later block appears first in the product on the right because it is the left matrix factor. Since real multiplication commutes, the numerical product would be unchanged if written in the other order, but keeping the cocycle order visible prevents the underlying noncommutative statement from being forgotten.

Camp four: prove norm measurability from entries

It is tempting to say “norms are continuous, so the norm observable is measurable.” That shortcut would skip a project-specific seam. The random matrix measurable space was introduced entrywise, while the matrix norm comes from a scoped analytic instance. RMT-14 proves the connection directly rather than silently assuming those structures coincide in the needed way.

Start with the RMT-13 theorem

The proof of measurable_normObservable then climbs four finite closure steps.

Step one: extract a measurable entry

For fixed \(i,j\in\iota\),

is measurable by RandomMatrix.measurable_entry.

Step two: take the complex norm

The map

is measurable. The Lean proof uses the nonnegative norm method .nnnorm, so the values lie in the nonnegative reals.

Step three: sum one row

For each fixed row \(i\), the finite sum

is measurable by Finset.measurable_sum.

Step four: take the finite supremum over rows

The proof establishes measurability for the supremum over an arbitrary finite set of rows by induction. The empty supremum is the constant zero function. Inserting a row replaces the previous supremum by the maximum of two measurable functions. The Measurable.max closure theorem finishes that step.

Finally, Matrix.linfty_opNorm_def identifies this finite supremum with the scoped matrix norm, and coercion from nonnegative reals to reals preserves measurability.

This proof works in empty dimension because both finite induction base cases are explicit.

Camp five: why the ordinary real logarithm is the wrong totalization

For a positive real \(r\), the ordinary logarithm changes multiplication into addition:

The boundary \(r=0\) creates the design problem. Mathematically, one usually thinks of \(\log r\) tending to negative infinity as \(r\) decreases to zero. Lean’s Real.log is a total function on all real inputs and uses

That convention is useful for total theorem statements, but it is wrong for this observable. It would assign the same logarithmic value to norm zero and norm one:

Exact matrix collapse would look like neutral size.

The module instead uses two extended number systems.

Extended nonnegative real input

Mathlib’s type ℝ≥0∞, also named ENNReal, contains all nonnegative real numbers together with a top endpoint. The extended norm notation ‖B‖ₑ lands there.

Extended real output

Mathlib’s EReal contains the real line together with bottom and top endpoints. The function

ENNReal.log : ℝ≥0∞ → EReal

satisfies

is strictly increasing, and obeys an unconditional product-to-sum identity (Mathlib contributors).

The seventh public declaration is therefore

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

Write this value as \(L_k(\omega)\).

Camp six: bottom exactly characterizes collapse

The theorem logNormObservable_eq_bot_iff states

This is an exact pointwise equivalence, not merely one implication. It follows from the exact endpoint theorem

and the zero-norm criterion.

Bottom has a semantic role. It means the finite matrix value is exactly the zero matrix. It does not mean “unknown,” “not measurable,” “outside the domain,” or “the proof failed.”

When the matrix value is nonzero, its norm is positive and finite, so the extended log norm agrees with an ordinary finite real logarithm. The sign has a direct finite-time interpretation:

These are worst-case operator-norm budgets. A negative value gives a strict supremum-norm contraction bound for the complete finite matrix, but a positive value does not force every vector to grow, and a zero value does not identify the matrix with the identity. A nonzero singular matrix still has a finite log-norm value; bottom characterizes the zero matrix, not singularity.

The one-step and time-zero identities follow the norm layer:

and, when \(\iota\) is nonempty,

The subscript \(e\) in the first display only reminds us that the norm has been embedded into the extended nonnegative reals. It does not select a new matrix norm.

Measurability of the extended log norm

The theorem measurable_logNormObservable composes three checked maps:

1. the real-valued norm observable is measurable;
2. ENNReal.ofReal measurably embeds its nonnegative values; and
3. ENNReal.log is measurable.

The key Mathlib identity ofReal_norm reconciles the real norm followed by ENNReal.ofReal with the extended norm notation used in the definition.

Measurability reaches no further. It does not show that the extended value is integrable, that its positive or negative parts have finite integral, or that bottom occurs only on a null set.

Camp seven: the zero-safe subadditivity proof

The theorem logNormObservable_add_le states

Its proof is a compact four-link chain.

Link one: rewrite by the cocycle law

Replace the full matrix value with the shifted later block times the early block:

Link two: apply the extended norm product bound

The chosen matrix norm is submultiplicative:

The Lean proof starts with the nonnegative norm inequality nnnorm_mul_le, then coerces it into ENNReal.

Link three: use logarithm monotonicity

Because ENNReal.log is monotone, the preceding norm inequality can be passed through the logarithm without reversing its direction.

Link four: turn the product into a sum

Mathlib’s ENNReal.log_mul_add gives

for all extended nonnegative \(r\) and \(s\), including zero and top endpoints. For finite matrix norms only the finite and zero cases arise, but the theorem does not need to split them.

This makes the proof zero-safe. No assumption says that either block is invertible or nonzero.

Nonzero factors can still collapse

Even if both block matrices are nonzero, their product may be zero. For example,

are nonzero but \(DB=0\). Then the full log norm is bottom while both block log norms are zero, since both block norms equal one. The inequality reads

which is true. This example also shows why subadditivity is an inequality, not an equality.

Return to the two sample paths after the general theorem

Split each horizon-two path after its first factor, so \(m=k=1\). On the positive path, the norm theorem reads

and extended-log subadditivity reads

On the collapse path,

while both one-step extended logs are zero and the full extended log is bottom:

The positive-log successor instead reports \(G_2(z_0)=0\). The values satisfy their own theorems; they answer different questions.

Type the two ledgers yourself with Lean and Std

The project modules use Mathlib’s general matrices, measurable cocycles, extended reals, and operator norm. A learner can first verify the exact integer products, row-sum norms, and symbolic zero policies with a bounded file that imports only Std.

Create a scratch directory outside formalization/. Save this exact block as FiniteCocycleObservablesTutorial.lean:

import Std

namespace FiniteCocycleObservablesTutorial

structure Matrix2 where
  a00 : Int
  a01 : Int
  a10 : Int
  a11 : Int
  deriving Repr, DecidableEq

def Matrix2.mul (A B : Matrix2) : Matrix2 :=
  { a00 := A.a00 * B.a00 + A.a01 * B.a10
    a01 := A.a00 * B.a01 + A.a01 * B.a11
    a10 := A.a10 * B.a00 + A.a11 * B.a10
    a11 := A.a10 * B.a01 + A.a11 * B.a11 }

def Matrix2.linftyOpNorm (A : Matrix2) : Nat :=
  max (A.a00.natAbs + A.a01.natAbs)
      (A.a10.natAbs + A.a11.natAbs)

def A0 : Matrix2 :=
  { a00 := 1, a01 := 1, a10 := 0, a11 := 1 }

def A1 : Matrix2 :=
  { a00 := 1, a01 := 0, a10 := 0, a11 := 2 }

def B0 : Matrix2 :=
  { a00 := 1, a01 := 0, a10 := 0, a11 := 0 }

def B1 : Matrix2 :=
  { a00 := 0, a01 := 0, a10 := 0, a11 := 1 }

def positiveProduct : Matrix2 := A1.mul A0
def collapseProduct : Matrix2 := B1.mul B0

inductive LogValue where
  | bottom
  | zero
  | logOfNat (n : Nat)
  deriving Repr, DecidableEq

def positiveLogToken (n : Nat) : LogValue :=
  if n ≤ 1 then .zero else .logOfNat n

def extendedLogToken (n : Nat) : LogValue :=
  if n = 0 then .bottom
  else if n = 1 then .zero
  else .logOfNat n

structure FiniteQuotient where
  numerator : LogValue
  factorCount : Nat
  deriving Repr, DecidableEq

def normalizeAt (k : Nat) (value : LogValue) : Option FiniteQuotient :=
  if k = 0 then none else some { numerator := value, factorCount := k }

structure ObservableLedger where
  product : Matrix2
  productNorm : Nat
  factorNormBudget : Nat
  positiveLog : LogValue
  extendedLog : LogValue
  normalizedPositiveLog : Option FiniteQuotient
  normalizedExtendedLog : Option FiniteQuotient
  deriving Repr, DecidableEq

def ledger (left right : Matrix2) : ObservableLedger :=
  let product := left.mul right
  let norm := product.linftyOpNorm
  { product := product
    productNorm := norm
    factorNormBudget := left.linftyOpNorm * right.linftyOpNorm
    positiveLog := positiveLogToken norm
    extendedLog := extendedLogToken norm
    normalizedPositiveLog := normalizeAt 2 (positiveLogToken norm)
    normalizedExtendedLog := normalizeAt 2 (extendedLogToken norm) }

def positiveLedger : ObservableLedger := ledger A1 A0
def collapseLedger : ObservableLedger := ledger B1 B0

#eval [positiveProduct, collapseProduct]
#eval [A0.linftyOpNorm, A1.linftyOpNorm,
  positiveProduct.linftyOpNorm,
  B0.linftyOpNorm, B1.linftyOpNorm,
  collapseProduct.linftyOpNorm]
#eval positiveLedger
#eval collapseLedger
#eval [positiveLogToken 0, positiveLogToken 1, positiveLogToken 2]
#eval [extendedLogToken 0, extendedLogToken 1, extendedLogToken 2]
#eval normalizeAt 0 (.logOfNat 2)

example : positiveProduct =
    { a00 := 1, a01 := 1, a10 := 0, a11 := 2 } := by decide
example : collapseProduct =
    { a00 := 0, a01 := 0, a10 := 0, a11 := 0 } := by decide
example : positiveProduct.linftyOpNorm = 2 := by decide
example : collapseProduct.linftyOpNorm = 0 := by decide
example : positiveLedger.factorNormBudget = 4 := by decide
example : collapseLedger.factorNormBudget = 1 := by decide
example : positiveLedger.positiveLog = .logOfNat 2 := by decide
example : positiveLedger.extendedLog = .logOfNat 2 := by decide
example : collapseLedger.positiveLog = .zero := by decide
example : collapseLedger.extendedLog = .bottom := by decide
example : normalizeAt 0 (.logOfNat 2) = none := by decide

end FiniteCocycleObservablesTutorial

Open a terminal in that scratch directory and type:

source "$HOME/.elan/env"
elan run leanprover/lean4:v4.32.0 lean FiniteCocycleObservablesTutorial.lean

Resource label: small standalone Lean tutorial, ordinary Mac or Linux. This exact worksheet was executed with Lean 4.32.0 and printed:

[{ a00 := 1, a01 := 1, a10 := 0, a11 := 2 }, { a00 := 0, a01 := 0, a10 := 0, a11 := 0 }]
[2, 2, 2, 1, 1, 0]
{ product := { a00 := 1, a01 := 1, a10 := 0, a11 := 2 },
  productNorm := 2,
  factorNormBudget := 4,
  positiveLog := FiniteCocycleObservablesTutorial.LogValue.logOfNat 2,
  extendedLog := FiniteCocycleObservablesTutorial.LogValue.logOfNat 2,
  normalizedPositiveLog := some { numerator := FiniteCocycleObservablesTutorial.LogValue.logOfNat 2, factorCount := 2 },
  normalizedExtendedLog := some { numerator := FiniteCocycleObservablesTutorial.LogValue.logOfNat 2,
                             factorCount := 2 } }
{ product := { a00 := 0, a01 := 0, a10 := 0, a11 := 0 },
  productNorm := 0,
  factorNormBudget := 1,
  positiveLog := FiniteCocycleObservablesTutorial.LogValue.zero,
  extendedLog := FiniteCocycleObservablesTutorial.LogValue.bottom,
  normalizedPositiveLog := some { numerator := FiniteCocycleObservablesTutorial.LogValue.zero, factorCount := 2 },
  normalizedExtendedLog := some { numerator := FiniteCocycleObservablesTutorial.LogValue.bottom, factorCount := 2 } }
[FiniteCocycleObservablesTutorial.LogValue.zero,
 FiniteCocycleObservablesTutorial.LogValue.zero,
 FiniteCocycleObservablesTutorial.LogValue.logOfNat 2]
[FiniteCocycleObservablesTutorial.LogValue.bottom,
 FiniteCocycleObservablesTutorial.LogValue.zero,
 FiniteCocycleObservablesTutorial.LogValue.logOfNat 2]
none

Read the output in layers:

1. the two products are the positive matrix and the zero matrix;
2. the factor and product norms are \(2,2,2\) and \(1,1,0\);
3. the positive ledger stores the symbolic numerator \(\log2\) in both logarithm slots and the factor count two;
4. the collapse ledger stores zero for the positive logarithm and bottom for the extended logarithm;
5. the separate token lists expose the policies at norms zero, one, and two; and
6. conventional normalization at horizon zero returns none.

LogValue.logOfNat 2 is a symbolic token for the exact expression \(\log2\); the worksheet does not approximate a transcendental number. Likewise, LogValue.bottom models the zero policy without reimplementing Mathlib’s EReal. Every integer product, norm, budget, branch, and example is kernel-checked. The project-level types and theorems remain the full project interfaces in the earlier repository checks.

The worksheet’s normalizeAt 0 = none intentionally models the classical partial convention that normalization needs a positive horizon. It is not an implementation of the much later real normalizedProcess, whose explicitly totalized time-zero value is zero.

Camp eight: positive and empty dimensions

The module treats the matrix index type \(\iota\) as finite, but does not assume it is inhabited unless a theorem needs the familiar identity normalization.

Nonempty coordinate type

If \(\iota\) has at least one index, the identity matrix has one in every diagonal position and zero elsewhere. Every row has absolute sum one, so

Therefore

Only normObservable_zero and logNormObservable_zero add Nonempty ι to the module’s finite-index assumptions.

Empty coordinate type

If \(\iota\) is empty, there are no matrix entries. There is exactly one square matrix function, so the zero and identity matrices are equal. The maximum absolute row-sum formula takes the supremum of an empty family and returns zero. Thus, at every horizon and base state,

The final two public theorems state those functions exactly:

• normObservable_eq_zero_of_isEmpty; and
• logNormObservable_eq_bot_of_isEmpty.

The second theorem reuses the exact bottom criterion after proving that the unique empty matrix equals zero.

There is no contradiction between “time-zero value is the identity” and “time-zero log norm is bottom” in empty dimension. The unique identity is also the zero matrix, and its empty row-sum norm is zero.

The complete fourteen-declaration map

All declarations share a measurable base space \(\Omega\), a finite matrix index type \(\iota\) with decidable equality, an arbitrary measure \(\mu\), and a bundled complex DiscreteMatrixCocycle. The table lists every additional assumption and exact result.

The declaration order is deliberate. The row-sum formula comes before the measurability proof that consumes it. The exact bottom criterion comes before the empty-dimension log theorem that reuses it.

The proof architecture

The module is short because each theorem consumes a precise upstream law.

Norm layer

• C.value_zero and Mathlib’s norm-one instance prove time zero in nonempty dimension.
• C.value_one proves the one-step generator identity.
• C.value_add plus norm_mul_le proves the split bound.
• C.measurable_value, measurable entries, finite sums, finite maxima, and Matrix.linfty_opNorm_def prove measurability.

Extended-log layer

• ENNReal.log_eq_bot_iff and norm zero equivalence prove the exact collapse criterion.
• ENNReal.log_one proves the positive-dimensional zero-time law.
• C.value_one proves the generator identity.
• measurable embedding plus Measurable.ennreal_log proves measurability.
• cocycle splitting, nnnorm_mul_le, logarithm monotonicity, and ENNReal.log_mul_add prove subadditivity.

Empty-dimension layer

Function extensionality and empty elimination show that every matrix value is the zero matrix. The norm theorem then simplifies directly, and the log theorem uses the exact bottom criterion.

No proof needs a matrix inverse, determinant, eigenvalue, singular value, probability instance, integral, or limit.

Assumption and type ledger

The word “observable” means a measurable function of the base state at a fixed horizon. It does not mean a physical measurement postulate or an expectation.

Why this layer matters

Matrix cocycle growth is the bridge between several future tracks:

• derivatives of nonlinear iterates can form matrix cocycles after a checked chain-rule construction;
• products of random matrices become cocycles when driven by a common base dynamics;
• finite norm bounds are raw material for stability and contraction criteria; and
• integrable log norms are among the hypotheses used in multiplicative ergodic theory.

But a bridge must begin with exact endpoints. Defining a real logarithm at zero without care would corrupt every later statement about collapse or asymptotic growth. Hiding the matrix norm would make constants and geometry ambiguous. Assuming measurability without connecting it to the project-owned matrix structure would leave a formal gap.

RMT-14 closes those finite-time seams and stops.

Common wrong turns

Calling the selected norm Frobenius

The active norm is the largest absolute row sum. Frobenius geometry sums the squares of every entry and then takes a square root. Those norms are not equal and support different proof interfaces.

Assuming norm notation is globally unambiguous

The meaning of ‖B‖ depends on open scoped Matrix.Norms.Operator. The explicit row-sum theorem is the audit trail.

Declaring measurability by continuity alone

The project’s matrix measurable structure is entrywise. The module proves measurability from measurable entries, finite sums, and finite suprema before using the row-sum identity.

Applying Real.log to the norm

Its total value at zero is zero, which would confuse exact collapse with norm one. The checked observable uses ENNReal.log into EReal.

Treating bottom as an error

Bottom is the exact intended value if and only if the cocycle matrix is zero. It is part of the mathematical codomain.

Assuming nonzero blocks have a nonzero product

Matrices can be zero divisors. The extended-real inequality remains valid when the full product collapses even though neither block is zero.

Replacing subadditivity with equality

The logarithm turns a product of norm bounds into a sum, but the matrix norm is only submultiplicative. Slack or complete collapse can occur.

Adding an unnecessary nonempty-dimension assumption

Only the familiar time-zero normalizations need an inhabited coordinate type. Definitions, measurability, inequalities, and explicit empty-dimension laws do not.

Reading measurability as integrability

A measurable extended-real function can fail every integrability condition needed later. The module evaluates no integral.

Reading subadditivity as Kingman’s theorem

A finite pointwise inequality is one input to subadditive ergodic theory. It is not a probability space, an integrability theorem, an ergodicity theorem, or a limit.

Reading a log-norm observable as a Lyapunov exponent

A Lyapunov exponent is asymptotic growth after a normalization and under additional hypotheses. \(L_k(\omega)\) is a finite-horizon value.

Assuming a nonlinear Jacobian origin

The generator is an arbitrary measurable complex matrix map. No nonlinear map, derivative, chain rule, or tangent-space identification appears here.

Exercises from trailhead to summit

Trailhead

1. Compute the largest absolute row sum of three different two-by-two matrices.
2. Verify both running horizon-two products entry by entry.
3. Give a nonidentity matrix with maximum absolute row-sum norm one.
4. Explain in words why one output coordinate corresponds to one matrix row.
5. Compare the row-sum norm and Frobenius norm of the identity in dimensions one, two, and three.
6. Build the four-row norm, positive-log, and extended-log table without looking back at the figure.

Mid-mountain

7. Derive matrix-vector control from the triangle inequality.
8. Derive the cocycle norm split from C.value_add and norm_mul_le.
9. Reconstruct the measurable-row-sum proof for a two-row matrix.
10. Generalize that proof by induction over an arbitrary finite set of rows.
11. Track the types in the composition from a real norm through ENNReal.ofReal to ENNReal.log.
12. Prove on paper that bottom characterizes a zero matrix.
13. Find two nonzero matrices with zero product and evaluate both sides of the extended log-norm inequality.
14. Explain why the norm split and log split need no probability assumption.

Summit

15. Audit every theorem in the fourteen-declaration map against its exact assumptions.
16. Prove that the empty square matrix is simultaneously zero and identity.
17. Derive the constant-zero norm and constant-bottom log-norm functions in empty dimension.
18. State a candidate integrability hypothesis for the one-step positive log norm and explain why it is absent here.
19. Compare finite subadditivity with the hypotheses and conclusion of Kingman’s subadditive ergodic theorem.
20. State the additional probability, invertibility, and integrability choices needed before an Oseledets theorem could even be formulated.
21. Design a separate theorem connecting the cocycle generator to a Jacobian along a nonlinear orbit. List the differentiability and chain-rule prerequisites.
22. Normalize both running logarithm ledgers at horizon two, then explain why the target module proves neither a normalized-process theorem nor a limit.

Reproduce the chapter

The bounded Std worksheet above is a standalone tutorial for an ordinary macOS or Linux host. The exact target and comparison modules import Mathlib and are full project checks. From the repository root, run:

cd formalization
lake env lean NonlinearDynamics/Random/RandomCocycles/NormObservables.lean
lake env lean NonlinearDynamics/Random/RandomCocycles/LogPlusIntegrability.lean
lake env lean NonlinearDynamics/Random/RandomCocycles/SubadditiveKingman.lean

These commands may require substantial disk space and memory. Passing the technical gates would still leave human mathematical, source, accessibility, scientific-integrity, and editorial review pending.

Summit: what has and has not been proved

The summit is an analytic interface, not an asymptotic theorem. Every finite cocycle value now has a checked measurable size, every exact collapse remains visible as bottom, and every time split obeys a zero-safe additive upper bound.

Where to continue

Finite-Horizon Log-Positive Cocycle Integrability is the immediate successor. It defines the real nonnegative log-positive integrability envelope , majorizes every finite horizon by shifted one-step terms, and propagates an explicit generator integrability assumption through that finite sum. It does not make this chapter’s contraction-sensitive extended log norm integrable and does not prove a Lyapunov exponent.

The extended log-norm observable glossary entry is the compact guide to the type ladder, bottom convention, and dimension boundary.

Generator-Presented One-Sided Discrete Matrix Cocycles develops the exact base-orbit and later-block-left algebra consumed here. Ordered Finite Matrix Products and Operator-Norm Growth develops the deterministic product and maximum-row-sum norm layer below the cocycle.

The next asymptotic layer must state an integrability policy before normalizing by time or invoking a subadditive or multiplicative ergodic theorem. It must also decide whether the base measure is probabilistic and whether ergodicity, invertibility, or one-sided time is required. None of those choices is made retroactively here.

References

Mathlib contributors. Norms on finite matrices, Mathlib 4 documentation. This official source defines the maximum absolute row-sum norm, proves its matrix-product and matrix-vector bounds, and identifies it with the operator norm on finite supremum-norm function spaces.

Mathlib contributors. Extended nonnegative-real logarithm, Mathlib 4 documentation. This official source defines ENNReal.log, including its zero-to-bottom convention, strict monotonicity, exact endpoint criteria, and unconditional product-to-sum law.

Mathlib contributors. Extended logarithm and exponential, Mathlib 4 documentation. This official source packages the logarithm as an order isomorphism and homeomorphism and proves that it is measurable.

Mathlib contributors. Positive part of the real logarithm, Mathlib 4 documentation. This official source defines Real.posLog as the maximum of zero and the real logarithm, proves its zero policy, nonnegativity, continuity, and product upper bound.

Mathlib contributors. Extended-real inversion and division, Mathlib 4 documentation. This official source records that bottom divided by a positive finite extended real remains bottom. The target module itself defines no normalized extended observable.

Roger A. Horn and Charles R. Johnson. Matrix Analysis, second edition, Cambridge University Press, 2013, International Standard Book Number (ISBN) 978-0-521-54823-6. Chapter 5 develops vector norms, induced matrix norms, and submultiplicative product estimates.

J. F. C. Kingman. The ergodic theory of subadditive stochastic processes, Journal of the Royal Statistical Society, Series B 30(3), 1968, 499-510. This primary source establishes a subadditive ergodic theorem under additional measure-theoretic hypotheses. RMT-14 supplies only the finite pointwise subadditivity input.

V. I. Oseledets. A multiplicative ergodic theorem. Characteristic Ljapunov exponents of dynamical systems, Transactions of the Moscow Mathematical Society 19 (1968), 197-231. This primary source supplies the historical long-time destination. The present module proves none of its integrability, limit, exponent, or splitting conclusions.

Ludwig Arnold. Random Dynamical Systems, Springer Monographs in Mathematics, 1998. This develops cocycles and multiplicative ergodic theory over metric dynamical systems. Its usual probability, invertibility, and asymptotic structures are context, not claims of this finite-time module.

The exact upstream Lean source audited for this chapter is Mathlib commit 81a5d257, the revision pinned by formalization/lake-manifest.json.