The top singular exponent γ_d and the genuine log|det| growth

This module completes the k = d (volume) end of the cumulative forward singular exponent family γ_k (Oseledets.forwardSingularExponent): it ties the top cumulative EReal exponent γ_d — and the forward top-d value Γ_d⁺ — to the genuine (not log⁺) determinant growth (1/n) log|det(A⁽ⁿ⁾ x)|, staying entirely inside the singular (forward-only) track.

The crux is that, at the top index, the singular-value product collapses to the absolute determinant, sprod A T d n x = |det(A⁽ⁿ⁾ x)| (Oseledets.sprod_d_eq_abs_det). Rewriting the top-k results of Oseledets/Lyapunov/Extensions/Singular.lean through this identity converts their log sprod_d statements into statements about log|det(A⁽ⁿ⁾)|:

• the a.e.-constant value: γ_d(x) = (Γ_d⁺ : EReal) μ-a.e. (k = d instance of Oseledets.ae_forwardSingularExponent_eq_coe);
• the genuine growth, when Γ_d⁺ > 0: limsup ((1/n) log|det(A⁽ⁿ⁾)| : EReal) = (Γ_d⁺ : EReal) μ-a.e. (k = d instance of Oseledets.limsup_logSprod_eq_top_of_pos, rewritten by sprod_d_eq_abs_det).

Main results

• Oseledets.ae_forwardSingularExponent_full_eq_coe — γ_d = (Γ_d⁺ : EReal) μ-a.e. (the top-index value, forward-only hypotheses).
• Oseledets.ae_forwardSingularExponent_full_eq_det_growth — the headline: a single forward top-d constant Γ_d⁺ is the μ-a.e. value of γ_d, and, whenever Γ_d⁺ > 0, also the exact EReal-limsup of the genuine normalized log|det(A⁽ⁿ⁾)|.

Implementation notes

• Everything here uses only the forward hypotheses [IsProbabilityMeasure μ], [NeZero d], Ergodic T μ, Measurable A, IntegrableLogNorm A μ (log⁺‖A‖ ∈ L¹). There is no call to the invertible additive Oseledets/Lyapunov/Extensions/DetIdentity.lean track: its genuine (1/n) log|det(A⁽ⁿ⁾)| → ∑ exponents requires det A ≠ 0, inverse integrability log⁺‖A⁻¹‖ ∈ L¹, and Oseledets filtration data, which the singular track does not assume. The EReal/limsup packaging here is the contraction-robust replacement.
• The positivity hypothesis Γ_d⁺ > 0 (the expanding-volume regime) is essential for the genuine log|det| identification: only then does the convergent log⁺ form agree eventually with the genuine log. When Γ_d⁺ = 0 (volume contraction, |det(A⁽ⁿ⁾)| → 0, genuine growth → −∞) the EReal-limsup of the genuine log|det| can fall strictly below Γ_d⁺, so only the ≤ form (Oseledets.limsup_logSprod_le_top rewritten through sprod_d_eq_abs_det) survives there; it is not folded in here.

References

• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).
• D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58.

theorem Oseledets.ae_forwardSingularExponent_full_eq_coe {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 μ) : ∃ (gam : ℝ), ∀ᵐ (x : X) ∂μ, forwardSingularExponent A T d x = ↑gam

γ_d is μ-a.e. a real constant Γ_d⁺ (the top-index value). The k = d instance of Oseledets.ae_forwardSingularExponent_eq_coe: for an ergodic measure-preserving T and a possibly-singular measurable generator with log⁺‖A‖ ∈ L¹, there is a real Γ_d⁺ with γ_d(x) = (Γ_d⁺ : EReal) for μ-a.e. x. No invertibility, no inverse integrability.

theorem Oseledets.ae_forwardSingularExponent_full_eq_det_growth {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 μ) : ∃ (gam : ℝ), (∀ᵐ (x : X) ∂μ, forwardSingularExponent A T d x = ↑gam) ∧ (0 < gam → ∀ᵐ (x : X) ∂μ, Filter.limsup (fun (n : ℕ) => ↑((↑n)⁻¹ * Real.log |(cocycle A T n x).det|)) Filter.atTop = ↑gam)

γ_d and the genuine log|det| growth (the headline). For an ergodic measure-preserving T and a possibly-singular measurable generator with log⁺‖A‖ ∈ L¹ (no det A ≠ 0, no inverse integrability), there is a single forward top-d constant Γ_d⁺ such that:

• γ_d(x) = (Γ_d⁺ : EReal) for μ-a.e. x (the cumulative top singular exponent is a.e. this constant), and
• whenever Γ_d⁺ > 0, for μ-a.e. x limsup (fun n => ((1/n) log|det(A⁽ⁿ⁾ x)| : EReal)) = (Γ_d⁺ : EReal), i.e. the genuine (not log⁺) normalized log absolute determinant has EReal-limsup exactly Γ_d⁺.

Proof: instantiate Oseledets.limsup_logSprod_eq_top_of_pos at k = d, which provides the constant Γ_d⁺ together with the a.e. limit of (1/n) log⁺ sprod_d and the positive-regime genuine limsup identity for log sprod_d. The value clause comes from that limit through forwardSingularExponent (mirroring ae_forwardSingularExponent_eq_coe); the growth clause is the genuine limsup rewritten by sprod_d_eq_abs_det (sprod_d = |det|). The positivity hypothesis is essential — in the contracting case Γ_d⁺ = 0 the genuine log|det| may tend to −∞, so its limsup can be strictly below Γ_d⁺.