The Oseledets filtration from structural interfaces

This file assembles the full Oseledets filtration statement from the structural layers already in place — the limsup flag Oseledets.vflag and the deterministic exponent enumeration Oseledets.expEnum — together with explicit analytic hypotheses (ergodic spectrum constancy, measurability of the flag levels, and exact per-vector growth).

Main definitions

• Oseledets.vassembled: the limsup flag vflag, reindexed to the deterministic index set Fin (k + 1) on the set where the per-point spectrum cardinality equals k.

Main results

• Oseledets.oseledets_filtration_of_interfaces: the Oseledets filtration conclusion, given the three analytic hypotheses.
• Oseledets.oseledets_filtration_assembled: the same statement with the exact conclusion shape of Oseledets.oseledets_filtration.

noncomputable def Oseledets.vassembled {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (k : ℕ) (i : Fin (k + 1)) (x : X) : Submodule ℝ (EuclideanSpace ℝ (Fin d))

The assembled deterministic-index filtration: on the (a.e.) good set where the per-point spectrum cardinality equals the deterministic k, it is the limsup flag vflag reindexed via the cast Fin (k+1) ≃ Fin (specCard x + 1); off the good set it is the junk value ⊤.

Equations

• Oseledets.vassembled A T k i x = if h : Oseledets.specCard A T x = k then Oseledets.vflag A T x (Fin.cast ⋯ i) else ⊤

theorem Oseledets.vassembled_of_eq {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X → X} {k : ℕ} {x : X} (h : specCard A T x = k) (i : Fin (k + 1)) : vassembled A T k i x = vflag A T x (Fin.cast ⋯ i)

On the good set, where the per-point spectrum cardinality equals k, the assembled filtration vassembled is the limsup flag vflag reindexed by the cast.

theorem Oseledets.oseledets_filtration_of_interfaces {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : 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 : ℕ → ℝ) (hspec : ∀ᵐ (x : X) ∂μ, ∃ (h : specCard A T x = numExp lam0 d), ∀ (i : Fin (specCard A T x)), specList A T x i = expEnum lam0 d (Fin.cast h i)) (hmeas : ∀ (i : Fin (numExp lam0 d + 1)), MeasurableSubspace fun (x : X) => vassembled A T (numExp lam0 d) i x) (hgrowth : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (specCard A T x)), ∀ v ∈ ↑(vflag A T x i.castSucc), v ∉ vflag A T x i.succ → Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A T n x)) v‖) Filter.atTop (nhds (specList A T x i))) : ∃ (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))

Assembly of the Oseledets filtration, modulo three analytic hypotheses.

The deterministic exponents lam = expEnum lam0 d (strictly antitone) and k = numExp lam0 d come from the ergodic singular-value Lyapunov spectrum lam0 of exists_lam_tendsto_singularValue. The subspace family is the limsup flag vflag reindexed to the deterministic index set (vassembled).

Three structural inputs are taken as explicit hypotheses; they are discharged downstream by the spectrum-constancy, measurability, and exact-growth layers:

• hspec — ergodic spectrum constancy: for a.e. x the per-point limsup spectrum cardinality equals k and its descending enumeration equals the deterministic lam.
• hmeas — measurability: each reindexed flag level is a MeasurableSubspace (discharged via measurableSubspace_vslow after the a.e. flag/Λ-spectral identification).
• hgrowth — per-vector exact growth: for a.e. x, on each stratum vflag castSucc \ vflag succ the normalized log-growth converges to the stratum exponent specList A T x i (the limsup is already pinned by lambdaBar_eq_on_stratum; this is upgraded to a genuine limit via tendsto_inv_mul_log_norm_cocycle_apply_of_bandProjector_envelope).

theorem Oseledets.oseledets_filtration_assembled {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : 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 : ℕ → ℝ) (hspec : ∀ᵐ (x : X) ∂μ, ∃ (h : specCard A T x = numExp lam0 d), ∀ (i : Fin (specCard A T x)), specList A T x i = expEnum lam0 d (Fin.cast h i)) (hmeas : ∀ (i : Fin (numExp lam0 d + 1)), MeasurableSubspace fun (x : X) => vassembled A T (numExp lam0 d) i x) (hgrowth : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (specCard A T x)), ∀ v ∈ ↑(vflag A T x i.castSucc), v ∉ vflag A T x i.succ → Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A T n x)) v‖) Filter.atTop (nhds (specList A T x i))) : ∃ (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 exact statement of Oseledets.oseledets_filtration, derived from oseledets_filtration_of_interfaces. The analytic hypotheses (lam0, hspec, hmeas, hgrowth) remain as explicit arguments; they are discharged by the spectrum-constancy, measurability, and exact-growth layers.