The genuine per-direction singular Lyapunov exponent λ_k^gen (EReal-valued, antitone)

For a possibly-singular matrix cocycle generator A : X → Matrix (Fin d) (Fin d) ℝ — no det A ≠ 0, no inverse integrability — this module builds the genuine (−∞-aware) per-direction forward singular Lyapunov exponent and proves it is antitone in the direction index, the gap datum that the intermediate filtration needs in order to choose its cut thresholds.

The log⁺ per-direction exponent of Oseledets/Lyapunov/Extensions/SingularPerDirectionExponent.lean (Oseledets.singularDirExponent) is NOT antitone — the positive-part clamp log⁺ resets the cumulative volume to 0 once it turns non-positive, so its increments jump back up (see that module's docstring for the explicit λ^gen = (1, −½, −½, −½) counterexample). The antitone ordering lives on the genuine logarithm. We capture it here with the −∞-valued ENNReal.log of the k-th singular value σ_k(A⁽ⁿ⁾) (zero-indexed, so σ_0 ≥ σ_1 ≥ …):

λ_k^gen(x) = limsup_n ((1/n : EReal) · log σ_k(A⁽ⁿ⁾ x)),

with log 0 = ⊥ (the collapse −∞ exponent). Because the singular values are antitone in k (LinearMap.singularValues_antitone) and ENNReal.log is monotone (ENNReal.log_monotone), the per-direction exponents are deterministically antitone — λ_{k+1}^gen(x) ≤ λ_k^gen(x) for every x, with no invertibility, integrability, or ergodicity hypothesis. This is exactly the property the log⁺ packaging lacks and the reason the genuine log is used.

Main definitions

• Oseledets.singularSpectralValue — the genuine per-direction forward singular exponent λ_k^gen, the EReal-valued limsup of (1/n) log σ_k(A⁽ⁿ⁾) (with log 0 = ⊥). It can equal ⊥ on the collapse / kernel stratum.

Main results

• Oseledets.singularSpectralValue_antitone — the headline: λ_k^gen is antitone in k for every x (deterministic), since the singular values are antitone and ENNReal.log is monotone.
• Oseledets.singularSpectralValue_le_genLog_sub / Oseledets.singularSpectralValue_succ_telescope — the telescoping tie to the cumulative genuine-log exponent Oseledets.forwardSingularExponentLog: where the top-k volume is positive, the per-direction exponent is the cumulative increment γ_{k+1}^log − γ_k^log.

Implementation notes

• The −∞-aware ENNReal.log : ℝ≥0∞ → EReal (log 0 = ⊥, log monotone) is the right logarithm here: with the plain Real.log (where Real.log 0 = 0 by convention) the per-direction exponents would not be antitone, because a collapsed singular value σ = 0 would read as log 0 = 0 rather than the genuine −∞. So the antitone ordering is genuinely an ENNReal.log phenomenon.
• Everything in the antitone core is deterministic (holds for every x); no det A ≠ 0, no log⁺‖A⁻¹‖ ∈ L¹, no ergodicity. The invertible analogues (Oseledets.exponents in Oseledets/Lyapunov/Extensions/Spectrum.lean, with their det ≠ 0 and inverse-integrability hypotheses) are deliberately not reused.

References

• A. Quas, Multiplicative Ergodic Theorems and Applications (Theorem 2, §3.1; SVD + exterior algebra + Kingman, Raghunathan's method).
• M. S. Raghunathan, A proof of Oseledec's multiplicative ergodic theorem, Israel J. Math. 32 (1979), 356–362.
• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

noncomputable def Oseledets.singularSpectralValue {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (k : ℕ) (x : X) : EReal

The genuine per-direction forward singular exponent λ_k^gen of a possibly-singular cocycle generator, as an EReal-valued limsup built from the −∞-aware logarithm ENNReal.log:

λ_k^gen(x) = limsup_n ((1/n : EReal) · log σ_k(A⁽ⁿ⁾ x)),

where σ_k(A⁽ⁿ⁾) = (toEuclideanLin (cocycle A T n x)).singularValues k is the k-th singular value (zero-indexed, non-increasing) and log = ENNReal.log (so a collapsed singular value σ_k = 0 reads as the genuine ⊥ = −∞, not the Real.log 0 = 0 junk). Unlike the log⁺ per-direction exponent Oseledets.singularDirExponent, this genuine version is antitone in k.

Equations

• One or more equations did not get rendered due to their size.

theorem Oseledets.singularSpectralValue_antitone {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) : Antitone fun (k : ℕ) => singularSpectralValue A T k x

The headline: λ_k^gen is antitone in k, deterministically. For every x (no invertibility, no integrability, no ergodicity), λ_{k+1}^gen(x) ≤ λ_k^gen(x). The singular values are antitone in the index (LinearMap.singularValues_antitone), ENNReal.ofReal is monotone, and the −∞-aware logarithm ENNReal.log is monotone (ENNReal.log_monotone), so each term (1/n) log σ_{k+1} ≤ (1/n) log σ_k (the factor (n : ℝ)⁻¹ ≥ 0); the EReal-limsup is monotone, giving the bound. This is precisely the antitone ordering the log⁺ packaging (Oseledets.singularDirExponent) lacks, and the gap datum the cut-threshold layer needs.

Telescoping tie to the cumulative genuine-log volume and measurability

theorem Oseledets.log_singularValue_eq_sub_sprod {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 x)).singularValues k)).log = (ENNReal.ofReal (sprod A T (k + 1) n x)).log - (ENNReal.ofReal (sprod A T k n x)).log

The genuine −∞-aware log of the k-th singular value is a measurable telescoping difference of cumulative log-volumes. For every n and x,

log σ_k(A⁽ⁿ⁾) = log (ofReal sprod_{k+1}) − log (ofReal sprod_k) (in EReal, log = ENNReal.log).

When sprod_k > 0, the factorization sprod_{k+1} = sprod_k · σ_k (Finset.prod_range_succ) and the unconditional additivity ENNReal.log_mul_add give log (ofReal sprod_{k+1}) = log (ofReal sprod_k) + log σ_k, and the (finite) log (ofReal sprod_k) cancels (EReal.add_sub_cancel_left). When sprod_k = 0, antitonicity of the singular values forces σ_k = 0, so the left side is ⊥, while the right side is ⊥ − ⊥ = ⊥ (EReal.bot_sub), so the identity holds there too. This expresses the per-direction term through the measurable sprod (Oseledets.measurable_sprod), sidestepping the absence of a direct singular-value measurability lemma.

theorem Oseledets.measurable_singularSpectralValue {X : Type u_1} [MeasurableSpace X] {T : X → X} {d : ℕ} [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (hAmeas : Measurable A) (hTmeas : Measurable T) (k : ℕ) : Measurable (singularSpectralValue A T k)

The per-direction exponent λ_k^gen is measurable. Via the telescoping identity log σ_k = log (ofReal sprod_{k+1}) − log (ofReal sprod_k) (Oseledets.log_singularValue_eq_sub_sprod), each defining term is the scalar multiple of a measurable EReal-difference: sprod is measurable (Oseledets.measurable_sprod, [NeZero d]), ENNReal.ofReal is measurable (ENNReal.measurable_ofReal), ENNReal.log is measurable (ENNReal.measurable_log), and EReal subtraction/scalar multiplication preserve measurability. The ℕ-limsup of measurable EReal-valued functions is measurable (Measurable.limsup).

theorem Oseledets.singularSpectralValue_term_le_posLogNorm {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (k n : ℕ) (x : X) : (↑↑n)⁻¹ * (ENNReal.ofReal ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues k)).log ≤ ↑((↑n)⁻¹ * ‖cocycle A T n x‖.posLog)

Each term of λ_k^gen is bounded above by (1/n) log⁺‖A⁽ⁿ⁾‖. Deterministically, for every n and x, (1/n) · log σ_k(A⁽ⁿ⁾) ≤ ((1/n) log⁺‖A⁽ⁿ⁾‖ : EReal). If σ_k = 0 the left side is ⊥; otherwise σ_k ≤ ‖A⁽ⁿ⁾‖ (Oseledets.sigma_le_opNorm) gives log σ_k ≤ log ‖A⁽ⁿ⁾‖ ≤ log⁺‖A⁽ⁿ⁾‖, and the factor (n : ℝ)⁻¹ ≥ 0 preserves the bound.

theorem Oseledets.ae_singularSpectralValue_lt_top {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 : ℕ) : ∀ᵐ (x : X) ∂μ, singularSpectralValue A T k x < ⊤

λ_k^gen < ⊤ μ-a.e. (the genuine per-direction exponent is a.e. finite above). For an ergodic measure-preserving T and a possibly-singular generator with log⁺‖A‖ ∈ L¹, each defining term is ≤ (1/n) log⁺‖A⁽ⁿ⁾‖ (Oseledets.singularSpectralValue_term_le_posLogNorm), and the latter converges μ-a.e. to the finite forward top value λ₁⁺ (Oseledets.tendsto_top_posLogNorm). So the EReal-limsup defining λ_k^gen is ≤ (λ₁⁺ : EReal) < ⊤. (The lower side can reach ⊥ on the collapse stratum, so no a.e. ⊥ < λ_k^gen companion is claimed — that is the whole point of the genuine −∞-aware exponent.)

Cut thresholds between consecutive distinct finite exponents

The intermediate singular filtration is built by feeding the Gram-sublevel projector Oseledets.cocycleSublevelEuclid a squared-singular-value threshold t strictly between the growth rates of two consecutive distinct exponents. A singular direction with per-direction exponent λ has singular value σ ≈ e^{nλ}, hence Gram eigenvalue σ² ≈ e^{2nλ}. So to separate the exponent λ_{j+1} (below) from λ_j (above) the threshold must satisfy e^{2 λ_{j+1}} < t_j < e^{2 λ_j}. This section constructs such thresholds from the a.e.-constant distinct finite exponent vector (the strictly-antitone list of distinct values), which is the gap datum the cut layer consumes. It is pure real analysis (Real.exp strict monotone + exists_between), with no cocycle, measure, or invertibility hypothesis.

theorem Oseledets.exists_cutThreshold {a b : ℝ} (hab : a < b) : ∃ (t : ℝ), Real.exp (2 * a) < t ∧ t < Real.exp (2 * b)

A cut threshold strictly between two consecutive distinct exponents. Given finite exponents a < b (so b is the larger, "faster" exponent), there is a squared-singular-value threshold t with Real.exp (2 * a) < t < Real.exp (2 * b): the Gram-eigenvalue scale strictly separates the two growth rates. Obtained from strict monotonicity of Real.exp and density of ℝ (exists_between).

theorem Oseledets.exists_cutThresholds {r : ℕ} (lam : Fin (r + 1) → ℝ) (hlam : StrictAnti lam) : ∃ (t : Fin r → ℝ), ∀ (j : Fin r), Real.exp (2 * lam j.succ) < t j ∧ t j < Real.exp (2 * lam j.castSucc)

The full ladder of cut thresholds for a strictly-antitone finite exponent vector. Given the distinct exponents lam : Fin (r + 1) → ℝ sorted strictly decreasingly (largest first; lam is the a.e.-constant list of distinct finite singular exponents, kernel/−∞ directions excluded), there is a threshold vector t : Fin r → ℝ placing, for each consecutive pair, a squared-singular-value cut strictly between the two growth rates:

Real.exp (2 · lam (j+1)) < t j < Real.exp (2 · lam j).

These are exactly the thresholds to feed Oseledets.cocycleSublevelEuclid so that its ≤ t_j Gram-sublevel space captures the directions with exponent ≤ lam (j+1) (the slow part below the j-th gap). Built by choosing each cut independently with Oseledets.exists_cutThreshold on the strict gap lam (j.succ) < lam (j.castSucc). No measure-theoretic or invertibility hypothesis.