The Oseledets multiplicative ergodic theorem (one-sided, filtration form)

The main theorem of the development, drawing on Oseledets/Ergodic/, Oseledets/Cocycle/, and Oseledets/Lyapunov/.

Main statements

For an ergodic measure-preserving T on a probability space and a measurable matrix cocycle generator A : X → GL(d, ℝ) (encoded as A x : Matrix (Fin d) (Fin d) ℝ with det (A x) ≠ 0) satisfying the one-sided integrability log⁺‖A‖, log⁺‖A⁻¹‖ ∈ L¹(μ), there exist finitely many distinct Lyapunov exponents λ₁ > ⋯ > λ_k and, for μ-a.e. x, a strictly decreasing, A-equivariant, measurable filtration of EuclideanSpace ℝ (Fin d) along which the cocycle grows at the exact rate λᵢ: (1/n) log‖A⁽ⁿ⁾(x) v‖ → λᵢ for v ∈ Vⁱₓ ∖ V^{i+1}ₓ.

The matrices act on EuclideanSpace ℝ (Fin d) via Matrix.toEuclideanCLM, so all norms are the L2 norm and the matrix operator norm is submultiplicative.

References

• V. I. Oseledets, A multiplicative ergodic theorem. Lyapunov characteristic numbers for dynamical systems, Trans. Moscow Math. Soc. 19 (1968), 197–231.
• D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979).
• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

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))), StrictAnti lam ∧ (∀ (i : Fin (k + 1)), MeasurableSubspace fun (x : X) => V i x) ∧ ∀ᵐ (x : X) ∂μ, V 0 x = ⊤ ∧ V (Fin.last k) x = ⊥ ∧ (∀ (i : Fin k), V i.succ x < V i.castSucc x) ∧ (∀ (i : Fin (k + 1)), Submodule.map (↑(Matrix.toEuclideanCLM (A x))) (V i x) = V i (T x)) ∧ ∀ (i : Fin k), ∀ v ∈ ↑(V i.castSucc x), v ∉ V i.succ x → Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A T n x)) v‖) Filter.atTop (nhds (lam i))

Oseledets multiplicative ergodic theorem (one-sided, filtration form).

Let μ be a probability measure, T : X → X ergodic measure-preserving, and A : X → Matrix (Fin d) (Fin d) ℝ a measurable cocycle generator with det (A x) ≠ 0 and log⁺‖A‖, log⁺‖A⁻¹‖ ∈ L¹(μ). Then there are k distinct Lyapunov exponents lam : Fin k → ℝ (strictly decreasing) and a measurable family of subspaces V : Fin (k+1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d)) forming, μ-a.e., a strictly decreasing A-equivariant flag ⊤ = V 0 ⊋ ⋯ ⊋ V k = ⊥ along which (1/n) log‖A⁽ⁿ⁾(x) v‖ → lam i for every v ∈ V iₓ ∖ V (i+1)ₓ.