Real Log-Norm Integrability from Forward and Inverse Tails in Lean

For reusable terminology, see one-sided discrete matrix cocycles , the extended log-norm observable , the log-positive integrability envelope , the integrated log-positive growth rate , and integrable generator log tails . The companion textbook chapter is The Forward-and-Inverse Tail Sandwich for Finite-Time Real Log Norms.

Orientation: one main route and one side route

RMT-33 proves almost-everywhere convergence of the normalized nonnegative observable

That theorem is deliberately expansion-only. If a scalar cocycle contracts by one half at each step, then \(P_n=0\) at every horizon even though the signed logarithmic growth is negative. RMT-34 begins recovering that missing signed information.

There are two routes through the module.

1. The main finite-time route assumes pointwise unit generators and integrable forward and inverse one-step log-positive tails. It produces an integrable real-valued subadditive-process candidate.
2. The side route assumes the existing forward-tail package, an ergodic probability base, and a strictly positive integrated rate. Positivity eventually removes the clipping in log⁺, so RMT-33 already supplies the real-log limit.

The immediate predecessor is Log-Positive Kingman Convergence from Rational Lower Deviations in Lean.

Prior work, this milestone’s contribution, and exact nonclaims

Historical placement. Furstenberg and Kesten’s 1960 paper is a foundational source for products of random matrices (Furstenberg and Kesten 1960). Kingman’s 1968 paper developed the general ergodic theory of subadditive stochastic processes (Kingman 1968). Oseledets’ 1968 paper is the original multiplicative ergodic theorem source (Oseledets 1968). Ruelle’s 1979 paper is particularly useful for separating a forward matrix-product theorem under a forward positive-log moment from an invertible theorem using both forward and inverse moments (Ruelle 1979). These sources motivate interfaces. They do not enlarge the checked Lean result.

Checked contribution. The module:

• defines and measures a total real logarithmic norm observable;
• propagates pointwise generator units to every finite cocycle value;
• bridges the earlier zero-faithful extended log to the real log under the exact nonempty-dimensional gate;
• proves signed shifted subadditivity under pointwise units;
• proves global measurability of Mathlib’s total matrix inverse through determinant and adjugate formulas;
• builds finite inverse-value and forward-orbit inverse-generator envelopes;
• proves a pointwise lower rail using only pointwise units;
• packages pointwise units and the two one-step integrability assumptions;
• proves finite-horizon real-log integrability by two-sided domination;
• packages the signed real-log family as an integrable subadditive candidate;
• compiles an infinite-volume inverse-tail separation and a geometric probability-space example showing that forward log-positive integrability does not imply inverse-tail or one-step signed real-log integrability; and
• proves the strictly positive-rate eventual-agreement endpoint.

Not claimed. The module proves no general almost-everywhere signed real-log limit, no signed Kingman theorem for arbitrary real subadditive processes, no convergence in \(L^1\), probability, or uniformly, no limit-integral interchange, no concentration inequality, and no convergence rate. It constructs no negative-time process and no same-base inverse cocycle. It proves no equality between the inverse orbit sum and the inverse of the finite product, no inverse-growth identity, no singular-value limit, no Lyapunov spectrum, no invariant filtration or splitting, and no Oseledets theorem. It formalizes no derivative cocycle, tangent bundle, stable manifold, nonlinear stability theorem, bifurcation, turbulence claim, or physical-chaos conclusion. It assumes no independence or mixing.

Three logarithmic observables and their information boundaries

For a nonnegative norm \(r\), the repository now has three relevant outputs:

The extended log is zero-faithful at collapse because its codomain contains bottom. The real log records finite contraction but totalizes collapse to zero. The positive log is continuous and nonnegative but deliberately clips both collapse and contraction.

The first four compiled probes make the scalar separation executable: Real.log 0 = 0, log⁺ (1 / 2) = 0, Real.log (1 / 2) < 0, and 0 < log⁺ ((1 / 2)⁻¹).

Pointwise units propagate, but time remains one-sided

The definition

def IsPointwiseInvertible
    (C : DiscreteMatrixCocycle (ι := ι) μ) : Prop :=
  ∀ ω, IsUnit (C.generator ω)

is pointwise. It is not an almost-everywhere representative condition. It is also algebraic rather than quantitative: it does not provide a uniform bound on inverse norms or condition numbers.

The successor recurrence is

The identity matrix is a unit at time zero. If the current finite product is a unit and the newest generator is a unit, their product is a unit. Induction therefore proves IsPointwiseInvertible.value_isUnit.

The distinction becomes decisive when products are inverted. Mathlib proves

Thus a newest-factor-left forward product acquires the reverse factor order under inversion. The noncommuting-shear counterexample exhibits two products for which the orders differ.

The nonempty bridge is semantic

Under pointwise units and [Nonempty ι], every finite value is nonzero, its selected norm is positive, and the earlier extended logarithm equals the coercion of the real logarithm:

The nonempty premise cannot be erased. For matrices indexed by Empty, the matrix type is subsingleton. Its zero matrix equals its identity matrix, so zero is algebraically a unit. The selected row-sup norm is nevertheless zero. The extended log is bottom while the total real log is zero.

The module consequently proves three separate simplification theorems:

• the real-log observable is identically zero for an empty index;
• it is zero at horizon zero in every finite dimension; and
• at horizon one it is the real logarithm of the generator norm.

Signed subadditivity needs nonvanishing

The cocycle law and norm submultiplicativity give

Taking an ordinary logarithm is legitimate only when the relevant norms are positive. Pointwise units provide three nonzero facts in the nonempty branch: the later block, the earlier block, and their product. Real.log_le_log handles the norm inequality and Real.log_mul splits the product. The empty branch is an all-zero calculation.

The pointwise theorem is

The unit hypothesis is not merely proof convenience. Let

Both selected norms are one half but \(AB=0\). Total real-log subadditivity would read

which is false. The module compiles exactly this counterexample.

A measurable total inverse from entries upward

The pinned library does not provide the matrix measurability shortcut needed by this module. RMT-34 therefore proves the route explicitly.

1. A determinant is a finite sum over permutations of finite products of measurable entries.
2. Updating one row by a constant row preserves entrywise measurability.
3. Every adjugate entry is a determinant of a row-updated matrix.
4. Mathlib’s total nonsingular inverse satisfies \(A^{-1}=\det(A)^{-1}\operatorname{adj}(A)\).
5. The selected matrix norm is a finite supremum of finite row sums of entry norms.
6. Real.posLog is continuous, so it composes measurably with that pipeline.

This gives unconditional measurability of both

and

On singular inputs these functions are still measurable, but the total inverse is zero and the positive log is zero. The word contraction is warranted only under pointwise invertibility.

Reverse order and the finite inverse orbit envelope

Define

and

The sum has the expected zero and successor equations. The key finite bound is

The proof is an induction over the newest-factor-left product. It first uses Matrix.mul_inv_rev, then matrix norm submultiplicativity, monotonicity of positive log on nonnegative inputs, and Real.posLog_mul.

The inequality is unconditional because Mathlib’s inverse and positive log are total. It becomes a valid lower-tail majorant only when the finite product is a unit. On a singular product, \(Q_k\) may be zero and contain no record of collapse.

Three separately stored fields in the tail package

The structure

structure HasIntegrableGeneratorLogTails
    (C : DiscreteMatrixCocycle (ι := ι) μ) : Prop where
  isPointwiseInvertible : C.IsPointwiseInvertible
  hasIntegrableGeneratorLogPlus : C.HasIntegrableGeneratorLogPlus
  integrable_inverseGeneratorLogPlus :
    Integrable C.inverseGeneratorLogPlusNormObservable μ

contains three logically distinct obligations.

Measure preservation transports the inverse-generator integrability through every nonnegative base iterate. A finite sum of those pullbacks is integrable, so every \(J_k\) is integrable. Base invertibility is not used.

The two-rail sandwich

For an invertible finite matrix \(A\) in nonempty dimension,

Taking logarithms and using

gives

Combining this one-value inequality with \(Q_k\le J_k\) yields the public lower rail. The empty-dimensional branch is separately zero. The upper rail is unconditional because \(x\le\max(0,x)\):

Mathlib’s integrable_of_le_of_le requires an almost-everywhere strongly measurable middle function, almost-everywhere lower and upper inequalities, and integrability of both rails. RMT-34 supplies stronger pointwise inequalities and unconditional ordinary measurability, then packages the result as integrable_realLogNormObservable.

The signed candidate is infrastructure, not convergence

The final main-route declaration is

theorem HasIntegrableGeneratorLogTails.isIntegrableSubadditiveProcessCandidate
    (hC : C.HasIntegrableGeneratorLogTails) :
    IsIntegrableSubadditiveProcessCandidate C.base μ
      C.realLogNormObservable

Its two fields are exactly the finite-horizon integrability theorem and the pointwise-unit subadditivity theorem. It is the interface a future signed subadditive convergence argument can consume.

It is not itself a convergence theorem. In particular, this module does not define an integrated signed Fekete rate, repeat the lower-deviation assembly for a general signed process, or identify an almost-everywhere signed limit.

Forward-tail integrability does not force inverse-tail integrability

The infinite-Lebesgue construction gives the simplest separation. A constant contraction by one half has a zero forward positive-log envelope and a strictly positive inverse positive-log envelope. The zero function is integrable on any measure, while a nonzero constant is not integrable over Lebesgue measure on the whole real line.

That example alone would not settle the probability-space boundary because every finite constant is integrable under a probability measure. The module therefore compiles a genuine heavy-tail construction.

Let \(N\) have Mathlib’s geometric distribution with parameter one half, so

On the identity base, take the invertible one-dimensional generator

Then

The absolute inverse and signed tails have expected summands

Their series diverges. The forward positive-log observable is identically zero and integrable. The cocycle is pointwise invertible and the base measure is a genuine probability measure. Thus forward positive-log integrability does not imply either inverse-generator integrability or one-step signed real-log integrability, even in an invertible one-dimensional probability example.

Every component of this example is Lean-checked in the module: the geometric probability instance, matrix norm and inverse formulas, pointwise units, observable identities, nonsummability, and the final five-part anonymous example.

The inverse lower rail can be strict

For

the selected maximum-row-sum norm is one half, while

Consequently

The inverse envelope bounds the strongest finite contraction visible to the selected inverse norm. It does not equal the negative top log norm in this example. No general inverse-exponent interpretation is proved.

Strict positive rate removes clipping eventually

Assume a probability measure, PreErgodic C.base μ, the existing forward generator positive-log integrability package, and

RMT-33 gives

for almost every \(\omega\). For such a sample, the normalized value is eventually greater than \(\gamma_+(C)/2\gt0\). At horizons \(n\ge1\), positivity of the quotient forces \(P_n(\omega)\gt0\). Since

this forces \(R_n\gt0\) and \(P_n=R_n\). The normalized sequences are eventually equal, so they have the same limit.

A singular matrix can still have expanding top norm. The compiled matrix diag(2,0) is not a unit and has norm greater than one. This is the substantive reason not to impose invertibility on the positive endpoint. Empty dimension is different: the module proves its integrated positive-log rate is exactly zero, so the strict positivity premise cannot be supplied.

Public declaration surface in exact source order

The following twenty-eight headings cover every source-level public declaration command. The three structure fields are expanded separately under declaration 20.

1. realLogNormObservable

This definition is the total real logarithm of the selected finite-time matrix norm. Its codomain is ℝ, so it is convenient for ordinary Bochner integrability and the generic real subadditive-process API. The definition alone carries no nonvanishing or integrability certificate.

2. IsPointwiseInvertible

This proposition says ∀ ω, IsUnit (C.generator ω). It is a pointwise algebraic interface. It is not an almost-everywhere predicate, a representative class, a moment condition, base-map invertibility, or a quantitative inverse bound.

3. IsPointwiseInvertible.value_isUnit

The theorem propagates generator units to C.value k ω for every horizon and base point. The proof follows value_succ: the shifted newest generator unit multiplies the induction hypothesis on the left.

4. IsPointwiseInvertible.logNormObservable_eq_coe_realLogNormObservable

Under [Nonempty ι], the finite value unit is nonzero, its norm is positive, and ENNReal.log_ofReal selects its finite branch. The earlier extended-real observable then equals the coercion of the new real observable. Empty dimension is excluded because examples 5–7 record different empty-dimensional behavior.

5. measurable_realLogNormObservable

The existing norm observable is measurable. Mathlib’s total real log is measurable globally, including at zero, so composition proves this theorem without invertibility.

6. realLogNormObservable_eq_zero_of_isEmpty

With [IsEmpty ι], every matrix entry is eliminated and every cocycle value is the zero matrix. The row-sup norm and total real logarithm are zero. The theorem is a function equality and carries a simp attribute.

7. realLogNormObservable_zero

At horizon zero, the theorem splits empty from nonempty index types. The empty branch calls declaration 6. The nonempty branch uses the identity matrix norm and Real.log_one. The result is the zero function in every finite dimension.

8. realLogNormObservable_one

The one-step cocycle value is the generator, so the observable simplifies to fun ω ↦ Real.log ‖C.generator ω‖. This theorem also has a simp attribute.

9. IsPointwiseInvertible.realLogNormObservable_add_le

This is signed shifted subadditivity. The empty branch is zero. In the nonempty branch, unit propagation supplies nonzero later, earlier, and product values. Those facts justify logarithmic monotonicity and the product logarithm law.

10. inverseGeneratorLogPlusNormObservable

The definition is fun ω ↦ log⁺ ‖(C.generator ω)⁻¹‖. The inverse is Mathlib’s total nonsingular inverse. Under pointwise units it measures the one-step inverse norm. At a singular generator it is zero and carries no quantitative collapse information.

11. measurable_inverseGeneratorLogPlusNormObservable

The private determinant-adjugate and row-sup pipeline makes the total inverse norm measurable. Continuity of positive log finishes the composition. No invertibility hypothesis is required for this totalized function.

12. inverseValueLogPlusNormObservable

This is the corresponding envelope for the inverse of a finite cocycle value: fun ω ↦ log⁺ ‖(C.value k ω)⁻¹‖. It is a genuine inverse-value envelope under pointwise units and an information-free zero on a singular value.

13. inverseValueLogPlusNormObservable_zero

The horizon-zero inverse-value envelope is the zero function in every finite dimension. The proof again treats the empty matrix ring separately.

14. inverseValueLogPlusNormObservable_one

At one step, the finite value is the generator, so the inverse-value envelope equals inverseGeneratorLogPlusNormObservable as a function.

15. measurable_inverseValueLogPlusNormObservable

Measurability of each finite cocycle value is composed with the same total inverse, row-sup norm, and positive-log pipeline used by declaration 11.

16. inverseOrbitLogPlusSum

This definition sums inverse-generator positive-log norms along the forward base orbit over Finset.range k. It does not sample negative time and is not defined as a cocycle value.

17. inverseOrbitLogPlusSum_zero

The finite range at horizon zero is empty, so the orbit sum is the zero function.

18. inverseOrbitLogPlusSum_succ

Finset.sum_range_succ appends the inverse-generator term at C.base^[k] ω. The equation mirrors the chronological order of forward base sampling.

19. inverseValueLogPlusNormObservable_le_inverseOrbitLogPlusSum

Induction reverses the newest-left product under inversion, bounds the norm of the reversed product, applies Real.posLog_mul, and appends the newest orbit term. The theorem is unconditional because both inverse and positive log are total. Pointwise units are needed only for its later lower-tail interpretation.

20. HasIntegrableGeneratorLogTails

The structure packages exactly three fields:

1. isPointwiseInvertible supplies algebraic units;
2. hasIntegrableGeneratorLogPlus supplies the existing integrable forward one-step positive-log envelope; and
3. integrable_inverseGeneratorLogPlus supplies integrability of the inverse one-step positive-log envelope.

The source stores these obligations separately and does not derive one from another. Its checked separation is one directional: the geometric probability construction is a counterexample to the claim that the forward integrability field implies the inverse field, even when pointwise units already hold. No reciprocal nonimplication is claimed.

21. measurable_inverseOrbitLogPlusSum

Every base iterate is measurable because C.base_preserving includes base measurability. Each composed inverse-generator observable is measurable, and a finite sum remains measurable.

22. HasIntegrableGeneratorLogTails.integrable_inverseGeneratorLogPlus_at_base_iterate

Every natural iterate of the base preserves the measure. Mathlib’s MeasurePreserving.integrable_comp_of_integrable transports the inverse generator’s integrability through that iterate. The declaration name states the transported observable explicitly.

23. HasIntegrableGeneratorLogTails.integrable_inverseOrbitLogPlusSum

Declaration 22 proves every summand integrable. integrable_finsetSum closes the finite orbit sum.

24. IsPointwiseInvertible.neg_inverseOrbitLogPlusSum_le_realLogNormObservable

This public lower rail requires only pointwise units, not either integrability field. In nonempty dimension it combines the private one-value lower lemma with declaration 19 after negation. In empty dimension, both functions are proved zero directly.

25. realLogNormObservable_le_logPlusNormObservable

Unfolding positive log reduces the statement to x ≤ max 0 x. It is unconditional and remains true at norm zero.

26. HasIntegrableGeneratorLogTails.integrable_realLogNormObservable

The measurable real-log function lies between the negative inverse orbit sum and the forward positive-log envelope. Declaration 23 makes the lower rail integrable after negation, and the existing RMT-15 theorem makes the upper rail integrable. MeasureTheory.integrable_of_le_of_le certifies the middle.

27. HasIntegrableGeneratorLogTails.isIntegrableSubadditiveProcessCandidate

The candidate’s integrable field is declaration 26. Its add_le field is declaration 9 through hC.isPointwiseInvertible. This theorem establishes the finite-time input interface for later subadditive work and no limiting claim.

28. HasIntegrableGeneratorLogPlus.ae_tendsto_normalizedRealLogNormObservable_of_pos

Under IsProbabilityMeasure μ, PreErgodic C.base μ, the existing forward integrability package, and a strictly positive integrated positive-log rate, RMT-33 supplies almost-everywhere convergence of the normalized clipped observable. Eventual positivity removes the clipping. Tendsto.congr' transfers the limit to the real-log observable. No pointwise units, inverse tail, or nonempty typeclass occurs in the signature. The empty-dimensional premise is impossible by compiled example 8.

Private support surface in exact source order

The module contains thirty-four private source-level commands. One is an unnamed local probability-measure instance. The remaining commands have private names. All are covered here because they carry proof architecture or boundary semantics even though they do not enlarge the public API.

The first five measurability helpers are plausible candidates for a later generic random-matrix utility layer, but keeping them private is appropriate for this milestone. The remaining private items exist to make semantic boundaries compile rather than live only in prose.

Sixteen compiled boundary examples in exact source order

1. Real.log (0 : ℝ) = 0 records totalization.
2. log⁺ (1 / 2 : ℝ) = 0 records contraction clipping.
3. Real.log (1 / 2 : ℝ) < 0 records signed contraction.
4. 0 < log⁺ ((1 / 2 : ℝ)⁻¹) records the scalar inverse tail.
5. The zero matrix on Empty × Empty is a unit.
6. Every empty-dimensional cocycle is pointwise invertible.
7. Empty dimension gives extended log bottom and total real log zero.
8. Empty dimension has integrated positive-log rate zero.
9. Matrix inversion reverses two-factor order.
10. singularExpandingMatrix is not a unit but has norm greater than one.
11. On infinite Lebesgue measure, the zero forward constant is integrable and the positive inverse constant is not.
12. The geometric probability cocycle is pointwise invertible and has integrable forward positive log, but its inverse-generator and one-step signed real-log observables are not integrable.
13. Total real-log subadditivity fails for two singular contractions whose product vanishes.
14. The inverse lower sandwich fails for a singular contraction because total nonsingular inverse returns zero.
15. The two-rate contraction has an explicit inverse and a strict lower-rail gap.
16. Noncommuting shears furnish a counterexample to equality between the same-order and reverse-order products of inverses.

Examples 11 and 12 address different statements. Example 11 illustrates why a finite constant can fail to be integrable on an infinite measure. Example 12 uses a genuinely unbounded tail and closes the probability-space loophole.

Exact complete source-order map

This map is tied to source SHA-256 ac950f8728e5fd003cff3b7a5d0750e5c36060730b3ebadc5b0e1165b54e72ea. If the Lean file changes, regenerate the line map and hash rather than silently retaining stale numbers.

Complete local proof-step ledger

The public declarations are concise because several local proof decisions do substantial work. This ledger keeps those decisions inspectable.

Lean engineering notes

Ordinary measurability is intentionally weaker than semantic fidelity

Real.log and the total matrix inverse are globally defined, so their compositions can be measurable without any unit hypothesis. That is useful for reusable APIs. It does not mean a singular input retains the intended contraction information. The later pointwise-unit theorem supplies that semantic interpretation.

IsUnit is the correct algebraic interface

The proof needs multiplication closure, nonzero values in the nonempty matrix ring, determinant units, and valid inverse multiplication. IsUnit connects to all of these APIs directly. A bare statement that every determinant is nonzero would be more field-specific and less compositional.

The public lower rail is weaker than the integrability package

The lower inequality uses only pointwise units. Its earlier receiver was the three-field tail package, but the proof did not consume either integrability field. The final source exposes the true dependency as IsPointwiseInvertible.neg_inverseOrbitLogPlusSum_le_realLogNormObservable.

The selected norm must remain visible

The project opens Matrix.Norms.Operator, so the norm is the maximum absolute row-sum operator norm. It is not the Frobenius norm or Euclidean spectral norm. The private measurability proof unfolds Matrix.linfty_opNorm_def, and the diagonal probes compute that same norm.

No pseudoinverse appears

Mathlib’s matrix A⁻¹ in this module is the determinant-adjugate nonsingular inverse and is zero when no inverse exists. A Moore-Penrose pseudoinverse would have different singular behavior and is not imported, defined, or used.

The geometric example uses Mathlib’s parameter convention

geometricMeasure p assigns weight \((1-p)^n p\) to natural number \(n\). With \(p=1/2\), the mass is \(2^{-n-1}\). The example chooses tail size \(2^n\) so each weighted absolute contribution is exactly one half. The proof uses the pinned library’s own integrability characterization rather than an informal expectation calculation.

“Two-sided tails” does not mean two-sided time

Both one-step functions are evaluated at the same forward base state. The inverse-generator term measures an inverse matrix, not a past state. All orbit sums still use C.base^[j] for natural \(j\).

Axiom audit

The source prints axioms for eleven representative theorems, in this exact order:

1. IsPointwiseInvertible.value_isUnit
2. IsPointwiseInvertible.logNormObservable_eq_coe_realLogNormObservable
3. measurable_realLogNormObservable
4. IsPointwiseInvertible.realLogNormObservable_add_le
5. measurable_inverseGeneratorLogPlusNormObservable
6. inverseValueLogPlusNormObservable_le_inverseOrbitLogPlusSum
7. HasIntegrableGeneratorLogTails.integrable_inverseOrbitLogPlusSum
8. IsPointwiseInvertible.neg_inverseOrbitLogPlusSum_le_realLogNormObservable
9. HasIntegrableGeneratorLogTails.integrable_realLogNormObservable
10. HasIntegrableGeneratorLogTails.isIntegrableSubadditiveProcessCandidate
11. HasIntegrableGeneratorLogPlus.ae_tendsto_normalizedRealLogNormObservable_of_pos

The warning-fatal compile reports only the standard logical axioms propext, Classical.choice, and Quot.sound. It reports no sorryAx, unsafe declaration, or project-specific axiom. The compiled geometric boundary construction is not included in the print list because it is private support, not part of the public theorem surface.

Reproduce the Lean and teaching artifacts

From the repository root on macOS or Linux:

source "$HOME/.elan/env"
cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomCocycles/RealLogNormIntegrability.lean
lake build NonlinearDynamics.Random.RandomCocycles.RealLogNormIntegrability
cd ..
hugo --source site --panicOnWarning --printPathWarnings

The direct leaf command is the fastest way to inspect theorem and axiom output. The named Lake build verifies module integration. The final command performs a warning-fatal build of the public teaching site.

Regenerate and verify this page’s deterministic card from any working directory:

site/content/development-notebook/2026/07/real-log-norm-integrability-from-forward-and-inverse-tails-in-lean/generate-card.sh
site/content/development-notebook/2026/07/real-log-norm-integrability-from-forward-and-inverse-tails-in-lean/generate-card.sh --verify

Validate the page-owned vector assets and shell script:

xmllint --noout site/content/development-notebook/2026/07/real-log-norm-integrability-from-forward-and-inverse-tails-in-lean/*.svg
shellcheck site/content/development-notebook/2026/07/real-log-norm-integrability-from-forward-and-inverse-tails-in-lean/generate-card.sh
make content-hygiene
make site-check

To inspect the draft interactively, run make blog-serve and open http://127.0.0.1:1333/. The checked source remains the mathematical source of truth.

Exercises with fully worked solutions

These exercises climb from scalar semantics to the finite-time sandwich and then to the exact theorem boundary. Each solution is placed immediately after its question so that the section can also serve as a guided second reading.

Exercise 1. Compare the three observables at collapse

Let the matrix norm be zero. What do the extended log, total real log, and positive log return, and which result still records collapse?

Solution. The extended log returns bottom, the total real log returns zero because Real.log 0 = 0, and the positive log also returns zero. Only the extended log distinguishes exact collapse from unit norm. This is why the new real-valued observable is convenient for integration but cannot carry zero-faithfulness by itself.

Exercise 2. Detect a strict contraction

Evaluate the information carried by the three observables when the norm is one half.

Solution. Both the extended log and total real log contain the negative number \(\log(1/2)\). The positive log is \(\max(0,\log(1/2))=0\). Thus the signed observables detect contraction, while the clipped observable deliberately forgets it.

Exercise 3. Separate neutral scale from expansion

What happens at norm one and at norm two?

Solution. At norm one, all three observables give zero because \(\log 1=0\). At norm two, the ordinary logarithm is positive, so clipping has no effect: the finite extended log, total real log, and positive log all carry the value \(\log 2\), with the extended value embedded in its larger codomain.

Exercise 4. Explain totality versus faithfulness

Why does global measurability of the total real-log observable not prove that it faithfully represents singular contraction?

Solution. Measurability only says inverse images of measurable sets are measurable. Mathlib’s Real.log is a total function and assigns zero at zero, so composition with a measurable norm is measurable without any nonzero premise. Faithfulness is a different semantic property, and it fails because norm zero and norm one both map to zero.

Exercise 5. Separate measurability from integrability

Can a measurable real-valued function fail to be integrable? Give the reason relevant to this module.

Solution. Yes. Integrability additionally requires a finite integral of the norm. In the geometric probability example, the inverse-log observable is measurable and finite at every natural number, but its weighted absolute series has constant terms equal to one half and therefore diverges.

Exercise 6. Propagate generator units

Assume every generator \(A(\omega)\) is a unit. Prove by induction that every finite cocycle value \(C_n(\omega)\) is a unit.

Solution. At time zero, the cocycle value is the identity matrix, which is a unit. For the successor step, the cocycle recurrence is \(C_{n+1}(\omega)=A(T^n\omega)C_n(\omega)\). The first factor is a unit by the pointwise hypothesis and the second by induction, so their product is a unit.

Exercise 7. Compare pointwise and almost-everywhere units

Why is an almost-everywhere invertibility premise not a drop-in replacement for IsPointwiseInvertible in the public pointwise inequalities?

Solution. The target inequalities quantify over every base point, and the induction proving value_isUnit also evaluates the generator at specific forward iterates. An almost-everywhere statement could support an almost-everywhere theorem after null-set bookkeeping, but it does not supply a unit at each requested point. The current interface intentionally avoids that representative-management problem.

Exercise 8. Understand the empty matrix ring

Why can the zero matrix indexed by Empty be a unit?

Solution. There is exactly one function from Empty × Empty to the scalar field, so all matrices of that shape are equal. In particular, zero equals the identity. Since the identity is a unit, the zero matrix is a unit in this degenerate one-element ring.

Exercise 9. Locate the nonempty gate

Why does the extended-log to real-log bridge require [Nonempty ι], while real-log subadditivity has an explicit empty branch?

Solution. In empty dimension, a unit matrix can still have selected norm zero, so the extended log is bottom while Real.log 0 is zero. The bridge is therefore false. Signed subadditivity, however, compares three real zeros in that branch and remains true, so its proof can split on empty versus nonempty instead of excluding the empty case.

Exercise 10. Compute the horizon-zero observable

Show that the total real-log norm observable is zero at horizon zero in every finite dimension.

Solution. The cocycle value at zero is the identity. In nonempty dimension the selected operator norm of the identity is one, hence its real logarithm is zero. In empty dimension the selected norm is zero, but Mathlib’s total real logarithm again returns zero. The two branches agree as a function.

Exercise 11. Diagnose singular subadditivity failure

Let \(A=\operatorname{diag}(1/2,0)\) and \(B=\operatorname{diag}(0,1/2)\). Why does total real-log subadditivity fail?

Solution. The selected norm of each factor is one half, while \(AB=0\). The proposed inequality becomes \(0\le 2\log(1/2)\). Its right side is strictly negative, so the inequality is false. The failure comes exactly from totalizing Real.log 0 to zero.

Exercise 12. Identify the three positivity facts

In the nonempty proof of signed subadditivity, why are nonzero facts needed for the later block, earlier block, and their product?

Solution. The norm inequality is converted through logarithmic monotonicity, which needs positive arguments. The product logarithm law also needs the factor norms to be nonzero. Unit propagation supplies a unit, hence a nonzero matrix and positive norm, for each factor and for the combined cocycle value.

Exercise 13. Expand determinant measurability

Suppose every matrix entry depends measurably on \(\omega\). Why is the determinant measurable?

Solution. The determinant is a finite sum indexed by permutations. Each summand is a sign times a finite product of selected entries. Measurable functions are closed under finite products, scalar multiplication, and finite sums, so the determinant is measurable without any continuity shortcut for the matrix space.

Exercise 14. Handle a constant row update

Why does replacing one row of a measurable matrix-valued function by a fixed row preserve entrywise measurability?

Solution. Fix an output entry. If its row index is the replaced row, the entry is a constant function and therefore measurable. Otherwise it is the corresponding original measurable entry. A decidable case split on equality of the row indices completes the entrywise proof.

Exercise 15. Make the adjugate measurable

How do determinant measurability and row-update measurability combine to prove adjugate measurability?

Solution. Mathlib expresses each adjugate entry as a signed determinant of a matrix obtained through a fixed row replacement. The updated matrix remains entrywise measurable by Exercise 14, and its determinant is measurable by Exercise 13. Multiplication by the fixed sign preserves measurability.

Exercise 16. Explain total inverse measurability

Use the determinant-adjugate formula to explain why the nonsingular inverse is measurable even at singular matrices.

Solution. Mathlib defines the total inverse as the determinant reciprocal times the adjugate. The determinant and adjugate are measurable, scalar reciprocal is measurable as a total field operation, and scalar-matrix multiplication is entrywise measurable. At a singular matrix this definition returns zero, so no partial-domain extension is needed.

Exercise 17. Unfold the selected matrix norm

Why is the row-sup operator norm measurable for an entrywise measurable finite matrix?

Solution. For each row, take the finite sum of the norms of its entries. Entry norms and their finite sum are measurable. The matrix norm is the finite supremum of these row sums, and finite suprema of measurable real functions are measurable.

Exercise 18. Finish the inverse-observable pipeline

How does the preceding work prove measurability of \(\omega\mapsto\log^+\lVert A(\omega)^{-1}\rVert\)?

Solution. Exercise 16 gives a measurable total inverse matrix, and Exercise 17 gives a measurable selected norm. Real.posLog is continuous and therefore measurable. Composition of the three maps proves the result, with no unit hypothesis.

Exercise 19. Compute inverse envelopes at zero and one

What are inverseValueLogPlusNormObservable 0 and inverseValueLogPlusNormObservable 1?

Solution. At zero, the cocycle value is identity. Its total inverse is identity in nonempty dimension and the unique empty matrix otherwise; in both cases the positive log of the selected norm is zero. At one, the cocycle value is the generator, so the finite-value envelope is definitionally the inverse-generator envelope after the one-step simplification.

Exercise 20. Unfold the inverse orbit sum

Derive its zero and successor equations.

Solution. The sum is over Finset.range k. At zero that range is empty, so the sum is zero. Finset.sum_range_succ says the range at k + 1 consists of the old range plus its final index k, yielding the old sum plus the inverse-generator observable at \(T^k\omega\).

Exercise 21. Reverse a two-factor inverse

If \(C_{k+1}=A_kC_k\), in what order do the factors appear after inversion?

Solution. Matrix inversion reverses multiplication, so \(C_{k+1}^{-1}=C_k^{-1}A_k^{-1}\). The order is essential because matrices need not commute. The compiled shear example shows that retaining the original order can change the matrix.

Exercise 22. Prove the finite inverse majorant

Sketch the induction proving \(Q_k\le J_k\).

Solution. Both sides are zero at horizon zero. At a successor, reverse the product under inversion, apply norm submultiplicativity, and use monotonicity of positive log. Real.posLog_mul bounds the positive log of the product by the sum of the two positive logs. The induction hypothesis controls the old finite inverse term, and the remaining term is exactly the new orbit summand.

Exercise 23. State the semantic limit of that majorant

Why is \(Q_k\le J_k\) unconditional but not informative about singular collapse?

Solution. The total inverse and positive log are defined for every matrix, so the algebraic inequality can be stated without units. For a singular matrix, however, the total inverse is zero and \(Q_k=0\). It then says nothing about how strongly the original matrix collapsed.

Exercise 24. Derive the one-value lower inequality

In nonempty matrix dimension, for a unit matrix \(M\), prove \(-\log^+\lVert M^{-1}\rVert\le\log\lVert M\rVert\).

Solution. Since \(M^{-1}M=I\), norm submultiplicativity gives \(1\le\lVert M^{-1}\rVert\lVert M\rVert\). Both norms are positive. Taking logs yields \(0\le\log\lVert M^{-1}\rVert+\log\lVert M\rVert\). The always-valid inequality \(\log\lVert M^{-1}\rVert\le \log^+\lVert M^{-1}\rVert\) enlarges the first term on the right. Rearranging the resulting inequality gives the desired lower bound.

Exercise 25. Explain why nonempty dimension enters Exercise 24

Where does the argument use a nontrivial identity norm?

Solution. It uses \(\lVert I\rVert=1\) to start the product inequality. In empty dimension, the selected norm of the unique identity matrix is zero. The public cocycle theorem handles that case separately, where both the lower rail and real-log observable are zero.

Exercise 26. Build the full lower rail

Combine the one-value lower inequality and finite inverse majorant.

Solution. In nonempty dimension, pointwise units make \(C_k(\omega)\) a unit, so Exercise 24 gives \(-Q_k(\omega)\le R_k(\omega)\). Exercise 22 gives \(Q_k\le J_k\); negating reverses the inequality and yields \(-J_k\le -Q_k\). Transitivity proves \(-J_k\le R_k\). In empty dimension, Lean takes the separate branch from Exercise 25: \(J_k\) and \(R_k\) are both zero, so the same public lower rail holds directly.

Exercise 27. Prove the upper rail

Why is \(R_k\le P_k\) unconditional?

Solution. For any real \(x\), one has \(x\le\max(0,x)\). Substitute \(x=\log\lVert C_k(\omega)\rVert\). This remains true when the norm is zero because both the real log and positive log are totalized to zero there.

Exercise 28. Transport one-step integrability along the base

Why is the inverse-generator observable composed with \(T^j\) integrable?

Solution. The tail package assumes the one-step inverse-generator observable is integrable. The cocycle stores that the base map preserves the measure, and every natural iterate of a measure-preserving map is again measure-preserving. Integrability is preserved under composition with such an iterate.

Exercise 29. Integrate the inverse orbit sum

Why is \(J_k\) integrable for each finite horizon?

Solution. By Exercise 28, every summand indexed by Finset.range k is integrable. The range is finite, and integrable functions are closed under finite sums. Therefore the orbit sum is integrable, with no appeal to an infinite series.

Exercise 30. Apply two-sided domination

Complete the proof that \(R_k\) is integrable.

Solution. The lower rail \(-J_k\) is integrable by Exercise 29 and closure under negation. The upper rail \(P_k\) is integrable by the existing forward log-positive envelope theorem. The real-log observable is measurable and satisfies \(-J_k\le R_k\le P_k\), so integrable_of_le_of_le makes the middle function integrable.

Exercise 31. Package the process candidate

Which two obligations define the signed subadditive-process candidate, and where are they discharged?

Solution. The candidate asks for integrability at every horizon and the shifted subadditive inequality. Exercise 30 supplies integrability from the three-field tail package. Pointwise invertibility, one of those fields, supplies signed shifted subadditivity through declaration 9.

Exercise 32. Analyze the infinite-measure boundary

Why is the zero forward constant integrable on real Lebesgue space while a strictly positive inverse-log constant is not?

Solution. The integral of the zero norm is zero on any measure space. A positive constant has integral equal to that constant times the total mass. Lebesgue measure of the real line is infinite, so the latter integral is infinite and the constant is not integrable.

Exercise 33. Analyze the geometric probability boundary

For atom \(n\), let its mass be \(2^{-n-1}\) and let the inverse-log size be \(2^n\). Prove that the inverse-log observable is not integrable.

Solution. The weighted absolute contribution at every atom is \(2^{-n-1}2^n=1/2\). The integral criterion for Mathlib’s geometric measure reduces integrability to summability of these contributions. The series of the constant one-half sequence diverges, so the observable is not integrable even though the total measure is one.

Exercise 34. Identify the scope of the geometric counterexample

Does that counterexample address independent sampling or an ergodic base?

Solution. No. Its base map is the identity on the natural-number sample space. It is a one-step tail counterexample: pointwise units and forward positive-log integrability do not force inverse-tail or signed one-step integrability. It makes no independence or ergodicity claim.

Exercise 35. Interpret the two-rate diagonal gap

For \(M=\operatorname{diag}(1/2,1/4)\), compare \(-\log^+\lVert M^{-1}\rVert\) with \(\log\lVert M\rVert\).

Solution. The selected norm is the maximum row sum, hence \(\lVert M\rVert=1/2\). The inverse is \(\operatorname{diag}(2,4)\), whose norm is four. The lower estimate is \(-\log 4=-2\log 2\), while the real log is \(\log(1/2)=-\log 2\). The lower rail is strict because it sees the strongest contracting direction, while the top norm sees the least contracting one.

Exercise 36. Use shears to reject same-order inversion

Why is a product of pointwise inverses in forward order not generally the inverse cocycle value?

Solution. For noncommuting matrices \(A\) and \(B\), \((AB)^{-1}=B^{-1}A^{-1}\), which need not equal \(A^{-1}B^{-1}\). Upper and lower unit shears provide explicit matrices for which the two products differ in an entry. Therefore a same-order inverse-generator product would define a different process.

Exercise 37. Prove eventual agreement at a positive limit

Suppose \(P_n/n\to\gamma\) almost everywhere with \(\gamma\gt0\). Why do \(P_n/n\) and \(R_n/n\) eventually agree at almost every convergent point?

Solution. Choose, for example, the positive threshold \(\gamma/2\). Convergence gives an eventual bound \(P_n/n\gt\gamma/2\), so for every sufficiently large positive \(n\), one has \(P_n\gt0\). Since \(P_n=\max(0,R_n)\), positivity forces \(P_n=R_n\). Dividing by the same positive natural cast preserves equality, and eventual equality transfers the limit.

Exercise 38. Explain why singular matrices remain allowed

Why does the positive-rate endpoint need no pointwise-unit hypothesis?

Solution. Its proof only uses convergence of the clipped top-norm observable and strict positivity of the limiting rate. A singular matrix can still have norm greater than one, such as diag(2,0), so singular steps are compatible with top-norm expansion. Once the realized finite-time log is positive, clipping agrees with the ordinary real log regardless of whether the underlying matrix is a unit.

Exercise 39. Close the empty-dimensional endpoint

Why is the positive-rate theorem harmless when the matrix index type is empty?

Solution. Every finite cocycle value then has selected norm zero, so every positive-log observable and its integral are zero. The integrated rate is therefore zero. The theorem’s strict positivity premise cannot be satisfied, making the specialization vacuous rather than contradictory.

Exercise 40. Give the next theorem exact hypotheses

What additional result is still required before claiming a general signed almost-everywhere limit from the RMT-34 candidate?

Solution. One needs a theorem that accepts an integrable real-valued shifted-subadditive process and proves its normalized almost-everywhere convergence under the appropriate probability and pre-ergodic hypotheses. The current module only builds the candidate and proves a separate positive-rate transfer from RMT-33. The successor RMT-35 module now supplies that signed endpoint. Calling either result inside RMT-34 a general signed Kingman theorem would exceed this page’s pinned source.

Discussion: what RMT-34 changes

The conceptual gain is a clean division of labor. Algebraic pointwise units make ordinary logarithmic identities valid. The forward moment controls expansion. The inverse moment controls finite contraction from below. Measure preservation moves the inverse moment along the same forward orbit. None of these jobs is silently assigned to another assumption.

That division also clarifies the next research step. RMT-34 has produced an integrable signed candidate with exactly the finite-time inequality expected by a real subadditive ergodic theorem. A later milestone can target that generic theorem without reopening matrix inversion or matrix measurability. Only after such a theorem is checked would it be appropriate to advertise a general signed top-growth limit.

The positive endpoint has a different logic. It does not approximate the negative tail and does not use the new candidate. It observes that a strictly positive asymptotic value eventually lies in the branch where positive-part clipping is inactive. Keeping these routes separate makes both the hypotheses and the nonclaims easier to audit.

References

The source boundary attached to each entry states exactly how it is used here.

H. Furstenberg and H. Kesten. “Products of Random Matrices.” The Annals of Mathematical Statistics 31, no. 2 (1960), 457-469. DOI record and Hebrew University research record. Used for historical placement of random matrix products, not as a claim that RMT-34 formalizes the paper’s limit theorem.

J. F. C. Kingman. “The Ergodic Theory of Subadditive Stochastic Processes.” Journal of the Royal Statistical Society: Series B 30, no. 3 (1968), 499-510. Publisher record and DOI. Used to place the process interface historically. RMT-34 does not claim a new formalization of Kingman’s general theorem.

V. I. Oseledets. “A Multiplicative Ergodic Theorem. Characteristic Lyapunov Exponents of Dynamical Systems.” Transactions of the Moscow Mathematical Society 19 (1968), 197-231. MathNet record. Used to identify the later multiplicative-ergodic destination. No spectrum, filtration, or splitting from that theorem is claimed here.

David Ruelle. “Ergodic Theory of Differentiable Dynamical Systems.” Publications Mathématiques de l’IHÉS 50 (1979), 27-58. Numdam record, DOI, and author-hosted scan. The introduction motivates derivative-cocycle applications. Theorem 1.1 and Corollary 1.2 use a forward positive-log condition; Theorem 1.6 permits a lowest exponent of negative infinity in its forward filtration; and Section 3, especially Theorem 3.1, treats the invertible setting with forward and inverse positive-log conditions. These are contextual comparisons, not imports into Lean.

Mathlib contributors. Real logarithm source at pinned commit. This is the source boundary for total Real.log, including its zero value and measurability facts.

Mathlib contributors. Positive logarithm source at pinned commit. This is the source boundary for Real.posLog, product bounds, clipping, and continuity.

Mathlib contributors. Nonsingular matrix inverse source at pinned commit. This is the source boundary for determinant-adjugate total inversion, singular-zero behavior, and reversed product inversion.

Mathlib contributors. Matrix operator norm source at pinned commit. This identifies the finite row-sup norm unfolded by the measurability proof.

Mathlib contributors. Bochner integrability source at pinned commit. This is the source boundary for finite-sum closure and domination-based integrability.

Mathlib contributors. Geometric distribution source at pinned commit. The compiled probability boundary uses geometricMeasure and integrable_geometricMeasure_iff from this file.

This project. The site-hosted checked source is taken directly from the formalization tree. Its repository provenance is commit 624c727146532d3b2656f5f23136557d5779b4fd, which requires repository access while the repository is private. The source is frozen for this note at 942 lines and SHA-256 ac950f8728e5fd003cff3b7a5d0750e5c36060730b3ebadc5b0e1165b54e72ea. This warning-fatal Lean file is the authority for every formal claim in the chapter.

Continue the ascent

Read the companion Knowledge Base chapter for a slower textbook treatment of the mathematics. Then return to the RMT-33 Development Notebook to compare the clipped convergence route with the signed finite-time package constructed here.