Strong export of the forward Oseledets filtration (two-sided MET)

This module records the one-sided Oseledets filtration theorem in a strong form: the deterministic spectral data lam0 and the everywhere-measurable filtration V are exposed by the existential (rather than buried), the Lyapunov exponents are the concrete descending enumeration expEnum lam0 d, and — the new content — the dimension of each interior filtration level is given by the forward dimension formula

finrank (V i.castSucc x) = #{j < d | lam0 j ≤ expEnum lam0 d i}.

The proof reuses the one-sided composition with the concrete witness V := vprime A T lam0: it discharges the top-gap fast-band-mass envelope, builds the spectral, slow-flag and growth interfaces exactly as oseledets_filtration_of_topgap and oseledets_filtration_of_upper' do, and reads the structural block off vassembled_structure_ae transported through vprime_eq_vassembled_of_slowflag. The dimension clause is supplied by ae_finrank_vslow, using that on the interior vprime A T lam0 reduces definitionally to vslow at the deterministic cutoff expEnum lam0 d i.

Main results

• oseledets_filtration_dims — the strong export with the spectral data exposed and the forward dimension formula adjoined.

theorem Oseledets.oseledets_filtration_dims {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)⁻¹) μ) : ∃ (lam0 : ℕ → ℝ), (∀ (a b : ℕ), a ≤ b → b < d → lam0 b ≤ lam0 a) ∧ (∀ 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))) ∧ ∃ (V : Fin (numExp lam0 d + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))), (∀ (i : Fin (numExp lam0 d + 1)), MeasurableSubspace fun (x : X) => V i x) ∧ ∀ᵐ (x : X) ∂μ, V 0 x = ⊤ ∧ V (Fin.last (numExp lam0 d)) x = ⊥ ∧ (∀ (i : Fin (numExp lam0 d)), V i.succ x < V i.castSucc x) ∧ (∀ (i : Fin (numExp lam0 d + 1)), Submodule.map (↑(Matrix.toEuclideanCLM (A x))) (V i x) = V i (T x)) ∧ (∀ (i : Fin (numExp lam0 d)), ∀ 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 (expEnum lam0 d i))) ∧ ∀ (i : Fin (numExp lam0 d)), Module.finrank ℝ ↥(V i.castSucc x) = {j ∈ Finset.range d | lam0 j ≤ expEnum lam0 d i}.card

Strong forward Oseledets filtration with dimensions.

The one-sided Oseledets theorem stated with its spectral data exposed: there is a deterministic antitone-on-[0, d) singular-exponent sequence lam0 such that, for every i < d, the normalized log of the i-th singular value of A⁽ⁿ⁾ converges to lam0 i a.e.; and there is an everywhere-measurable filtration V of EuclideanSpace ℝ (Fin d) indexed by Fin (numExp lam0 d + 1), whose Lyapunov exponents are the descending enumeration expEnum lam0 d, which is, a.e., a strictly decreasing A-equivariant flag ⊤ = V 0 ⊋ ⋯ ⊋ V (last) = ⊥ along which (1/n) log‖A⁽ⁿ⁾ v‖ → expEnum lam0 d i for v ∈ V i.castSucc ∖ V i.succ, and whose interior level dimensions satisfy the forward dimension formula finrank (V i.castSucc x) = #{j < d | lam0 j ≤ expEnum lam0 d i}.