Lyapunov exponents of a constant cocycle

For a constant generator A ≡ M the iterated cocycle is just the matrix power, cocycle (fun _ => M) T n x = Mⁿ, and the whole Oseledets apparatus collapses to ordinary linear algebra. This module records that collapse and, for a symmetric (real Hermitian) generator M, identifies the Lyapunov spectrum with the log-moduli of the eigenvalues of M.

The geometric content is the polar/singular-value picture of a symmetric matrix: the Oseledets limit Λ x = lim_n (Qₙ)^{1/(2n)} of the constant cocycle is, for every x, the absolute value |M| = cfc |·| M, whose sorted eigenvalues are the moduli |λᵢ(M)| sorted in non-increasing order. Feeding this through the eigenvalue tie Oseledets.exp_exponents_eq_eigenvalues₀_oseledetsLimit gives exp (exponents … i) = |M|'s i-th sorted eigenvalue, hence exponents … i = log of the i-th largest modulus.

Main definitions

• Oseledets.absMatrix — the absolute value |M| = cfc |·| M of a (real) matrix, the Oseledets limit of the constant symmetric cocycle.

Main results

• Oseledets.cocycle_const — cocycle (fun _ => M) T n x = Mⁿ for an arbitrary generator M.
• Oseledets.gram_const, Oseledets.qpow_const, Oseledets.oseledetsLimit_const — for symmetric M, the Gram matrix is M^{2n}, the approximant qpow is |M| for every n ≥ 1, and the Oseledets limit is |M|.
• Oseledets.exp_exponents_const_eq_eigenvalues₀_absMatrix — for symmetric invertible M, exp (exponents (fun _ => M) … i) = |M|'s i-th sorted eigenvalue.
• Oseledets.exponents_const — for symmetric invertible M, exponents (fun _ => M) … i = Real.log (|M|.eigenvalues₀ i), i.e. the log of the i-th largest modulus of an eigenvalue of M.

References

• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

The constant cocycle is the matrix power

theorem Oseledets.cocycle_const {X : Type u_1} [MeasurableSpace X] {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) : cocycle (fun (x : X) => M) T n x = M ^ n

The constant cocycle is the matrix power. For a constant generator A ≡ M, the iterated cocycle is cocycle (fun _ => M) T n x = Mⁿ, independent of the base point and the dynamics.

The Gram matrix and qpow of a symmetric constant cocycle

theorem Oseledets.gram_const {X : Type u_1} [MeasurableSpace X] {d : ℕ} {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.transpose = M) (T : X → X) (n : ℕ) (x : X) : gram (fun (x : X) => M) T n x = M ^ (2 * n)

For a symmetric constant generator M (hM : Mᵀ = M), the Gram matrix of the constant cocycle is the even power gram (fun _ => M) T n x = M^{2n}: indeed (Mⁿ)ᵀ Mⁿ = (Mᵀ)ⁿ Mⁿ = Mⁿ Mⁿ = M^{n+n}.

noncomputable def Oseledets.absMatrix {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) : Matrix (Fin d) (Fin d) ℝ

The absolute value of a real matrix, |M| = cfc |·| M, defined through the continuous functional calculus. For a symmetric M it is positive semidefinite with eigenvalues the moduli |λᵢ(M)|, and it is the Oseledets limit of the constant cocycle generated by M (oseledetsLimit_const).

Equations

• Oseledets.absMatrix M = cfc (fun (t : ℝ) => |t|) M

theorem Oseledets.absMatrix_isSelfAdjoint {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) : IsSelfAdjoint (absMatrix M)

|M| = cfc |·| M is self-adjoint (a real-valued continuous functional calculus is always self-adjoint), hence Hermitian.

theorem Oseledets.absMatrix_isHermitian {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) : (absMatrix M).IsHermitian

|M| = cfc |·| M is Hermitian.

theorem Oseledets.qpow_const {X : Type u_1} [MeasurableSpace X] {d : ℕ} {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.transpose = M) (T : X → X) {n : ℕ} (hn : 1 ≤ n) (x : X) : qpow (fun (x : X) => M) T n x = absMatrix M

For a symmetric generator M and every n ≥ 1, the Oseledets approximant of the constant cocycle is the absolute value qpow (fun _ => M) T n x = |M|.

The Gram matrix is M^{2n} (gram_const), so qpow = cfc (·^{1/(2n)}) (M^{2n}). Pulling the (2n)-th power inside the calculus (cfc_comp_pow) turns this into cfc (fun t => (t^{2n})^{1/(2n)}) M, and (t^{2n})^{1/(2n)} = |t| for every real t (even power, then rpow cancellation), so the calculus reduces to cfc |·| M = |M|.

The Oseledets limit of a symmetric constant cocycle is |M|

theorem Oseledets.oseledetsLimit_const {X : Type u_1} [MeasurableSpace X] {d : ℕ} {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.transpose = M) (T : X → X) (x : X) : oseledetsLimit (fun (x : X) => M) T x = absMatrix M

For a symmetric generator M, the Oseledets limit of the constant cocycle is, for every base point, the absolute value oseledetsLimit (fun _ => M) T x = |M|. The approximants qpow (fun _ => M) T n x are equal to |M| for every n ≥ 1 (qpow_const), so each entry of the limit (limUnder of an eventually-constant sequence) is the corresponding entry of |M|.

The Lyapunov spectrum of a symmetric constant cocycle

We now fix an ergodic, probability-preserving system (X, μ, T) and an invertible symmetric generator M, and discharge the standing spectrum hypotheses for the constant cocycle A := fun _ => M.

theorem Oseledets.const_det_ne_zero {X : Type u_1} [MeasurableSpace X] {d : ℕ} {M : Matrix (Fin d) (Fin d) ℝ} (hdet : M.det ≠ 0) (x : X) : ((fun (x : X) => M) x).det ≠ 0

The invertibility hypothesis ∀ x, (A x).det ≠ 0 for the constant cocycle, from M.det ≠ 0.

theorem Oseledets.const_measurable {X : Type u_1} [MeasurableSpace X] {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) : Measurable fun (x : X) => M

The measurability hypothesis for the constant cocycle: a constant map is measurable.

theorem Oseledets.const_integrableLogNorm {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] (M : Matrix (Fin d) (Fin d) ℝ) : IntegrableLogNorm (fun (x : X) => M) μ

The log-integrability hypothesis IntegrableLogNorm A μ for the constant cocycle: log⁺‖M‖ is a constant, integrable over a finite (probability) measure.

theorem Oseledets.const_integrableLogNorm_inv {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] (M : Matrix (Fin d) (Fin d) ℝ) : IntegrableLogNorm (fun (x : X) => ((fun (x : X) => M) x)⁻¹) μ

The inverse log-integrability hypothesis for the constant cocycle: log⁺‖M⁻¹‖ is a constant, integrable over a finite (probability) measure.

theorem Oseledets.exp_exponents_const_eq_eigenvalues₀_absMatrix {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.transpose = M) (hdet : M.det ≠ 0) [NeZero d] (i : Fin (Fintype.card (Fin d))) : Real.exp (exponents hT ⋯ ⋯ ⋯ ⋯ ⟨↑i, ⋯⟩) = ⋯.eigenvalues₀ i

The eigenvalue tie for a symmetric constant cocycle. For symmetric invertible M, the exponential of the i-th Lyapunov exponent of the constant cocycle is the i-th sorted eigenvalue of the absolute value |M|: exp (exponents (fun _ => M) … i) = |M|.eigenvalues₀ i.

This specializes exp_exponents_eq_eigenvalues₀_oseledetsLimit using oseledetsLimit (fun _ => M) T x = |M|. Both sides are independent of the base point, so the a.e. statement is upgraded to a genuine ∀ i by extracting a single point (the probability measure has a nonempty a.e.-filter).

theorem Oseledets.exponents_const {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.transpose = M) (hdet : M.det ≠ 0) [NeZero d] (i : Fin (Fintype.card (Fin d))) : exponents hT ⋯ ⋯ ⋯ ⋯ ⟨↑i, ⋯⟩ = Real.log (⋯.eigenvalues₀ i)

The Lyapunov spectrum of a symmetric constant cocycle. For symmetric invertible M, the i-th Lyapunov exponent of the constant cocycle is log of the i-th sorted eigenvalue of |M|, i.e. the log of the i-th largest modulus |λ(M)| of an eigenvalue of M. Obtained by taking Real.log of the positive eigenvalue tie exp_exponents_const_eq_eigenvalues₀_absMatrix.