Extended log-norm observable

An extended log-norm observable answers a concrete question:

After \(k\) steps, how large is the cocycle matrix at the base state \(\omega\), measured on a logarithmic scale that still recognizes exact collapse?

For a one-sided discrete matrix cocycle \(C\), the project defines

and then

The first observable \(N_k\) is a finite nonnegative real number. The second observable \(L_k\) takes values on the extended real line. It can therefore say all four of the following without ambiguity:

• \(\bot=-\infty\): exact matrix collapse;
• a finite negative number: strict norm contraction;
• \(0\): norm exactly one; and
• a finite positive number: norm expansion.

That four-way distinction is the main idea. The logarithm also converts the multiplicative estimate for cocycle norms into an additive estimate, which is the shape later ergodic theorems expect.

Start with four real matrices

Consider four \(2\times2\) diagonal matrices:

The project uses the maximum absolute row-sum norm

For a diagonal matrix, each row total equals the magnitude of its diagonal entry. We therefore obtain

The two rightmost columns are deliberately different observables.

• The signed extended log preserves contraction and gives zero a genuine negative-infinity endpoint.
• The real log-positive observable \(\log^+ r=\max\{0,\log r\}\) keeps only expansion above one. It sends the first three rows of the table to zero.

Work through each row

Zero matrix: collapse is bottom

For \(A_0\), both row sums vanish, so \(\lVert A_0\rVert_\infty=0\). The extended logarithm uses

This is not an error, missing value, or failed proof. It is the intended record of exact collapse. The project proves the sharp statement

The real log-positive envelope gives \(\log^+0=0\). That is also intentional: the envelope does not record collapse; it isolates expansion above one for an integrability argument.

Norm one half: contraction is finite and negative

For \(A_{1/2}\), the row totals are \(1/2\) and \(0\), hence

Because the norm is positive and finite, the extended logarithm agrees with the ordinary logarithm:

But \(\log^+(1/2)=0\). This is the cleanest example of why the two observables must not be used as synonyms: one records contraction and the other discards it.

Norm one: zero means neutral size

For the identity matrix, both row totals are one. Thus

Here zero means norm one, not zero matrix. Many nonidentity matrices also have operator norm one, so a zero log norm does not identify the matrix.

Norm \(e^2\): both observables retain expansion

For \(A_{e^2}\), the largest row total is \(e^2\). Therefore

Above one, the ordinary log is nonnegative, so taking its positive part changes nothing.

Four logarithmic conventions that look deceptively similar

At a positive real input, all relevant signed logarithms agree. The zero input is where notation must be read carefully.

Mathlib defines

Because Mathlib also has \(\operatorname{Real.log}0=0\), its log-positive function is continuous at zero and returns zero there. This is useful, but it does not repair the signed information that total real log loses at a zero norm.

Later, under a nonzero or pointwise-invertibility hypothesis and in nonempty matrix dimension, the project can identify the extended log with the coercion of the real signed log. Without such a hypothesis, they differ precisely at zero.

Bottom is not top

Two extended number systems appear in the Lean definition:

The endpoint rules are

The cocycle observable cannot reach the second branch. A finite matrix has a finite real norm, and its extended norm notation ‖A‖ₑ embeds that finite value into ENNReal; it is never ⊤. Therefore logNormObservable can be bottom or a finite real value, but not top.

That distinction prevents a common reading error:

• ⊥ means negative infinity and comes from norm zero;
• ⊤ means positive infinity and would come from an infinite extended input; and
• neither symbol is the real number zero.

Why this is the raw cocycle-growth observable

A one-sided cocycle satisfies the later-block-left split

The induced infinity norm is submultiplicative, so

The extended logarithm is monotone and turns products into sums, including at zero. Hence

This is the raw finite-time growth observable:

• it uses the actual \(k\)-step cocycle value;
• it is not divided by \(k\);
• it has not been integrated over the base space;
• it has not been replaced by a probability distribution; and
• no limit as \(k\to\infty\) has been taken.

The inequality can be strict. Matrix multiplication can produce cancellation, and two nonzero matrices can even have zero product. In that case the left side is bottom while the two terms on the right remain finite.

The log-positive envelope also satisfies a subadditive bound,

but it serves a different purpose: it is a nonnegative upper-tail quantity that can be integrated once a genuine integrability hypothesis is supplied.

Measurability: build it from visible pieces

An observable must be measurable before measure-theoretic tools can use it. The project proves this from the finite row-sum formula rather than treating matrix norm notation as a black box.

For fixed \(k\):

1. every coordinate map \(\omega\mapsto C(k,\omega)_{ij}\) is measurable;
2. complex magnitude preserves measurability;
3. a finite sum of measurable column terms is measurable;
4. a finite maximum over the rows is measurable;
5. the row-sum theorem identifies that maximum with \(N_k\); and
6. composition with measurable ENNReal.log gives measurable \(L_k\).

The log-positive observable is measurable by composing \(N_k\) with the continuous real function Real.posLog.

Measurability is not integrability. A measurable growth observable can still have an infinite integral, a nonintegrable positive tail, or bottom on a set of positive measure. The later finite-horizon integrability module therefore introduces an explicit hypothesis on the one-step log-positive observable; it does not derive integrability from measurability or measure preservation.

Time zero and the empty-coordinate edge case

At time zero, a cocycle value is the identity. If the finite coordinate type \(\iota\) is nonempty, the familiar normalization holds:

The hypothesis Nonempty ι matters. If \(\iota\) is empty, there are no rows, so the supremum of the row totals is zero. The unique empty square matrix is both the zero matrix and the identity matrix. Consequently,

for every \(k\) and \(\omega\) in that edge case. The real log-positive observable remains zero. The definitions, measurability results, and split inequalities all allow empty dimension; only the usual identity-norm normalization needs positive dimension.

A non-tight two-block calculation

Let an earlier block be

and a shifted later block be

Their maximum absolute row sums are

Because the later block acts on the left,

Thus

and, since all three norms are positive,

The estimate is deliberately a budget, not an equality. If \(D\) were zero, then \(DB=0\), both corresponding extended log norms would be bottom, and no special nonzero exception would be required.

In Lean: form the signed observable

C.logNormObservable k ω

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

#check C.logNormObservable k ω

In Lean: recognize exact collapse

C.logNormObservable_eq_bot_iff k ω

#check C.logNormObservable_eq_bot_iff k ω

In Lean: form the real log-positive envelope

C.logPlusNormObservable k ω

def logPlusNormObservable
    (C : DiscreteMatrixCocycle (ι := ι) μ) (k : ℕ) : Ω → ℝ :=
  fun ω ↦ log⁺ (C.normObservable k ω)

#check Real.posLog_apply
#check C.logPlusNormObservable k ω

In Lean: state measurability and the cocycle split

C.measurable_logNormObservable k; C.measurable_logPlusNormObservable k

#check C.measurable_logNormObservable k
#check C.measurable_logPlusNormObservable k

C.logNormObservable_add_le m k ω

#check C.logNormObservable_add_le m k ω
#check C.logPlusNormObservable_add_le m k ω

Exact source excerpts

Full project check. This uses the repository’s pinned Lean and Mathlib dependencies and may require substantial disk space and memory. The zero-faithful observable, collapse theorem, and measurability proof are in NormObservables.lean:

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

@[simp] theorem logNormObservable_eq_bot_iff
    (C : DiscreteMatrixCocycle (ι := ι) μ) (k : ℕ) (ω : Ω) :
    C.logNormObservable k ω = ⊥ ↔ C.value k ω = 0 := by
  simp [logNormObservable]

theorem measurable_logNormObservable
    (C : DiscreteMatrixCocycle (ι := ι) μ) (k : ℕ) :
    Measurable (C.logNormObservable k) := by
  have hnorm : Measurable (C.normObservable k) := C.measurable_normObservable k
  unfold logNormObservable
  unfold normObservable at hnorm
  simpa only [ofReal_norm] using hnorm.ennreal_ofReal.ennreal_log

The subadditive result first uses matrix-norm submultiplicativity and then Mathlib’s unconditional product rule ENNReal.log_mul_add:

theorem logNormObservable_add_le
    (C : DiscreteMatrixCocycle (ι := ι) μ) (m k : ℕ) (ω : Ω) :
    C.logNormObservable (m + k) ω ≤
      C.logNormObservable k (C.base^[m] ω) + C.logNormObservable m ω := by
  rw [logNormObservable, C.value_add]
  calc
    ENNReal.log ‖C.value k (C.base^[m] ω) * C.value m ω‖ₑ ≤
        ENNReal.log (‖C.value k (C.base^[m] ω)‖ₑ * ‖C.value m ω‖ₑ) := by
      apply ENNReal.log_monotone
      simpa only [enorm_eq_nnnorm, ← ENNReal.coe_mul, ENNReal.coe_le_coe] using
        (nnnorm_mul_le (C.value k (C.base^[m] ω)) (C.value m ω))
    _ = ENNReal.log ‖C.value k (C.base^[m] ω)‖ₑ +
        ENNReal.log ‖C.value m ω‖ₑ := ENNReal.log_mul_add

Full project check. This uses the repository’s pinned Lean and Mathlib dependencies and may require substantial disk space and memory. The nonnegative envelope is defined separately in LogPlusIntegrability.lean:

def logPlusNormObservable
    (C : DiscreteMatrixCocycle (ι := ι) μ) (k : ℕ) : Ω → ℝ :=
  fun ω ↦ log⁺ (C.normObservable k ω)

theorem measurable_logPlusNormObservable
    (C : DiscreteMatrixCocycle (ι := ι) μ) (k : ℕ) :
    Measurable (C.logPlusNormObservable k) :=
  Real.continuous_posLog.measurable.comp (C.measurable_normObservable k)

These excerpts establish definitions and finite-horizon infrastructure. They do not establish an asymptotic exponent.

Standalone tutorial: symbolic worksheet

Standalone tutorial. Transcendental real logarithms belong to Mathlib, so this dependency-light worksheet uses an exact symbolic four-case ledger. It checks the branch logic with only Std; it does not implement EReal, matrix norms, or analytic logarithms.

Save it as LogNormFourCasesScratch.lean:

import Std

inductive NormCase where
  | zero
  | half
  | one
  | expTwo
deriving Repr, BEq

inductive ExtendedLogValue where
  | bottom
  | negLogTwo
  | zero
  | two
deriving Repr, BEq

def extendedLogTable : NormCase → ExtendedLogValue
  | .zero => .bottom
  | .half => .negLogTwo
  | .one => .zero
  | .expTwo => .two

def logPlusTable : NormCase → Nat
  | .zero => 0
  | .half => 0
  | .one => 0
  | .expTwo => 2

def cases : List NormCase :=
  [.zero, .half, .one, .expTwo]

#eval cases.map fun c => (c, extendedLogTable c, logPlusTable c)
#eval extendedLogTable .zero == .bottom
#eval extendedLogTable .half == .negLogTwo
#eval logPlusTable .half == 0
#eval logPlusTable .expTwo == 2

Run it with the repository’s pinned Lean version but outside the Mathlib project:

elan run leanprover/lean4:v4.32.0 lean LogNormFourCasesScratch.lean

The first output should list (zero, bottom, 0), (half, negLogTwo, 0), (one, zero, 0), and (expTwo, two, 2). The four Boolean checks should all print true.

This worksheet is intentionally a teaching surrogate. The exact analytic facts are the pinned Mathlib and project declarations checked next.

Try the exact declarations in the project

import NonlinearDynamics.Random.RandomCocycles.LogPlusIntegrability

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

#check ENNReal.log_zero
#check ENNReal.log_one
#check ENNReal.log_top
#check ENNReal.log_mul_add
#check ENNReal.log_eq_bot_iff
#check Real.posLog_apply
#check Real.posLog_zero
#check Real.posLog_one
#check Real.continuous_posLog
#check DiscreteMatrixCocycle.normObservable
#check DiscreteMatrixCocycle.normObservable_eq_rowSumSup
#check DiscreteMatrixCocycle.measurable_normObservable
#check 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.logNormObservable_eq_bot_of_isEmpty
#check DiscreteMatrixCocycle.logPlusNormObservable
#check DiscreteMatrixCocycle.logPlusNormObservable_nonneg
#check DiscreteMatrixCocycle.logPlusNormObservable_zero
#check DiscreteMatrixCocycle.logPlusNormObservable_one
#check DiscreteMatrixCocycle.measurable_logPlusNormObservable
#check DiscreteMatrixCocycle.logPlusNormObservable_add_le
#check DiscreteMatrixCocycle.logPlusNormObservable_eq_zero_of_isEmpty

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

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

What has and has not been formalized here

The checked finite-time layer provides:

• the maximum-row-sum norm observable;
• its exact row-sum formula;
• a zero-faithful signed extended log observable;
• bottom exactly at a zero cocycle matrix;
• a real-valued nonnegative log-positive envelope;
• measurability of both logarithmic observables;
• subadditivity across every finite cocycle split;
• the positive-dimensional time-zero normalization; and
• explicit empty-dimensional behavior.

It does not yet provide:

• integrability merely from measurability;
• a probability assumption on the base measure;
• normalized growth \(k^{-1}L_k\);
• almost-everywhere or \(L^1\) convergence;
• a Lyapunov exponent or Lyapunov spectrum;
• an Oseledets invariant splitting;
• invertibility or negative-time dynamics;
• a lower singular-value estimate;
• a distribution of the observable; or
• an identification of the generator with a nonlinear Jacobian.

It is also not a matrix logarithm. Nor is it the distinct logarithmic norm or matrix measure used in some ODE stability arguments. Here the order is: take a scalar operator norm first, then apply a scalar logarithm.

Exercises

1. Compute both logarithmic observables for \(\operatorname{diag}(1/4,0)\). Which information does \(\log^+\) discard?
2. Compute both observables for \(2I\). Why is the infinity norm \(2\), not \(4\)?
3. Explain in one sentence why ⊥ cannot mean neutral growth.
4. Give two nonzero \(2\times2\) matrices whose product is zero. What are the three terms in the signed subadditive inequality?
5. Starting from measurable entries, reconstruct the six-step measurability argument above.
6. Why can this cocycle observable never equal ⊤ even though ENNReal.log ⊤ = ⊤?
7. Explain why Real.log 0 = 0 is convenient for total real functions but unsuitable for recording exact matrix collapse.
8. List the additional assumptions needed before a subadditive ergodic theorem could turn finite-time growth into an almost-sure asymptotic rate.

Where to continue

Finite-Horizon Log-Positive Cocycle Integrability develops the nonnegative envelope, its orbit-sum majorant, and the explicit one-step integrability hypothesis that propagates to finite horizons.

The Forward-and-Inverse Tail Sandwich for Finite-Time Real Log Norms returns to signed real logarithms. It explains exactly when a nonzero cocycle value lets the extended log be read as an ordinary real log and why inverse tails are needed to control contraction.

Finite-Time Norm and Extended-Log-Norm Observables for Matrix Cocycles derives the complete formal interface: row-sum measurability, zero-safe subadditivity, time-zero normalization, and the empty-dimension ledger.

The one-sided discrete matrix cocycle entry supplies the base orbit and later-block-left product law. The log-positive integrability envelope entry focuses on why contraction is deliberately removed.

References

Mathlib contributors. Norms on finite matrices, Mathlib 4 documentation. This official source defines the maximum absolute row-sum matrix norm and proves its product inequality and operator-norm interpretation.

Mathlib contributors. Extended nonnegative-real logarithm, Mathlib 4 documentation. This official source defines ENNReal.log, including log 0 = ⊥, log ⊤ = ⊤, strict monotonicity, and the unconditional product-to-sum identity.

Mathlib contributors. Extended logarithm and exponential, Mathlib 4 documentation. This official source packages the logarithm as an order isomorphism and homeomorphism and proves its measurability.

Mathlib contributors. Positive part of the real logarithm, Mathlib 4 documentation. This official source defines Real.posLog, proves continuity and nonnegativity, and develops its product estimate.

Roger A. Horn and Charles R. Johnson. Matrix Analysis, second edition, Cambridge University Press, 2013, ISBN 978-0-521-54823-6. Chapter 5 develops induced matrix norms and submultiplicativity. The project selects the maximum absolute row-sum convention.

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 supplies a later asymptotic destination. The present page does not claim Kingman’s hypotheses or conclusions.

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