Reduction of the continuous-flow MET to the discrete theorem

At integer times the continuous-flow Oseledets multiplicative ergodic theorem reduces to the discrete-time theorem Oseledets.oseledets_filtration'.

The continuous-flow data is a measure-preserving flow φ (Oseledets.MeasurePreservingFlow) and a continuous-time linear cocycle A over it (Oseledets.FlowCocycle). The reduction identity Oseledets.FlowCocycle.toCocycle_eq shows that at integer times the continuous-time cocycle equals the discrete iterated cocycle generated by its time-1 map A 1 over the time-1 flow map φ 1. Hence, once the discrete MET is applied to the generator A 1 and the dynamics φ 1, an Oseledets filtration for the integer-time continuous cocycle is obtained.

The additional ingredient is the integrability of the time-1 log-norms. The discrete theorem requires log⁺ ‖A 1‖ ∈ L¹(μ) and log⁺ ‖(A 1)⁻¹‖ ∈ L¹(μ); these follow from a uniform-on-[0,1] integrable dominating function for the continuous family, which is the natural continuous-flow hypothesis (a continuous-time analogue of the discrete one-sided integrability assumption).

Main results

• Oseledets.integrableLogNorm_timeOne: the time-1 map A 1 has integrable positive log-norm, given an integrable function dominating log⁺ ‖A s‖ uniformly for s ∈ [0,1].
• Oseledets.integrableLogNorm_timeOne_inv: the analogous statement for the inverse (A 1)⁻¹.
• Oseledets.exists_isOseledetsFiltration_timeOne: the discrete MET applied to the time-1 data, yielding an Oseledets filtration for the generator A 1 over the dynamics φ 1.

theorem Oseledets.integrableLogNorm_timeOne {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (A : FlowCocycle φ d) {g : X → ℝ} (hg : MeasureTheory.Integrable g μ) (hgb : ∀ s ∈ Set.Icc 0 1, ∀ (x : X), ‖A.toFun s x‖.posLog ≤ g x) : IntegrableLogNorm (fun (x : X) => A.toFun 1 x) μ

Integrability of the time-1 log-norm. If an integrable function g dominates log⁺ ‖A s‖ uniformly over s ∈ [0,1] (in particular at s = 1), then the time-1 map A 1 of the continuous-time cocycle has integrable positive log-norm, i.e. IntegrableLogNorm (A 1 ·) μ. This is exactly the discrete one-sided integrability hypothesis for the generator A 1.

theorem Oseledets.integrableLogNorm_timeOne_inv {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (A : FlowCocycle φ d) {g' : X → ℝ} (hg' : MeasureTheory.Integrable g' μ) (hg'b : ∀ s ∈ Set.Icc 0 1, ∀ (x : X), ‖(A.toFun s x)⁻¹‖.posLog ≤ g' x) : IntegrableLogNorm (fun (x : X) => (A.toFun 1 x)⁻¹) μ

Integrability of the time-1 inverse log-norm. If an integrable function g' dominates log⁺ ‖(A s)⁻¹‖ uniformly over s ∈ [0,1] (in particular at s = 1), then the inverse (A 1)⁻¹ of the time-1 cocycle map has integrable positive log-norm, i.e. IntegrableLogNorm (fun x => (A 1 x)⁻¹) μ. This is the discrete one-sided integrability hypothesis for the inverse generator.

theorem Oseledets.exists_isOseledetsFiltration_timeOne {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))), IsOseledetsFiltration μ (φ.toFun 1) (fun (x : X) => A.toFun 1 x) k lam V

Reduction of the continuous-flow MET to the discrete theorem at integer times. Applying the discrete Oseledets theorem Oseledets.oseledets_filtration' to the generator A 1 over the ergodic time-1 dynamics φ 1 yields an Oseledets filtration for the time-1 cocycle map. Combined with the reduction identity Oseledets.FlowCocycle.toCocycle_eq (which identifies the integer-time continuous cocycle with the discrete iterated cocycle of A 1 over φ 1), this gives the integer-time behaviour of the continuous-flow cocycle.

The integrability hypotheses are stated as integrable dominating functions for the continuous family log⁺ ‖A s‖ (resp. log⁺ ‖(A s)⁻¹‖) uniformly over s ∈ [0,1].