The full Lyapunov spectrum as a consumable object

This module packages the deterministic Lyapunov spectrum produced by Oseledets.exists_lam_tendsto_singularValue into a single, directly usable term: the sorted, with-multiplicity exponent vector

exponents A T hT hA hAmeas hint hint' : Fin d → ℝ.

For an ergodic, invertible, log-integrable matrix cocycle (the standing hypotheses hT : Ergodic T μ, hA : ∀ x, (A x).det ≠ 0, hAmeas : Measurable A, hint : IntegrableLogNorm A μ, hint' : IntegrableLogNorm (fun x => (A x)⁻¹) μ, together with [IsProbabilityMeasure μ]), exponents is the antitone Fin d → ℝ whose i-th entry is the deterministic limit of (1/n) log σᵢ(A⁽ⁿ⁾). It is the canonical spectrum object that downstream consumers (exponent sums, the determinant identity, the exterior characterization, …) build on, so all later statements funnel through this one definition.

Main definitions

• Oseledets.exponents — the sorted, with-multiplicity Lyapunov spectrum, as a total Fin d → ℝ, obtained by Classical.choose-ing the lam : ℕ → ℝ of exists_lam_tendsto_singularValue and restricting it to Fin d.
• Oseledets.exponentMultiset — the same data as a Multiset ℝ for multiset-style consumers.
• Oseledets.topExponent — the largest exponent exponents … 0.

Main results

• Oseledets.exponents_antitone — the spectrum is antitone (largest first).
• Oseledets.exponents_tendsto_log_singularValue — for each i, a.e. x, the normalized log of the i-th singular value of A⁽ⁿ⁾ converges to exponents … i.
• Oseledets.exp_exponents_eq_eigenvalues₀_oseledetsLimit — the eigenvalue tie: a.e. x, for every sorted index i, exp (exponents … i) is the i-th sorted eigenvalue of the Oseledets limit Λ x.

References

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

noncomputable def Oseledets.chosenLam {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)⁻¹) μ) : ℕ → ℝ

The chosen deterministic exponent sequence lam : ℕ → ℝ underlying the spectrum, extracted from exists_lam_tendsto_singularValue via Classical.choose. It is antitone on [0, d) and gives the a.e. σ-limits; both properties are recorded as chosenLam_antitone and chosenLam_tendsto. Use exponents (the Fin d → ℝ restriction) as the public object.

Equations

• Oseledets.chosenLam hT hA hAmeas hint hint' = Classical.choose ⋯

theorem Oseledets.chosenLam_spec {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)⁻¹) μ) : (∀ (a b : ℕ), a ≤ b → b < d → chosenLam hT hA hAmeas hint hint' b ≤ chosenLam hT hA hAmeas hint hint' a) ∧ ∀ i < d, ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues i)) Filter.atTop (nhds (chosenLam hT hA hAmeas hint hint' i))

The defining specification of chosenLam: antitonicity on [0, d) and the a.e. per-singular-value σ-limit.

noncomputable def Oseledets.exponents {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)⁻¹) μ) : Fin d → ℝ

The full sorted Lyapunov spectrum, with multiplicity, as a total Fin d → ℝ. Its i-th entry is the deterministic limit of (1/n) log σᵢ(A⁽ⁿ⁾); the entries are sorted in non-increasing order (largest exponent first) and each distinct exponent is repeated according to its multiplicity. This is the canonical spectrum object.

Equations

• Oseledets.exponents hT hA hAmeas hint hint' i = Oseledets.chosenLam hT hA hAmeas hint hint' ↑i

theorem Oseledets.exponents_antitone {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)⁻¹) μ) : Antitone (exponents hT hA hAmeas hint hint')

The spectrum is antitone: exponents lists the Lyapunov exponents in non-increasing order (largest first), counted with multiplicity.

theorem Oseledets.exponents_tendsto_log_singularValue {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))

The defining σ-limit of the spectrum. For each sorted index i and μ-a.e. x, the normalized log of the i-th singular value of the cocycle iterate A⁽ⁿ⁾ converges to exponents … i.

noncomputable def Oseledets.exponentMultiset {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)⁻¹) μ) : Multiset ℝ

The spectrum as a Multiset ℝ, for multiset-style consumers (e.g. counting exponents with multiplicity by membership). It is the image of Finset.univ under exponents.

Equations

• Oseledets.exponentMultiset hT hA hAmeas hint hint' = Multiset.map (Oseledets.exponents hT hA hAmeas hint hint') Finset.univ.val

noncomputable def Oseledets.topExponent {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)⁻¹) μ) : ℝ

The top (largest) Lyapunov exponent, exponents … 0. Requires d ≠ 0 (the index 0 is ⟨0, _⟩ : Fin d), which is available from [NeZero d].

Equations

• Oseledets.topExponent hT hA hAmeas hint hint' = Oseledets.exponents hT hA hAmeas hint hint' ⟨0, ⋯⟩

theorem Oseledets.exp_exponents_eq_eigenvalues₀_oseledetsLimit {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) ∂μ, ∀ (hH : (oseledetsLimit A T x).IsHermitian) (i : Fin (Fintype.card (Fin d))), Real.exp (exponents hT hA hAmeas hint hint' ⟨↑i, ⋯⟩) = hH.eigenvalues₀ i

The eigenvalue tie. For μ-a.e. x and every sorted index i, the exponential of the i-th Lyapunov exponent is the i-th sorted eigenvalue of the Oseledets limit matrix Λ x: exp (exponents … i) = eigenvalues₀ (Λ x) i.

This couples the deterministic spectrum to the (per-point) spectral data of the Oseledets limit, combining oseledetsLimit_eigenvalues₀_eq (eigenvalues of Λ are e^{lamSing}) with the identification lamSing A T x i = exponents … i valid a.e.