The genuine singular Lyapunov spectrum is μ-a.e. constant (det-free)

For a possibly-singular matrix cocycle generator A : X → Matrix (Fin d) (Fin d) ℝ — no det A ≠ 0, no inverse integrability, only forward integrability log⁺‖A‖ ∈ L¹ — this module proves that the genuine (−∞-aware) per-direction forward singular Lyapunov exponent λ_k^gen = Oseledets.singularSpectralValue A T k is μ-a.e. constant under an ergodic measure-preserving T:

∃ c : EReal, ∀ᵐ x ∂μ, singularSpectralValue A T k x = c.

The route (integrability-free sub-invariance)

The standard Kingman path to a.e.-constant exponents needs the cocycle bounded below, a proviso the genuine −∞-aware exponent lacks (it can fall to ⊥ on the kernel / volume-collapse stratum). We sidestep integrability entirely:

1. Per-direction singular-value submultiplicativity σ_k(g ∘ f) ≤ σ_k(g) · ‖f‖ (Oseledets.singularValues_comp_le_opNorm). This is a Courant–Fischer dimension count built on Oseledets.Weyl (spanP, quad_ge_on_top, quad_le_on_bot, finrank_spanP): the top-(k+1) eigenspace of (g ∘ f)*(g ∘ f) (dim k+1) and the f-preimage of the bottom-(n-k) eigenspace of g*g (dim ≥ n-k) sum to dimension > n, hence meet nonzero, pinning the squared singular value. It is the genuine Horn inequality that Mathlib lacks.

2. Sub-invariance λ_k^gen(x) ≤ λ_k^gen(T x) for every x (Oseledets.singularSpectralValue_le_comp). From cocycle (n+1) x = cocycle n (T x) · A x and step 1, σ_k(A⁽ⁿ⁺¹⁾ x) ≤ σ_k(A⁽ⁿ⁾(T x)) · ‖A x‖. After (1/n) log and limsup, the fixed single-step factor log ‖A x‖ washes out ((1/n) · c → 0), giving the bound. The reverse genuinely needs the smallest singular value of A x (invertibility), so only sub-invariance is claimed.

3. Sub-invariant ⟹ invariant without integrability (Oseledets.singularSpectralValue_invariant_ae). Compose with the bounded strictly-monotone transform EReal.exp : EReal → ℝ≥0∞ (an order-iso, so injective). h := exp ∘ λ_k^gen is ≤ a finite constant exp λ₁⁺ a.e. (the forward top value, via Oseledets.ae_singularSpectralValue_lt_top), so ∫⁻ h < ∞; h ≤ h ∘ T a.e. and ∫⁻ (h ∘ T) = ∫⁻ h (measure-preserving) give h =ᵐ h ∘ T (MeasureTheory.ae_eq_of_ae_le_of_lintegral_le); injectivity of exp lifts back to λ_k^gen =ᵐ λ_k^gen ∘ T.

4. Invariant ⟹ a.e. constant under ergodicity (Oseledets.ae_singularSpectralValue_eq_const), via Ergodic.ae_eq_const_of_ae_eq_comp₀ (EReal is Polish, hence has a countably-separated Borel structure).

Main results

• Oseledets.singularValues_comp_le_opNorm — the per-direction Horn submultiplicativity σ_k(g ∘ f) ≤ σ_k(g) · ‖f‖.
• Oseledets.singularSpectralValue_le_comp — deterministic sub-invariance λ_k^gen(x) ≤ λ_k^gen(T x).
• Oseledets.singularSpectralValue_invariant_ae — λ_k^gen =ᵐ λ_k^gen ∘ T (integrability-free).
• Oseledets.ae_singularSpectralValue_eq_const — the headline: λ_k^gen is μ-a.e. constant.

References

• A. Quas, Multiplicative Ergodic Theorems and Applications (Theorem 2, §3.1).
• M. S. Raghunathan, A proof of Oseledec's multiplicative ergodic theorem, Israel J. Math. 32 (1979), 356–362.
• R. A. Horn, C. R. Johnson, Topics in Matrix Analysis (Thm 3.3.16, singular-value submultiplicativity).

Per-direction singular-value submultiplicativity (Horn inequality)

The genuine Horn inequality σ_k(g ∘ f) ≤ σ_k(g) · ‖f‖ is built from the Courant–Fischer dimension-count infrastructure of Oseledets.Weyl. Mathlib provides only σ_k ≤ ‖·‖ (LinearMap.singularValues_le_opNorm) and the product submultiplicativity of Oseledets.sprod; the per-index bound is new.

theorem Oseledets.singularValues_comp_le_opNorm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f g : E →ₗ[ℝ] E) (i : ℕ) : (g ∘ₗ f).singularValues i ≤ g.singularValues i * ‖LinearMap.toContinuousLinearMap f‖

Per-direction singular-value submultiplicativity (Horn). For f g : E →ₗ[ℝ] E on a finite-dimensional inner product space and any i, the i-th singular value of the composition is bounded by σ_i(g) · ‖f‖ (‖f‖ the operator norm ‖toContinuousLinearMap f‖): σ_i(g ∘ₗ f) ≤ σ_i(g) · ‖f‖.

Proof by the Courant–Fischer dimension count. Write n = finrank ℝ E. For i < n, σ_i(g ∘ₗ f)² = μ_i(S') and σ_i(g)² = μ_i(S) are sorted eigenvalues of the Gram operators S' = (g ∘ₗ f)*(g ∘ₗ f) and S = g* g. The top-(i+1) eigenspace V of S' (dim i+1) and W := f⁻¹(bottom-(n-i) eigenspace of S)(dim≥ n-i) have dim V + dim W ≥ n+1, so meet at a nonzero v. There σ_i(g ∘ₗ f)²‖v‖² ≤ ‖g(f v)‖²(top bound forS') and, since f vlies in the bottom eigenspace ofS, ‖g(f v)‖² ≤ σ_i(g)²‖f v‖² ≤ σ_i(g)²‖f‖²‖v‖²(bottom bound forSplus `‖f v‖ ≤ ‖f‖‖v‖). For i ≥ nthe left side is0`.

The (n+1)⁻¹ → n⁻¹ reindexing of the EReal-limsup

Sub-invariance compares cocycle (n+1) x (at x) with cocycle n (T x) (at T x), so the defining limsup of λ_k^gen(x) (normalized by (n+1)⁻¹ after the +1 shift) must be compared with that of λ_k^gen(T x) (normalized by n⁻¹). The two normalizations are asymptotically equivalent, but because the genuine exponent is unbounded below (it can fall to ⊥), the standard "perturbation tends to 0" lemma (which needs two-sided boundedness, à la Oseledets.lambdaBar_equivariant) does not apply. The bound limsup ((n+1)⁻¹ Bₙ) ≤ limsup (n⁻¹ Bₙ) is still true and proved here directly via Filter.limsup_le_iff, using only that the target limsup is < ⊤: for any threshold y above it, n⁻¹ Bₙ < y' eventually for some y' < y, and then (n+1)⁻¹ Bₙ = (n⁻¹ Bₙ) · (n/(n+1)) is ≤ y' (if n⁻¹ Bₙ ≥ 0) or ≤ y' · n/(n+1) → y' < y (if n⁻¹ Bₙ < 0); either way < y eventually.

theorem Oseledets.limsup_inv_succ_mul_add_le (B : ℕ → EReal) (cr : ℝ) : Filter.limsup (fun (n : ℕ) => (↑↑n + 1)⁻¹ * (B n + ↑cr)) Filter.atTop ≤ Filter.limsup (fun (n : ℕ) => (↑↑n)⁻¹ * B n) Filter.atTop

Reindexing the EReal-limsup from (n+1)⁻¹ to n⁻¹. For B : ℕ → EReal and a finite real additive perturbation cr : ℝ,

limsup_n ((n+1)⁻¹ · (Bₙ + cr)) ≤ limsup_n (n⁻¹ · Bₙ).

The (n+1)⁻¹ normalization (after the +1 shift of the defining sequence) is dominated by the n⁻¹ one even though Bₙ may be unbounded below; the perturbation washes out ((n+1)⁻¹ · cr → 0). The bound is proved via Filter.limsup_le_iff: for y above the target limsup, pick a finite real z with the target < z < y; then n⁻¹ Bₙ < z eventually, so Bₙ ≤ n · z, and (n+1)⁻¹ (Bₙ + cr) ≤ (n·z + cr)/(n+1) → z < y.

Deterministic sub-invariance of λ_k^gen

theorem Oseledets.singularValue_cocycle_succ_le {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (k n : ℕ) (x : X) : (Matrix.toEuclideanLin (cocycle A T (n + 1) x)).singularValues k ≤ (Matrix.toEuclideanLin (cocycle A T n (T x))).singularValues k * ‖A x‖

The single-step Horn bound for the cocycle. From cocycle (n+1) x = cocycle n (T x) · A x and the per-direction submultiplicativity Oseledets.singularValues_comp_le_opNorm,

σ_k(A⁽ⁿ⁺¹⁾ x) ≤ σ_k(A⁽ⁿ⁾(T x)) · ‖A x‖.

theorem Oseledets.logSingularValue_cocycle_succ_le {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (k n : ℕ) (x : X) : (ENNReal.ofReal ((Matrix.toEuclideanLin (cocycle A T (n + 1) x)).singularValues k)).log ≤ (ENNReal.ofReal ((Matrix.toEuclideanLin (cocycle A T n (T x))).singularValues k)).log + (ENNReal.ofReal ‖A x‖).log

The single-step Horn bound in −∞-aware log form. Applying ENNReal.log ∘ ofReal to Oseledets.singularValue_cocycle_succ_le (with log monotone and ENNReal.log_mul_add),

log σ_k(A⁽ⁿ⁺¹⁾ x) ≤ log σ_k(A⁽ⁿ⁾(T x)) + log ‖A x‖ (in EReal, log = ENNReal.log).

theorem Oseledets.singularSpectralValue_le_comp {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (k : ℕ) (x : X) : singularSpectralValue A T k x ≤ singularSpectralValue A T k (T x)

Deterministic sub-invariance of the genuine per-direction exponent. For every x (no invertibility, no integrability, no ergodicity), λ_k^gen(x) ≤ λ_k^gen(T x). From the single-step Horn log bound log σ_k(A⁽ⁿ⁺¹⁾ x) ≤ log σ_k(A⁽ⁿ⁾(T x)) + log ‖A x‖ (Oseledets.logSingularValue_cocycle_succ_le), the defining limsup of λ_k^gen(x) shifts by +1 (Filter.limsup_nat_add) and is dominated by the n⁻¹-normalized limsup at T x plus the fixed single-step term log ‖A x‖ that washes out, via the reindexing Oseledets.limsup_inv_succ_mul_add_le. The reverse inequality genuinely needs the smallest singular value of A x (invertibility), so only the sub-invariant direction is established.

Sub-invariant ⟹ invariant ⟹ a.e. constant

theorem Oseledets.ae_singularSpectralValue_le {X : Type u_1} [MeasurableSpace X] {T : X → X} {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] [NeZero d] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (k : ℕ) : ∃ (lam : ℝ), ∀ᵐ (x : X) ∂μ, singularSpectralValue A T k x ≤ ↑lam

An a.e. finite upper bound on λ_k^gen. For an ergodic measure-preserving T and a possibly-singular generator with log⁺‖A‖ ∈ L¹, there is a finite real constant lam (the forward top value λ₁⁺) with λ_k^gen(x) ≤ lam for μ-a.e. x. Each defining term is ≤ (1/n) log⁺‖A⁽ⁿ⁾‖ (Oseledets.singularSpectralValue_term_le_posLogNorm), whose limsup is the a.e. limit lam of tendsto_top_posLogNorm.

theorem Oseledets.singularSpectralValue_invariant_ae {X : Type u_1} [MeasurableSpace X] {T : X → X} {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] [NeZero d] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (k : ℕ) : singularSpectralValue A T k ∘ T =ᵐ[μ] singularSpectralValue A T k

Integrability-free invariance of λ_k^gen. For an ergodic measure-preserving T and a possibly-singular generator with log⁺‖A‖ ∈ L¹, the genuine per-direction exponent is μ-a.e. T-invariant: λ_k^gen =ᵐ λ_k^gen ∘ T. From the deterministic sub-invariance λ_k^gen ≤ λ_k^gen ∘ T (Oseledets.singularSpectralValue_le_comp), the bounded strictly-monotone transform EReal.exp : EReal → ℝ≥0∞ gives h := exp ∘ λ_k^gen with h ≤ h ∘ T and ∫⁻ h < ∞ (since λ_k^gen ≤ λ₁⁺ a.e., Oseledets.ae_singularSpectralValue_le, and μ is a probability measure). As T is measure-preserving ∫⁻ (h ∘ T) = ∫⁻ h, so h =ᵐ h ∘ T (MeasureTheory.ae_eq_of_ae_le_of_lintegral_le); injectivity of exp lifts back.

theorem Oseledets.ae_singularSpectralValue_eq_const {X : Type u_1} [MeasurableSpace X] {T : X → X} {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] [NeZero d] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (k : ℕ) : ∃ (c : EReal), ∀ᵐ (x : X) ∂μ, singularSpectralValue A T k x = c

The genuine singular Lyapunov spectrum is μ-a.e. constant (det-free). For an ergodic measure-preserving T and a possibly-singular measurable generator with log⁺‖A‖ ∈ L¹ (and no det A ≠ 0, no inverse integrability), the genuine −∞-aware per-direction singular exponent λ_k^gen = Oseledets.singularSpectralValue A T k is μ-a.e. equal to a single constant c : EReal:

∃ c : EReal, ∀ᵐ x ∂μ, singularSpectralValue A T k x = c.

From the integrability-free a.e. T-invariance Oseledets.singularSpectralValue_invariant_ae, the exponent is a.e. constant by ergodicity (Ergodic.ae_eq_const_of_ae_eq_comp₀; EReal is Polish, hence has a countably-separated Borel structure). The value c can be ⊥ on the kernel / volume-collapse stratum — that is the whole point of the genuine −∞-aware exponent.