Reducing the interface hypotheses of the Oseledets filtration

This file provides three independent reduction steps feeding the final assembly of Oseledets.oseledets_filtration:

1. tendsto_inv_mul_log_norm_cocycle_apply_of_upper_lower — the per-vector exact growth interface (hgrowth) from the per-vector upper bound (limsup ≤ specList) and lower bound (specList ≤ liminf), squeezed to a genuine Tendsto via tendsto_inv_mul_log_norm_cocycle_apply.

2. oseledets_filtration_of_interfaces' — a re-pointing of the assembly from the only-a.e.-measurable limsup flag vflag onto an everywhere-measurable family (built from the slow spectral filtration vslow), transporting the a.e. structural interfaces along the a.e. identification vslow = vflag.

3. specList_eq_expEnum_of_lyapunovSpectrum_const — the spectrum-constancy interface (hspec), reducing it to the a.e. constancy of the (T-invariant) per-point Lyapunov spectrum.

Main results

• Oseledets.tendsto_inv_mul_log_norm_cocycle_apply_of_upper_lower: the per-vector growth limit from the two one-sided bounds.
• Oseledets.vassembled_structure_ae: the a.e. structural block of the assembled flag vassembled, stated without any measurability conclusion.
• Oseledets.oseledets_filtration_of_interfaces': the Oseledets filtration target with the measurability clause carried by an everywhere-measurable witness family.
• Oseledets.specList_eq_expEnum_of_lyapunovSpectrum_const: the hspec interface from a.e. spectrum constancy.

The per-vector growth interface from the upper and lower bounds

The hgrowth interface of oseledets_filtration_of_interfaces asks, a.e., for a genuine limit (1/n) log‖A⁽ⁿ⁾ v‖ → specList A T x i on each stratum vflag castSucc \ vflag succ. The analytic core supplies the two one-sided bounds:

• the per-vector lower bound specList A T x i ≤ liminf … (from log_le_liminf_log_cocycle_apply at threshold c = e^{specList i}, packaged here as the hypothesis hlb); and
• the spectral upper bound limsup … ≤ specList A T x i (packaged here as the hypothesis hub).

The squeeze tendsto_inv_mul_log_norm_cocycle_apply turns the two bounds into the limit, modulo the two IsBoundedUnder side-conditions; we take those as the minimal a.e. hypothesis hbdd.

theorem Oseledets.tendsto_inv_mul_log_norm_cocycle_apply_of_upper_lower {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} (A : X → Matrix (Fin d) (Fin d) ℝ) (hub : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (specCard A T x)), ∀ v ∈ ↑(vflag A T x i.castSucc), v ∉ vflag A T x i.succ → Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) Filter.atTop ≤ specList A T x i) (hlb : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (specCard A T x)), ∀ v ∈ ↑(vflag A T x i.castSucc), v ∉ vflag A T x i.succ → specList A T x i ≤ Filter.liminf (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) Filter.atTop) (hbdd : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (specCard A T x)), ∀ v ∈ ↑(vflag A T x i.castSucc), v ∉ vflag A T x i.succ → (Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) ∧ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) : ∀ᵐ (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))

hgrowth from upper + lower bounds. Given, a.e., the per-stratum-vector upper bound (limsup ≤ specList), lower bound (specList ≤ liminf), and the two IsBoundedUnder side-conditions, the per-vector growth interface of oseledets_filtration_of_interfaces holds.

The conclusion is stated with Matrix.toEuclideanCLM (the form consumed by the assembly); the hypotheses use Matrix.toEuclideanLin, and the two coincide (Matrix.coe_toEuclideanCLM_eq_toEuclideanLin).

The measurability-independent structural core of the assembly

oseledets_filtration_of_interfaces bundles the a.e. structural block with the existential (V := vassembled) and the hmeas argument. To re-point onto an everywhere-measurable witness we need that a.e. block separately, without the hmeas argument. vassembled_structure_ae extracts exactly that block; its proof is the structural body of oseledets_filtration_of_interfaces, dropping only the existential-introduction refine.

theorem Oseledets.vassembled_structure_ae {X : Type u_1} [MeasurableSpace X] {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 : ℕ → ℝ) (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)) (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))) : ∀ᵐ (x : X) ∂μ, vassembled A T (numExp lam0 d) 0 x = ⊤ ∧ vassembled A T (numExp lam0 d) (Fin.last (numExp lam0 d)) x = ⊥ ∧ (∀ (i : Fin (numExp lam0 d)), vassembled A T (numExp lam0 d) i.succ x < vassembled A T (numExp lam0 d) i.castSucc x) ∧ (∀ (i : Fin (numExp lam0 d + 1)), Submodule.map (↑(Matrix.toEuclideanCLM (A x))) (vassembled A T (numExp lam0 d) i x) = vassembled A T (numExp lam0 d) i (T x)) ∧ ∀ (i : Fin (numExp lam0 d)), ∀ v ∈ ↑(vassembled A T (numExp lam0 d) i.castSucc x), v ∉ vassembled A T (numExp lam0 d) 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))

The a.e. structural block of the assembled flag vassembled: almost everywhere the flag is full at 0, trivial at Fin.last, strictly decreasing, equivariant under A x, and carries the exact per-vector growth rates expEnum lam0 d. This is the conclusion of oseledets_filtration_of_interfaces without the measurability clause and without the existential packaging.

Re-pointing the assembly onto an everywhere-measurable family

vassembled is built from the limsup flag vflag, whose measurability is only available a.e. The MeasurableSubspace predicate is an everywhere statement, so hmeas cannot be discharged for vassembled directly. The fix is to carry the structural conclusion on a different, everywhere-measurable family vprime (built from the slow spectral filtration vslow, whose measurability is measurableSubspace_vslow), and transport the a.e. structural facts along the a.e. identification vprime = vassembled.

oseledets_filtration_of_interfaces' takes:

• the same hspec/hgrowth interfaces as oseledets_filtration_of_interfaces (they feed vassembled);
• hmeas' — MeasurableSubspace for the slow-based family vprime (discharged via measurableSubspace_vslow); and
• hae — the a.e. identification vprime i x = vassembled A T (numExp lam0 d) i x.

It produces the oseledets_filtration target with witness V := vprime. The structural a.e. block is the vassembled block of vassembled_structure_ae rewritten, level by level, through hae.

The a.e. identification hae is itself the substantive mathematical content (vslow = vflag a.e.); it is taken here as a cleanly-typed hypothesis and is discharged by vprime_eq_vassembled_of_slowflag.

theorem Oseledets.oseledets_filtration_of_interfaces' {X : Type u_1} [MeasurableSpace X] {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 : ℕ → ℝ) (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)) (vprime : Fin (numExp lam0 d + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))) (hmeas' : ∀ (i : Fin (numExp lam0 d + 1)), MeasurableSubspace fun (x : X) => vprime i x) (hae : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (numExp lam0 d + 1)), vprime i 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 Oseledets filtration target from the structural interfaces, with the measurability clause carried by an everywhere-measurable family vprime that agrees a.e. with the assembled flag vassembled.

The spectrum-constancy interface

hspec asks that, a.e., the per-point limsup spectrum (specCard/specList, built from the finite limsup spectrum lyapunovSpectrum A T x of lambdaBar) coincides with the deterministic singular-value spectrum (numExp/expEnum, built from distinctExp lam0 d).

lyapunovSpectrum_equivariant_ae provides the T-invariance lyapunovSpectrum A T x = lyapunovSpectrum A T (T x) a.e.; ergodicity upgrades this to a.e. constancy of the finite set lyapunovSpectrum A T x, and the spectral identification of Λ pins that constant set to distinctExp lam0 d. Packaging both as the single hypothesis hspecconst : ∀ᵐ x, lyapunovSpectrum A T x = distinctExp lam0 d, the hspec shape is then a pure Finset/Fin-reindexing computation: specCard and numExp are both the cardinality of the (now-equal) finite set, and specList and expEnum are both its descending orderEmbOfFin-enumeration, so they agree along the cardinality cast.

The constancy-to-distinctExp step (hspecconst) is the ergodic content; it is taken here as a cleanly-typed hypothesis and is discharged by lyapunovSpectrum_eq_distinctExp_of_lambdaBar.

theorem Oseledets.specList_eq_expEnum_of_lyapunovSpectrum_const {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} (A : X → Matrix (Fin d) (Fin d) ℝ) (lam0 : ℕ → ℝ) (hspecconst : ∀ᵐ (x : X) ∂μ, lyapunovSpectrum A T x = distinctExp lam0 d) : ∀ᵐ (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)

hspec from a.e. spectrum constancy. If the per-point limsup spectrum lyapunovSpectrum A T x equals the deterministic distinct-exponent set distinctExp lam0 d a.e., then the hspec interface of oseledets_filtration_of_interfaces holds: a.e. the spectrum cardinality equals numExp lam0 d and the descending enumeration specList equals expEnum lam0 d along the cardinality cast.