Log-positive integrability envelope

Start with a four-state clock:

Give \(\Omega\) the discrete measurable structure, in which every subset is an allowed event, and define

This is a probability measure because the four masses add to one. The map \(T\) merely rotates those equal masses, so it preserves \(\mu\).

At the four states, let a one-dimensional matrix cocycle use the positive scalar generators

A one-by-one matrix is still a matrix. Its induced infinity norm is the absolute value of its only entry. Starting at state \(0\), the chronological norms are therefore

The exact four-step product norm is

Its positive logarithmic growth is

Now clip every one-step contraction before adding:

Thus

The gap is the whole point. The exact product incorporates the contractions \(1/2\) and \(1/4\), which offset part of the expansion. The envelope deletes those negative logarithms, so it is easier to integrate but intentionally less precise.

This scalar model was chosen to expose the bookkeeping. General matrices need not commute, but their norms still satisfy the submultiplicative inequality that drives the same envelope estimate.

Define the observable

A log-positive integrability envelope is a real-valued upper-growth observable for a matrix cocycle. It keeps positive logarithmic expansion and clips everything else to zero. If

is the finite-time maximum absolute row-sum norm, define

Here \(C(k,\omega)\) is the cocycle matrix after \(k\) steps from base state \(\omega\). The notation \(\log^+\), read “log positive,” is Mathlib’s Real.posLog. The result \(P_k:\Omega\to\mathbb R\) is measurable and nonnegative.

The word envelope is essential. \(P_k\) controls the positive tail of norm growth, but it does not preserve the full logarithmic dynamics. It sends exact collapse, strict contraction, and neutral norm one to the same real value zero.

What the gate retains and discards

For a nonnegative real norm \(r\), Mathlib’s definition gives the piecewise picture

The overlap at \(r=1\) is harmless because both branches equal zero. The construction is continuous even at \(r=0\), where Lean’s total real logarithm also has value zero.

Compare it with the extended log-norm observable \(L_k\) from RMT-14:

Thus \(P_k\) is not a replacement for \(L_k\). It is the simpler real majorant needed to state an ordinary Bochner-integrability hypothesis for the expanding part.

Finite-time subadditivity

RMT-14 proves norm submultiplicativity across the one-sided cocycle split:

The positive logarithm is monotone on nonnegative inputs, and Mathlib proves

Consequently RMT-15 obtains

This is still a pointwise finite-time inequality. It invokes no probability, ergodicity, expectation, or limiting theorem.

The orbit-sum majorant

The one-step envelope is sampled along the forward base orbit and added:

Lean names this function orbitLogPlusSum. The empty sum is zero, and extending the horizon appends the newest shifted one-step term:

Induction with finite-time subadditivity proves the domination estimate

The right side is deliberately loose. It discards cancellation between matrix factors and every contracting one-step contribution. Its value is that it is a finite sum of copies of one measurable function pulled back along the base orbit.

The explicit integrability hypothesis

The project does not derive integrability from measure preservation. It names the missing assumption:

def HasIntegrableGeneratorLogPlus
    (C : DiscreteMatrixCocycle (ι := ι) μ) : Prop :=
  Integrable (C.logPlusNormObservable 1) μ

For a real-valued function, Mathlib’s Integrable predicate is absolute Bochner integrability with respect to the stated measure. Because \(P_1\) is nonnegative, this asks for a finite integral of its expanding tail. The measure \(\mu\) may be arbitrary. The definition does not assert \(\mu(\Omega)=1\), so the integral is not automatically an expectation.

The bundled base map is a measure-preserving transformation . Every natural iterate therefore also preserves \(\mu\), and integrability survives pullback:

A finite sum of those pullbacks is integrable, so \(S_k\) is integrable. Finally, measurability and \(0\le P_k\le S_k\) transfer integrability to every finite-horizon \(P_k\).

How the Lean interface is layered

The sixteen exported declarations deliberately separate four claims that are often compressed into one sentence.

First, logPlusNormObservable defines \(P_k\), while logPlusNormObservable_nonneg, logPlusNormObservable_zero, logPlusNormObservable_one, and measurable_logPlusNormObservable establish its elementary pointwise and measurable behavior. The finite split theorem logPlusNormObservable_add_le remains algebraic and pointwise.

Second, orbitLogPlusSum defines \(S_k\). Its zero and successor theorems fix the indexing convention, and measurable_orbitLogPlusSum proves the finite sum measurable. The theorem logPlusNormObservable_le_orbitLogPlusSum is the pointwise bridge \(P_k\le S_k\). None of these declarations assumes the generator envelope is integrable.

Third, HasIntegrableGeneratorLogPlus names the missing one-step hypothesis. It is a proposition attached to a cocycle, not a field silently inserted into every cocycle and not a conclusion of measure preservation.

Fourth, the three declarations in the HasIntegrableGeneratorLogPlus namespace propagate that hypothesis to base iterates, orbit sums, and finally finite-horizon envelopes. This order makes the proof auditable: transport, finite addition, then domination.

In Lean: define the clipped observable

C.logPlusNormObservable k ω = log⁺ (C.normObservable k ω)

The exact project definition is:

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

Read fun ω ↦ … as “the function that sends \(\omega\) to …”. The result type Ω → ℝ is a real-valued observable, not a measure and not yet an integral.

In Lean: dominate a horizon by one-step terms

C.logPlusNormObservable_le_orbitLogPlusSum k ω

The definition being bounded is:

def orbitLogPlusSum
    (C : DiscreteMatrixCocycle (ι := ι) μ) (k : ℕ) : Ω → ℝ :=
  fun ω ↦ ∑ j ∈ Finset.range k,
    C.logPlusNormObservable 1 (C.base^[j] ω)

At k = 0, Finset.range 0 is empty, so this sum is zero. At k + 1, the new term has index k. That is the same half-open indexing convention used in the paper sum.

In Lean: propagate the integrability certificate

hC.integrable_logPlusNormObservable k

The proof uses two reusable intermediate certificates:

hC.integrable_at_base_iterate j
hC.integrable_orbitLogPlusSum k
hC.integrable_logPlusNormObservable k

They correspond, in order, to preservation under the shift, closure under a finite sum, and domination of the target observable by that sum.

Three common misreads

“Zero positive log means no dynamics.” False. It can mean exact annihilation, strict contraction, or norm one. The full matrix can still rotate, project, shear within unit norm, or collapse every vector.

“An integrable expanding tail gives an integrable logarithm.” False. The negative tail has been deleted. A zero matrix is the sharp counterexample: \(P_k=0\) but \(L_k=\bot\).

“A preserved measure turns the integral into an expectation.” False. Preservation says that pulling an integrable function along the base does not destroy integrability. Only a separately supplied probability normalization would justify expectation language.

Read the four-state integrability ledger

In the opening model, the one-step observable has four values:

Every function on this finite space is measurable. All four displayed values are finite, so the function is integrable. Its integral is

Because \(\mu\) is a probability measure, this integral may also be called the expectation of \(P_1\). The project definition does not assume probability, so its general theorem correctly says “integrable” rather than “has finite expectation.”

Composing with the rotation only permutes the value list. For example,

The integral remains \(5\log2/4\). The same holds for every iterate \(P_1\circ T^j\). Adding four such shifted functions gives an integrable orbit sum. The theorem then uses

and measurability of \(P_4\) to transfer integrability from \(S_4\) to \(P_4\). This last step is a domination argument, not another appeal to measure preservation.

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 checked implementation is in LogPlusIntegrability.lean. Its pointwise finite-horizon split first combines norm submultiplicativity, monotonicity of positive log, and the positive-log product inequality:

theorem logPlusNormObservable_add_le
    (C : DiscreteMatrixCocycle (ι := ι) μ) (m k : ℕ) (ω : Ω) :
    C.logPlusNormObservable (m + k) ω ≤
      C.logPlusNormObservable k (C.base^[m] ω) +
        C.logPlusNormObservable m ω := by
  calc
    log⁺ (C.normObservable (m + k) ω) ≤
        log⁺ (C.normObservable k (C.base^[m] ω) * C.normObservable m ω) :=
      Real.posLog_le_posLog (norm_nonneg _) (C.normObservable_add_le m k ω)
    _ ≤ log⁺ (C.normObservable k (C.base^[m] ω)) +
        log⁺ (C.normObservable m ω) := Real.posLog_mul

The first line after calc replaces the whole-product norm by a product of block norms. The second turns positive log of that product into a sum. No integration occurs in this theorem.

The final integrability theorem makes the proof order explicit:

theorem HasIntegrableGeneratorLogPlus.integrable_logPlusNormObservable
    {C : DiscreteMatrixCocycle (ι := ι) μ}
    (hC : C.HasIntegrableGeneratorLogPlus) (k : ℕ) :
    Integrable (C.logPlusNormObservable k) μ := by
  apply (hC.integrable_orbitLogPlusSum k).mono'
    (C.measurable_logPlusNormObservable k).aestronglyMeasurable
  filter_upwards with ω
  rw [Real.norm_eq_abs, abs_of_nonneg (C.logPlusNormObservable_nonneg k ω)]
  exact C.logPlusNormObservable_le_orbitLogPlusSum k ω

The mono’ domination principle asks for an integrable majorant, an almost-everywhere strongly measurable target, and an almost-everywhere norm bound. The project has a pointwise bound, so it is strong enough to discharge the almost-everywhere obligation.

Standalone tutorial: arithmetic worksheet

Standalone tutorial. The real logarithm is analytic, but the opening example uses powers of two. We can therefore record every log size exactly by its coefficient of \(\log2\). This complete program imports only Std; it does not import Mathlib or the project.

Save it as LogPositiveEnvelopeScratch.lean:

import Std

namespace LogPositiveEnvelopeScratch

-- A value e represents the scalar generator norm 2^e.
def exponents : List Int := [-1, 2, -2, 3]

-- log⁺(2^e) = max(0, e) · log 2.
def positiveLogCoeff (e : Int) : Nat :=
  e.toNat

def productExponent : Int :=
  exponents.foldl (fun total e => total + e) 0

def finiteLogPlusCoeff : Nat :=
  positiveLogCoeff productExponent

def orbitEnvelopeCoeff : Nat :=
  (exponents.map positiveLogCoeff).sum

def envelopeBoundHolds : Bool :=
  decide (finiteLogPlusCoeff ≤ orbitEnvelopeCoeff)

#eval exponents.map positiveLogCoeff
#eval productExponent
#eval finiteLogPlusCoeff
#eval orbitEnvelopeCoeff
#eval envelopeBoundHolds
#eval (orbitEnvelopeCoeff, exponents.length)

end LogPositiveEnvelopeScratch

Run exactly this small file on macOS or Linux with the pinned Lean toolchain:

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

The outputs should be [0, 2, 0, 3], 2, 2, 5, true, and (5, 4). They encode

The worksheet checks the finite arithmetic only. A list of integer exponents does not define Mathlib’s matrix cocycle or measure-preserving map, and it supplies no Bochner-integrability proof.

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 Real.posLog
#check Real.posLog_nonneg
#check Real.posLog_mul
#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.orbitLogPlusSum
#check DiscreteMatrixCocycle.orbitLogPlusSum_zero
#check DiscreteMatrixCocycle.orbitLogPlusSum_succ
#check DiscreteMatrixCocycle.logPlusNormObservable_le_orbitLogPlusSum
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.integrable_at_base_iterate
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.integrable_orbitLogPlusSum
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.integrable_logPlusNormObservable

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

Empty matrix dimension

When the matrix index type is empty, RMT-14 proves \(N_k=0\) at every horizon. Because \(\log^+0=0\), RMT-15 proves

for every \(k\) and \(\omega\). This also explains why the time-zero identity \(P_0=0\) needs no Nonempty ι assumption: the inhabited branch has norm one, while the empty branch has norm zero, and positive log sends both to zero.

The module does not export a separate empty-dimensional theorem for every orbit sum or integrability proposition. Those consequences can be derived from the checked zero observable and general finite-sum facts when needed.

What this envelope does not establish

The RMT-15 interface does not prove:

• integrability of the RMT-14 EReal-valued extended log norm;
• any estimate for negative logarithmic growth or inverse-matrix norms;
• that cocycle matrices are nonzero, injective, or invertible;
• a probability normalization, expectation, or distributional law;
• ergodicity, mixing, independence, or identical distribution;
• a normalized process such as \(k^{-1}P_k\) or \(k^{-1}L_k\);
• convergence, an almost-sure growth rate, or a deterministic limit;
• Kingman’s subadditive ergodic theorem or the Furstenberg-Kesten theorem;
• a Lyapunov exponent, Lyapunov spectrum, or Oseledets splitting;
• a two-sided cocycle or negative-time dynamics; or
• a derivative, tangent-space, or random-Jacobian interpretation.

An integrable \(P_k\) can coexist with complete collapse. If \(C(k,\omega)=0\), then \(P_k(\omega)=0\) while the extended log norm is \(\bot\). Positive-tail integrability alone therefore says nothing about the negative endpoint needed for a full Lyapunov analysis.

Where to continue

RMT-34 repairs the missing negative tail under an explicit, stronger interface. The integrable generator log tails package combines pointwise matrix units with integrable forward and inverse one-step log-positive norms, producing integrable lower and upper rails around every finite-time real log norm. A checked geometric-probability example shows that the forward moment does not imply the inverse moment. There is one separate shortcut: if the RMT-33 log-positive rate is strictly positive, the positive log and real log eventually agree almost everywhere without those inverse assumptions. That shortcut proves no result in the zero or negative rate regime.

The integrated log-positive growth rate is the RMT-16 successor. It integrates each finite-horizon envelope, proves under the same explicit one-step integrability hypothesis that the resulting real sequence is subadditive, and applies deterministic Fekete convergence over positive horizons. The successor still assumes no probability normalization or ergodicity and proves no samplewise or Lyapunov limit.

Finite-Horizon Log-Positive Cocycle Integrability derives the complete sixteen-declaration Lean layer, including the orbit-sum recurrence, measure-preserving pullbacks, finite-sum integrability, and the final domination proof.

Finite-Time Norm and Extended-Log-Norm Observables for Matrix Cocycles develops the zero-faithful predecessor. The one-sided discrete matrix cocycle entry supplies the shifted base orbit and product convention.

References

Mathlib contributors. The positive part of the logarithm, Mathlib 4 documentation. This official source defines Real.posLog, proves nonnegativity, continuity, monotonicity on nonnegative inputs, and the two-factor product estimate used by RMT-15.

Mathlib contributors. Bochner integrability, Mathlib 4 documentation. This official source contains integrability under a measure-preserving pullback, finite-sum closure, and domination principles.

J. F. C. Kingman. The ergodic theory of subadditive stochastic processes, Journal of the Royal Statistical Society: Series B 30(3), 499-510, 1968. This primary source is a later asymptotic destination. The present envelope supplies only finite-horizon measurability, domination, and integrability.

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