Companion corollaries of the Oseledets theorem

The target theorem Oseledets.oseledets_filtration produces a witness (k, lam, V) of a five-conjunct almost-everywhere block: a strictly decreasing measurable flag ⊤ = V 0 ⊋ ⋯ ⊋ V k = ⊥, equivariance under the cocycle generator, and the exact growth rate lam i on each stratum V i \ V (i+1). This file bundles that conclusion as the predicate Oseledets.IsOseledetsFiltration and derives the standard companion corollaries from the statement alone, quantified over an arbitrary witness:

• canonical characterization: a.e., each level is exactly the sublevel set of the exponential growth rate, so the data (k, lam, V) is unique;
• top exponent: the operator norm of the cocycle grows at the exact rate lam 0, so the top Oseledets exponent is the Furstenberg–Kesten constant;
• multiplicities: for ergodic T the level dimensions are a.e. constant, yielding positive per-exponent multiplicities summing to d.

Only the multiplicity corollary uses ergodicity (an a.e.-invariant measurable ℕ-valued function is a.e. constant); it is also where the MeasurableSubspace conjunct of the main theorem becomes load-bearing, via the trace of the orthogonal projector.

Main results

• Oseledets.IsOseledetsFiltration: the conclusion of the main theorem as a predicate.
• Oseledets.oseledets_filtration': the main theorem repackaged through the predicate.
• Oseledets.IsOseledetsFiltration.ae_mem_iff_limsup_le: a.e., v ∈ V i iff v = 0 or the normalized log-growth of ‖A⁽ⁿ⁾(x) v‖ has limsup ≤ lam i.
• Oseledets.IsOseledetsFiltration.unique: two Oseledets filtration data for the same cocycle have the same k, the same exponents, and a.e. the same subspaces.
• Oseledets.IsOseledetsFiltration.tendsto_log_opNorm_cocycle: (1/n) log ‖A⁽ⁿ⁾(x)‖ → lam 0 a.e.
• Oseledets.oseledets_top_exponent_eq_furstenbergKesten: the top exponent equals any Furstenberg–Kesten constant for the cocycle.
• Oseledets.trace_orthProjMatrix, Oseledets.MeasurableSubspace.measurable_finrank: the dimension of a measurable family of subspaces is measurable.
• Oseledets.IsOseledetsFiltration.exists_finrank_ae_eq: for ergodic T, the level dimensions are a.e. given by a deterministic strictly decreasing profile d = m 0 > ⋯ > m k = 0.
• Oseledets.IsOseledetsFiltration.exists_multiplicity: per-exponent multiplicities, positive and summing to d.
• Oseledets.oseledets_filtration_with_multiplicities: the strengthened existence statement combining the main theorem with the multiplicity profile.

References

• L. Arnold, Random Dynamical Systems, Springer (1998), Theorem 3.4.1.
• M. Viana, Lectures on Lyapunov Exponents, Cambridge University Press (2014), Chapter 4.

theorem Matrix.l2_opNorm_le_sum_norm_basisFun {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) : ‖M‖ ≤ ∑ j : Fin d, ‖(toEuclideanCLM M) ((EuclideanSpace.basisFun (Fin d) ℝ) j)‖

The L2 operator norm of a square matrix is at most the sum of the norms of the images of the standard basis vectors (the "columns") under the induced map on Euclidean space.

The bundled Oseledets predicate

def Oseledets.IsOseledetsFiltration {X : Type u_1} [MeasurableSpace X] {d : ℕ} (μ : MeasureTheory.Measure X) (T : X → X) (A : X → Matrix (Fin d) (Fin d) ℝ) (k : ℕ) (lam : Fin k → ℝ) (V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))) : Prop

The conclusion of oseledets_filtration, bundled as a predicate on a candidate exponent/filtration datum (k, lam, V): the exponents are strictly decreasing, each level is a measurable family of subspaces, and almost every x carries the strictly decreasing A-equivariant flag ⊤ = V 0 ⊋ ⋯ ⊋ V k = ⊥ with exact growth rate lam i on the stratum V i \ V (i+1).

Equations

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

theorem Oseledets.oseledets_filtration' {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X → X} (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)⁻¹) μ) : ∃ (k : ℕ) (lam : Fin k → ℝ) (V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))), IsOseledetsFiltration μ T A k lam V

The Oseledets multiplicative ergodic theorem, repackaged through the bundled predicate IsOseledetsFiltration.

Flag-order helpers

On the a.e. good set, membership in the flag is an initial segment of the index range: every nonzero vector has a well-defined stratum, the last level containing it.

Trace and rank of the orthogonal projector

The MeasurableSubspace conjunct of the main theorem encodes a subspace by its orthogonal-projection matrix; the trace of that matrix is the dimension, which makes x ↦ finrank ℝ (V x) measurable.

theorem Oseledets.trace_orthProjMatrix {d : ℕ} (K : Submodule ℝ (EuclideanSpace ℝ (Fin d))) : (orthProjMatrix K).trace = ↑(Module.finrank ℝ ↥K)

The trace of the orthogonal-projection matrix of a subspace is its dimension.

theorem Oseledets.MeasurableSubspace.measurable_finrank {X : Type u_1} [MeasurableSpace X] {d : ℕ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hV : MeasurableSubspace V) : Measurable fun (x : X) => Module.finrank ℝ ↥(V x)

For a measurable family of subspaces, the dimension is a measurable map to ℕ.

The canonical growth-sublevel characterization (uniqueness, part one)

theorem Oseledets.IsOseledetsFiltration.ae_mem_iff_limsup_le {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} {k : ℕ} {lam : Fin k → ℝ} {V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hV : IsOseledetsFiltration μ T A k lam V) : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin k) (v : EuclideanSpace ℝ (Fin d)), v ∈ V i.castSucc x ↔ v = 0 ∨ Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A T n x)) v‖) Filter.atTop ≤ lam i

Canonical characterization of the Oseledets filtration. Almost everywhere, each level is exactly the sublevel set of the exponential growth rate: v ∈ V i x iff v = 0 or limsup (1/n) log ‖A⁽ⁿ⁾(x) v‖ ≤ lam i. No hypotheses beyond the defining a.e. block are needed.

Uniqueness of the filtration data

theorem Oseledets.IsOseledetsFiltration.unique {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} {k : ℕ} {lam : Fin k → ℝ} {V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] {k₂ : ℕ} {lam₂ : Fin k₂ → ℝ} {V₂ : Fin (k₂ + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hV : IsOseledetsFiltration μ T A k lam V) (hV₂ : IsOseledetsFiltration μ T A k₂ lam₂ V₂) : ∃ (hk : k = k₂), (∀ (i : Fin k), lam i = lam₂ (Fin.cast hk i)) ∧ ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (k + 1)), V i x = V₂ (Fin.cast ⋯ i) x

Uniqueness of the Oseledets data. Two Oseledets filtration data for the same cocycle agree: same number of exponents, same exponents, and a.e. the same subspaces.

The top exponent is the operator-norm growth rate

theorem Oseledets.IsOseledetsFiltration.k_pos {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} {k : ℕ} {lam : Fin k → ℝ} {V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] (hd : 0 < d) (hV : IsOseledetsFiltration μ T A k lam V) : 0 < k

The Oseledets filtration is nontrivial in positive dimension.

theorem Oseledets.IsOseledetsFiltration.tendsto_log_opNorm_cocycle {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} {k : ℕ} {lam : Fin k → ℝ} {V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] (hA : ∀ (x : X), (A x).det ≠ 0) (hV : IsOseledetsFiltration μ T A k lam V) (hk : 0 < k) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖cocycle A T n x‖) Filter.atTop (nhds (lam ⟨0, hk⟩))

The top Lyapunov exponent is the operator-norm growth rate. Almost everywhere, (1/n) log ‖A⁽ⁿ⁾(x)‖ → lam 0: the top stratum gives the lower bound, and the column-sum bound on the L2 operator norm gives the upper bound. Neither ergodicity nor integrability is needed beyond the defining a.e. block.

theorem Oseledets.oseledets_top_exponent_eq_furstenbergKesten {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} {k : ℕ} {lam : Fin k → ℝ} {V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] (hA : ∀ (x : X), (A x).det ≠ 0) (hV : IsOseledetsFiltration μ T A k lam V) (hk : 0 < k) {c : ℝ} (hc : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖cocycle A T n x‖) Filter.atTop (nhds c)) : lam ⟨0, hk⟩ = c

The top Oseledets exponent is the Furstenberg–Kesten constant: any constant to which the normalized log operator norm of the cocycle converges a.e. — such as the one produced by furstenbergKesten_norm — equals lam 0.

Almost-everywhere constant multiplicities

theorem Oseledets.IsOseledetsFiltration.exists_finrank_ae_eq {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} {k : ℕ} {lam : Fin k → ℝ} {V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) (hA : ∀ (x : X), (A x).det ≠ 0) (hV : IsOseledetsFiltration μ T A k lam V) : ∃ (m : Fin (k + 1) → ℕ), StrictAnti m ∧ m 0 = d ∧ m (Fin.last k) = 0 ∧ ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (k + 1)), Module.finrank ℝ ↥(V i x) = m i

A.e.-constant level dimensions. For ergodic T, every Oseledets filtration has a deterministic dimension profile: there is a strictly decreasing m with m 0 = d and m k = 0 such that a.e. finrank ℝ (V i x) = m i. The dimension is measurable via the trace of the orthogonal projector, invariant via equivariance, hence a.e. constant by ergodicity.

theorem Oseledets.IsOseledetsFiltration.exists_multiplicity {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} {k : ℕ} {lam : Fin k → ℝ} {V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) (hA : ∀ (x : X), (A x).det ≠ 0) (hV : IsOseledetsFiltration μ T A k lam V) : ∃ (m : Fin k → ℕ), (∀ (i : Fin k), 0 < m i) ∧ ∑ i : Fin k, m i = d ∧ ∀ᵐ (x : X) ∂μ, ∀ (i : Fin k), Module.finrank ℝ ↥(V i.castSucc x) = Module.finrank ℝ ↥(V i.succ x) + m i

Per-exponent multiplicities. For ergodic T, each exponent lam i of an Oseledets filtration carries a positive multiplicity m i = dim (V i) - dim (V (i+1)), deterministic, with ∑ i, m i = d.

theorem Oseledets.oseledets_filtration_with_multiplicities {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X → X} (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)⁻¹) μ) : ∃ (k : ℕ) (lam : Fin k → ℝ) (V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))) (m : Fin (k + 1) → ℕ), IsOseledetsFiltration μ T A k lam V ∧ StrictAnti m ∧ m 0 = d ∧ m (Fin.last k) = 0 ∧ ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (k + 1)), Module.finrank ℝ ↥(V i x) = m i

The Oseledets theorem with multiplicities: the existence statement of oseledets_filtration strengthened by the deterministic dimension profile of the filtration levels.