Singular (one-sided) cocycles: top-exponent upper bounds without invertibility #
This module develops the one-sided Lyapunov data available for a
possibly-singular matrix cocycle, i.e. a generator A : X → Matrix (Fin d) (Fin d) ℝ
that is not assumed everywhere invertible (no det A ≠ 0) and for which only
the forward integrability IntegrableLogNorm A μ (log⁺‖A‖ ∈ L¹) is assumed (no inverse
integrability IntegrableLogNorm (fun x => (A x)⁻¹) μ).
Submultiplicativity of the operator norm holds with no invertibility hypothesis
(Matrix.l2_opNorm_mul), and the positive part log⁺ = Real.posLog of a product is
subadditive (Real.posLog_mul). Hence the non-negative cocycle
gₙ x = log⁺‖A⁽ⁿ⁾(x)‖ is a genuine subadditive cocycle (Kingman index convention) that is
automatically bounded below by 0, so its normalized integrals are bounded below for free —
no log⁺‖A⁻¹‖ is needed to keep the Furstenberg–Kesten/Kingman limit finite from below.
Feeding it to tendsto_kingman_ergodic produces an a.e.-constant forward top value
λ₁⁺ := lim (1/n) log⁺‖A⁽ⁿ⁾(x)‖, and since log t ≤ log⁺ t this yields the upper bound
∀ᵐ x, limsup (fun n => (1/n) log‖A⁽ⁿ⁾(x)‖) ≤ λ₁⁺.
The same log⁺-of-a-non-negative-subadditive-quantity argument applies to the top-k
singular-value product sprod (whose submultiplicativity sprod_submul also needs no
invertibility), giving an a.e.-constant top-k volume value Γ_k⁺ with the matching
upper bound limsup (1/n) log sprod_k ≤ Γ_k⁺.
Main results #
Oseledets.isSubadditiveCocycle_posLogNorm—log⁺‖A⁽ⁿ⁾‖is a subadditive cocycle, no invertibility.Oseledets.integrable_posLogNorm_cocycle,Oseledets.bddBelow_posLogNorm— the Kingman provisos, discharged fromIntegrableLogNorm A μalone.Oseledets.tendsto_top_posLogNorm— the a.e.-constant forward top valueλ₁⁺.Oseledets.limsup_logNorm_le_top— the upper boundlimsup (1/n) log‖A⁽ⁿ⁾‖ ≤ λ₁⁺.Oseledets.isSubadditiveCocycle_posLogSprod,Oseledets.integrable_posLogSprod,Oseledets.tendsto_top_posLogSprod,Oseledets.limsup_logSprod_le_top— the analogous top-kvolume statements viasprod_submul.
Implementation notes #
- These are one-sided upper bounds only. There is no Oseledets filtration, no exact
exponents, and no lower bound for a singular cocycle: a singular generator can collapse
directions, so
(1/n) log‖A⁽ⁿ⁾‖need not converge, and the limit may live in[-∞, ∞). Thelimsupis bounded above by the forward top valueλ₁⁺, which is thelog⁺(notlog) Furstenberg–Kesten constant. λ₁⁺andΓ_k⁺are the limits of the positive partslog⁺‖A⁽ⁿ⁾‖,log⁺ sprod_k. They coincide with the usual exponents whenever the latter are≥ 0; when the cocycle is asymptotically contracting they are pinned at0and the boundlimsup log-growth ≤ λ₁⁺remains correct (the true growth is then≤ 0).- The development uses neither
∀ x, (A x).det ≠ 0norIntegrableLogNorm (fun x => (A x)⁻¹) μ; only the forward hypothesisIntegrableLogNorm A μis needed. - Ergodicity (via
tendsto_kingman_ergodic) makesλ₁⁺,Γ_k⁺a.e. constant; a non-ergodic variant replaces these by invariant measurable functions (tendsto_kingman).
References #
- H. Furstenberg and H. Kesten, Products of random matrices, Ann. Math. Statist. 31 (1960), 457–469.
- M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).
Real-analysis helpers: log ≤ log⁺, measurability of log⁺ #
The non-negative subadditive cocycle log⁺‖A⁽ⁿ⁾‖ (no invertibility) #
The forward log⁺-norm cocycle is subadditive with NO invertibility hypothesis.
gₙ = log⁺‖A⁽ⁿ⁾‖ satisfies the Kingman bound g (m+n) x ≤ g m x + g n (T^[m] x), using only
submultiplicativity of the L2 operator norm (Matrix.l2_opNorm_mul) and subadditivity of the
positive part of the logarithm (Real.posLog_mul). No det A ≠ 0 is required.
Upper bound by a Birkhoff sum: log⁺‖A⁽ⁿ⁾(x)‖ ≤ birkhoffSum T (log⁺‖A‖) n x. This is the
subadditive-cocycle bound g (n) ≤ birkhoffSum (g 1) n specialised to gₙ = log⁺‖A⁽ⁿ⁾‖.
Integrability of each level gₙ = log⁺‖A⁽ⁿ⁾‖ from the forward hypothesis alone:
0 ≤ gₙ ≤ birkhoffSum (log⁺‖A‖) n, the upper bound integrable since log⁺‖A‖ ∈ L¹. No
inverse integrability is used.
Bounded-below proviso for free. Since gₙ = log⁺‖A⁽ⁿ⁾‖ ≥ 0, its normalized integrals
are bounded below by 0 — no log⁺‖A⁻¹‖ ∈ L¹ is needed (contrast with
Oseledets.furstenbergKesten_norm).
The a.e.-constant forward top value λ₁⁺ and the upper bound #
The forward top value λ₁⁺ (Furstenberg–Kesten with log⁺, no invertibility). For an
ergodic measure-preserving T and a possibly-singular measurable generator with
log⁺‖A‖ ∈ L¹, the normalized positive-part log-norms (1/n) log⁺‖A⁽ⁿ⁾(x)‖ converge μ-a.e.
to a constant λ₁⁺. This uses only the forward integrability hypothesis.
Upper bound on the singular top exponent. For an ergodic measure-preserving T and
a possibly-singular measurable generator with log⁺‖A‖ ∈ L¹ (and no invertibility, no
inverse integrability), there is a constant λ₁⁺ such that for μ-a.e. x
limsup (fun n => ((1/n) log‖A⁽ⁿ⁾(x)‖ : EReal)) ≤ λ₁⁺.
Here λ₁⁺ is the a.e. limit of (1/n) log⁺‖A⁽ⁿ⁾‖ (tendsto_top_posLogNorm). The proof bounds
each term using log ≤ log⁺ and passes to the EReal limsup (the log⁺ sequence converges,
so its limsup equals λ₁⁺). The limsup is taken in EReal so that the statement is
unconditional even when the growth rate tends to −∞ (the genuinely singular case): the true
top growth rate lives in [−∞, ∞) and is bounded above by λ₁⁺. This is a one-sided UPPER
bound only — the liminf is unbounded below in general (a singular cocycle may collapse
directions), so no two-sided exponent is claimed.
Top-k volume upper bound via sprod (still no invertibility) #
sprod A T k n x = ∏_{i<k} σᵢ(A⁽ⁿ⁾) is the top-k singular-value product (the k-volume
growth). Its submultiplicativity sprod_submul holds with no invertibility, and
sprod ≥ 0 always, so the same log⁺-of-a-non-negative-subadditive-quantity construction
gives an a.e.-constant forward top-k volume value Γ_k⁺ and the matching upper bound.
log⁺ sprod_k is a subadditive cocycle with NO invertibility. From sprod_submul
(submultiplicativity of the top-k singular-value product, which needs no det ≠ 0) and
Real.posLog_mul, with the symmetric Kingman split.
Birkhoff-sum upper bound for log⁺ sprod_k: log⁺ sprod_k(n) ≤ k · birkhoffSum (log⁺‖A‖) n.
Each singular value is ≤ ‖A⁽ⁿ⁾‖, so sprod_k ≤ ‖A⁽ⁿ⁾‖^k, and log⁺ is monotone with
log⁺ (t^k) = k · log⁺ t.
Integrability of each level log⁺ sprod_k from the forward hypothesis alone:
0 ≤ log⁺ sprod_k ≤ k · birkhoffSum (log⁺‖A‖) n. No invertibility, no inverse integrability.
Bounded-below proviso for free (log⁺ sprod_k ≥ 0).
The forward top-k volume value Γ_k⁺. For an ergodic measure-preserving T and a
possibly-singular measurable generator with log⁺‖A‖ ∈ L¹, the normalized positive-part log
volumes (1/n) log⁺ sprod_k(x) converge μ-a.e. to a constant Γ_k⁺, using only the forward
integrability.
Top-k volume upper bound (singular cocycle). For an ergodic measure-preserving T and
a possibly-singular measurable generator with log⁺‖A‖ ∈ L¹ (no invertibility, no inverse
integrability), there is a constant Γ_k⁺ such that for μ-a.e. x
limsup (fun n => ((1/n) log sprod_k(x) : EReal)) ≤ Γ_k⁺,
i.e. the top-k volume growth rate is bounded above by the forward top-k value. The limsup
is taken in EReal so the bound is unconditional even when the volume collapses
(sprod_k → 0, growth → −∞). One-sided UPPER bound only. Carries [NeZero d] (the d = 0
algebra is trivial).
EReal-limit packaging and the exact limsup of the genuine log #
The results above bound limsup (1/n) log‖A⁽ⁿ⁾‖ ≤ λ₁⁺ in EReal. The log⁺ sequence has an
ℝ-limit (tendsto_top_posLogNorm), so its EReal-coercion also converges
(tendsto_top_posLogNorm_ereal), and its EReal-limsup and liminf both equal λ₁⁺
(limsup_eq_liminf_posLogNorm). The sharper statement limsup_logNorm_eq_top_of_pos shows that,
when the forward top value λ₁⁺ is strictly positive, the limsup of the genuine
(1/n) log‖A⁽ⁿ⁾‖ (not log⁺) is exactly λ₁⁺. A genuine limit of (1/n) log‖A⁽ⁿ⁾‖ is false in
general for a singular cocycle (the liminf may be strictly below the limsup, even −∞), so only
the limsup is identified, and only when λ₁⁺ > 0: the contracting case λ₁⁺ = 0 breaks the
equality, so the positivity hypothesis is essential.
EReal-valued limit of the normalized log⁺-norms. Lifts the genuine ℝ-limit
tendsto_top_posLogNorm through the embedding ℝ ↪ EReal (continuous_coe_real_ereal): the
EReal-coerced sequence ((1/n) log⁺‖A⁽ⁿ⁾‖ : EReal) converges μ-a.e. to (λ₁⁺ : EReal).
The limsup/liminf of the EReal log⁺-norm sequence coincide (both equal λ₁⁺).
Since the EReal-coerced sequence converges (tendsto_top_posLogNorm_ereal), its limsup and
liminf coincide with the limit. The EReal-limsup/liminf are unconditional (EReal is a
complete linear order).
The canonical forward top value λ₁⁺, and the exact limsup of the genuine log-norm
growth when it is positive. For an ergodic measure-preserving T and a possibly-singular
measurable generator with log⁺‖A‖ ∈ L¹, there is a constant λ₁⁺ that is the μ-a.e. limit
of the normalized positive-part log-norms (1/n) log⁺‖A⁽ⁿ⁾‖ (this pins λ₁⁺ to the genuine
top value, not an arbitrary witness), and such that, whenever λ₁⁺ > 0, for μ-a.e. x
limsup (fun n => ((1/n) log‖A⁽ⁿ⁾(x)‖ : EReal)) = λ₁⁺.
This sharpens limsup_logNorm_le_top from ≤ to =. The ≤ half reuses the body of
limsup_logNorm_le_top (ereal_limsup_le_of_tendsto_dom). The ≥ half is the new content:
on the a.e. set where (1/n) log⁺‖A⁽ⁿ⁾‖ → λ₁⁺ > 0, the sequence is eventually positive, forcing
log⁺‖A⁽ⁿ⁾‖ > 0, hence log‖A⁽ⁿ⁾‖ > 0 and so log⁺‖A⁽ⁿ⁾‖ = log‖A⁽ⁿ⁾‖
(posLog_eq_log_of_log_nonneg); the two EReal sequences are thus eventually equal, so their
limsups agree (Filter.limsup_congr), and the latter equals λ₁⁺ (limsup_eq_liminf_posLogNorm
/ tendsto_top_posLogNorm_ereal). The positivity hypothesis is essential: in the contracting
case λ₁⁺ = 0 the genuine log-growth may tend to −∞, so its limsup can be strictly below
λ₁⁺ and the equality fails.
EReal-valued limit of the normalized log⁺ sprod_k. Top-k mirror of
tendsto_top_posLogNorm_ereal: lifts the genuine ℝ-limit tendsto_top_posLogSprod through
continuous_coe_real_ereal, so ((1/n) log⁺ sprod_k(x) : EReal) converges μ-a.e. to
(Γ_k⁺ : EReal).
The canonical forward top-k value Γ_k⁺, and the exact limsup of the genuine top-k
log-volume growth when it is positive. Top-k mirror of limsup_logNorm_eq_top_of_pos. For
an ergodic measure-preserving T and a possibly-singular measurable generator with
log⁺‖A‖ ∈ L¹, there is a constant Γ_k⁺ that is the μ-a.e. limit of the normalized
positive-part log-volumes (1/n) log⁺ sprod_k (this pins Γ_k⁺ to the genuine top-k value),
and such that, whenever Γ_k⁺ > 0, for μ-a.e. x
limsup (fun n => ((1/n) log sprod_k(x) : EReal)) = Γ_k⁺.
This sharpens limsup_logSprod_le_top from ≤ to =. The ≤ half reuses the body of
limsup_logSprod_le_top; the ≥ half uses that on the a.e. set where (1/n) log⁺ sprod_k → Γ_k⁺ > 0, the sequence is eventually positive, forcing log⁺ sprod_k > 0, hence log sprod_k > 0
and log⁺ sprod_k = log sprod_k (posLog_eq_log_of_log_nonneg); the two EReal sequences are
eventually equal so their limsups agree (Filter.limsup_congr). The positivity hypothesis is
essential (the contracting case Γ_k⁺ = 0 breaks the equality). Carries [NeZero d].