The continuous-flow Oseledets multiplicative ergodic theorem

This file contains the continuous-flow Oseledets multiplicative ergodic theorem (MET): Oseledets.oseledets_flow. It is the continuous-time analogue of the discrete-time target Oseledets.oseledets_filtration, stated over a measure-preserving one-parameter flow φ (Oseledets.MeasurePreservingFlow) and a continuous-time linear cocycle A (Oseledets.FlowCocycle).

The proof combines four continuous-flow ingredients:

• Reduction (Oseledets.exists_isOseledetsFiltration_timeOne): the discrete MET applied to the generator A 1 over the ergodic time-1 dynamics φ 1 produces an Oseledets filtration for the time-1 cocycle map. This yields the dimension k, the exponents lam, the measurable subspace family V, the strictly decreasing flag, and the integer-time growth rates.
• Equivariance (Oseledets.ae_flow_equivariant): for every fixed time t₀, the time-t₀ cocycle map sends each level of the filtration at x onto the corresponding level at φ t₀ x, almost everywhere. This upgrades the discrete (time-1) equivariance to the full continuous flow.
• Error sublinearity (Oseledets.ae_tendsto_flowError_zero): the integrable controls fluctuate sublinearly along the integer orbit of the flow, almost everywhere.
• Between-times limit (Oseledets.tendsto_log_norm_atTop_of_discrete): the integer-time growth rate of a vector forces the continuous-time growth rate t⁻¹ log ‖A t x v‖ to the same limit as t → ∞.

Main statements

• Oseledets.oseledets_flow: the continuous-flow Oseledets MET. For an ergodic (at time 1) measure-preserving flow φ on a probability space and a continuous-time linear cocycle A whose one-step log-norms are dominated uniformly on [0,1] by integrable functions, almost every point carries a strictly decreasing, fully flow-equivariant Oseledets flag whose strata realise the exponents lam i as continuous-time growth rates.

References

• V. I. Oseledets, A multiplicative ergodic theorem. Lyapunov characteristic numbers for dynamical systems, Trans. Moscow Math. Soc. 19 (1968), 197–231.
• L. Arnold, Random Dynamical Systems, Springer Monographs in Mathematics, 1998.

theorem Oseledets.oseledets_flow {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] (φ : MeasurePreservingFlow μ) (herg : Ergodic (φ.toFun 1) μ) (A : FlowCocycle φ d) (g g' : X → ℝ) (hg : MeasureTheory.Integrable g μ) (hg' : MeasureTheory.Integrable g' μ) (hgb : ∀ s ∈ Set.Icc 0 1, ∀ (x : X), ‖A.toFun s x‖.posLog ≤ g x) (hg'b : ∀ s ∈ Set.Icc 0 1, ∀ (x : X), ‖(A.toFun s x)⁻¹‖.posLog ≤ g' 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) ∧ (∀ (t : ℝ), ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (k + 1)), Submodule.map (↑(Matrix.toEuclideanCLM (A.toFun t x))) (V i x) = V i (φ.toFun t 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), ∀ v ∈ ↑(V i.castSucc x), v ∉ V i.succ x → Filter.Tendsto (fun (t : ℝ) => t⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (A.toFun t x)) v‖) Filter.atTop (nhds (lam i))

The continuous-flow Oseledets multiplicative ergodic theorem.

Let μ be a probability measure on X, let φ be a measure-preserving one-parameter flow whose time-1 map is μ-ergodic, and let A be a continuous-time linear cocycle over φ valued in invertible d × d real matrices. Assume the one-step log-norms are controlled uniformly on [0,1] by integrable functions: log⁺ ‖A s x‖ ≤ g x and log⁺ ‖(A s x)⁻¹‖ ≤ g' x for all s ∈ [0,1] and x, with g, g' ∈ L¹(μ).

Then there is a finite Oseledets spectrum: a number k of distinct Lyapunov exponents lam : Fin k → ℝ (strictly decreasing) and a measurable family of nested subspaces V : Fin (k+1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d)) such that:

• the exponents are strictly decreasing;
• each level V i is a measurable family of subspaces;
• (full flow equivariance) for every time t, almost every x has each level mapped by the time-t cocycle onto the level at the flowed point: A t x · V i x = V i (φ t x);
• almost every x carries the strictly decreasing flag ⊤ = V 0 x ⊋ ⋯ ⊋ V k x = ⊥, and on each stratum V i \ V (i+1) the continuous-time growth rate is exactly lam i: t⁻¹ log ‖A t x v‖ → lam i as t → ∞.