The Oseledets filtration theorem from the top-gap envelope

This module proves Oseledets.oseledets_filtration_of_topgap: the statement of the Oseledets multiplicative ergodic theorem Oseledets.oseledets_filtration (see Oseledets/MultiplicativeErgodic.lean) with one additional hypothesis, the top-gap fast-band-mass envelope Oseledets.TopGapMassEnvelope, quantified over the deterministic singular-exponent data lam0.

The proof composes the deterministic singular-value exponents, the limit eigenbasis with its eigenpair and slow-orthogonality data, the spectral-identification band projectors, the forward graded-overlap bound (which consumes the envelope), Ruelle's reverse cofactor bound for orthogonal matrices, and the spectrum-identification residuals.

Oseledets.oseledets_filtration follows by discharging the envelope hypothesis with Oseledets.topGapMassEnvelope_ae and treating dimension zero separately.

Main results

• Oseledets.oseledets_filtration_of_topgap: the Oseledets filtration theorem for an ergodic, log-integrable, invertible matrix cocycle, assuming the top-gap fast-band-mass envelope.

References

• D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58.

theorem Oseledets.oseledets_filtration_of_topgap {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero 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)⁻¹) μ) (htopgap : ∀ (lam0 : ℕ → ℝ), (∀ i < d, ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues i)) Filter.atTop (nhds (lam0 i))) → ∀ᵐ (x : X) ∂μ, TopGapMassEnvelope A T lam0 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))

The Oseledets filtration theorem, assuming the top-gap envelope.

The statement of oseledets_filtration with one additional hypothesis htopgap: the top-gap fast-band-mass envelope TopGapMassEnvelope, quantified over the deterministic singular-exponent data lam0.