The inverse (time-reversed) singular-value spectrum

This module is purely additive on top of the spectrum object Oseledets.exponents : Fin d → ℝ (defined in Oseledets/Lyapunov/Spectrum.lean). It records the inverse-matrix-cocycle reciprocity: the singular values of M⁻¹ are the reciprocals, in reversed order, of the singular values of M, and consequently the Lyapunov exponents of the inverse cocycle n ↦ (cocycle A T n x)⁻¹ are the negatives, in reversed order, of the exponents of A.

The honest caveat on "time reversal"

With a one-sided (possibly non-invertible) base map T, this is the inverse-matrix-cocycle statement only: it concerns the matrix inverse (cocycle A T n x)⁻¹ of the forward cocycle iterate, not a genuine two-sided time-reversed cocycle. The genuine time-reversed cocycle cocycle (fun y => (A (T⁻¹ y))⁻¹) T⁻¹ requires T to be invertible (an automorphism) with T⁻¹ measure-preserving; that two-sided development is deferred to the two-sided / backward Oseledets work and is not attempted here. The reciprocity proved here is exactly the matrix-level statement, which is what the existing one-sided machinery supports.

The inverse-integrability hypothesis hint' : IntegrableLogNorm (fun x => (A x)⁻¹) μ (already part of the standing hypotheses) is precisely what makes the inverse spectrum exist: it is the symmetric counterpart of hint that keeps both extremal exponents finite. We note this explicitly because it is the hypothesis carrying the inverse spectrum.

Main results

• Oseledets.singularValues_inv — the SVD reciprocal-reversed identity: for an invertible matrix M, σᵢ(M⁻¹) = (σ_{rev i}(M))⁻¹, where rev is the order reversal on Fin d.
• Oseledets.singularValues_inv_mul — the product form σᵢ(M⁻¹) · σ_{rev i}(M) = 1.
• Oseledets.tendsto_log_singularValue_inv_cocycle — for each sorted index i and μ-a.e. x, the normalized log of the i-th singular value of the inverse cocycle iterate (cocycle A T n x)⁻¹ converges to - exponents … (rev i): the inverse exponents are the negatives in reversed order.
• Oseledets.topExponent_inv_eq_neg_bot — the top exponent of the inverse cocycle equals the negative of the bottom exponent of A, tying the positive and negative ends of the spectrum.

References

• L. Arnold, Random Dynamical Systems, Springer Monographs in Mathematics, 1998.
• D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58.

The eigenvalue reciprocal-reversal lemma (operator level)

The SVD reciprocal-reversed identity (matrix level)

theorem Oseledets.singularValues_inv {d : ℕ} [NeZero d] {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.det ≠ 0) (i : Fin d) : (Matrix.toEuclideanLin M⁻¹).singularValues ↑i = ((Matrix.toEuclideanLin M).singularValues ↑i.rev)⁻¹

The SVD reciprocal-reversed identity. For an invertible matrix M, the singular values of M⁻¹ are the reciprocals, in reversed order, of the singular values of M: σᵢ(M⁻¹) = (σ_{rev i}(M))⁻¹.

The proof routes the squared singular values through the Gram operators: σᵢ(M⁻¹)² is the i-th sorted eigenvalue of (M⁻¹)ᵀ M⁻¹, which is the inverse of M Mᵀ; the eigenvalue reciprocal-reversal lemma identifies this with the reciprocal-reversed eigenvalue of M Mᵀ, and M Mᵀ is cospectral with the Gram matrix Mᵀ M (by Matrix.charpoly_mul_comm), whose (rev i)-th eigenvalue is σ_{rev i}(M)². Taking square roots (all quantities nonnegative) yields the claim.

theorem Oseledets.singularValues_inv_mul {d : ℕ} [NeZero d] {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.det ≠ 0) (i : Fin d) : (Matrix.toEuclideanLin M⁻¹).singularValues ↑i * (Matrix.toEuclideanLin M).singularValues ↑i.rev = 1

The SVD reciprocity, product form. For an invertible matrix M, the i-th singular value of M⁻¹ and the (rev i)-th singular value of M are reciprocal: σᵢ(M⁻¹) · σ_{rev i}(M) = 1.

The inverse cocycle's exponents (cocycle level)

theorem Oseledets.tendsto_log_singularValue_inv_cocycle {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) (i : Fin d) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)⁻¹).singularValues ↑i)) Filter.atTop (nhds (-exponents hT hA hAmeas hint hint' i.rev))

The inverse cocycle's singular-value exponents. For each sorted index i and μ-a.e. x, the normalized log of the i-th singular value of the inverse cocycle iterate (cocycle A T n x)⁻¹ converges to - exponents … (rev i): the Lyapunov exponents of the inverse(-matrix) cocycle are the negatives, in reversed order, of the exponents of A.

This is the singular-value reciprocity singularValues_inv (applied to the invertible iterate cocycle A T n x) combined with exponents_tendsto_log_singularValue. See the module docstring for the honest caveat: with a one-sided base map T this is the inverse-matrix cocycle, not the genuine two-sided time-reversed cocycle.

theorem Oseledets.topExponent_inv_eq_neg_bot {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)⁻¹).singularValues 0)) Filter.atTop (nhds (-exponents hT hA hAmeas hint hint' ⟨d - 1, ⋯⟩))

Positive ↔ negative spectrum bridge. The top exponent of the inverse(-matrix) cocycle equals the negative of the bottom exponent of A: writing λ_bot := exponents … (last index) for the smallest Lyapunov exponent of A, the inverse cocycle's 0-th (largest) exponent is - λ_bot. This ties the bottom of the forward spectrum to the top of the reversed spectrum, complementing the sign characterizations of ExponentSums.