The Oseledets filtration from the spectral-identification hypothesis

This file proves a variant of Oseledets.oseledets_filtration_of_upper in which the band-projector convergence hypothesis hband is replaced by the spectral-identification hypothesis hident, and the lower-bound step hlb is accordingly obtained from specList_le_liminf_inv_mul_log_norm_cocycle_apply_of_slowflag (fed hident and the slow-flag datum hslowflag computed earlier in the proof) instead of specList_le_liminf_inv_mul_log_norm_cocycle_apply_of_bandProjector.

Main results

• Oseledets.oseledets_filtration_of_upper': the Oseledets filtration theorem, conditional on the a.e. spectral upper bound over the slow flag, the reverse slow-flag inclusion, the two spectrum inclusions, and the spectral-identification band-projector limit.

theorem Oseledets.oseledets_filtration_of_upper' {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X → X} (hT : Ergodic T μ) (hTmeas : Measurable 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)⁻¹) μ) (hupper : ∀ᵐ (x : X) ∂μ, ∀ (t : ℝ), ∀ v ∈ vslow A T (Real.exp t) x, v ≠ 0 → Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) Filter.atTop ≤ t) (hslowrev : ∀ᵐ (x : X) ∂μ, ∀ (t : ℝ), lambdaSublevel A T x t ≤ vslow A T (Real.exp t) x) (hub_spec : ∀ (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) ∂μ, lyapunovSpectrum A T x ⊆ distinctExp lam0 d) (hlb_spec : ∀ (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) ∂μ, distinctExp lam0 d ⊆ lyapunovSpectrum A T x) (hident : ∀ᵐ (x : X) ∂μ, ∀ (c : ℝ), 0 < c → (∀ (i : Fin d), Real.exp (lamSing A T x ↑i) ≠ c) → Filter.Tendsto (fun (n : ℕ) => bandProjector A T ((Set.Ioi c).indicator 1) n x) Filter.atTop (nhds (cfc ((Set.Ioi c).indicator 1) (lambdaHat A T 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 filtration theorem, via the spectral-identification hypothesis.

Same as oseledets_filtration_of_upper, but with the band-projector hypothesis hband replaced by the spectral-identification hypothesis hident, consumed by specList_le_liminf_inv_mul_log_norm_cocycle_apply_of_slowflag.