Restriction of the cocycle to an invariant subbundle

Given a measurable, cocycle-invariant subbundle W : X → Submodule ℝ (EuclideanSpace ℝ (Fin d)) of the ambient bundle, the Lyapunov spectrum realized inside W is a sub-object of the ambient limsup spectrum.

Main definitions

• InvariantSubbundle — a measurable, a.e. cocycle-invariant subbundle, with the equivariance shape Submodule.map (toEuclideanCLM (A x)).toLinearMap (W x) = W (T x) matching Oseledets.IsOseledetsFiltration / vflag_equivariant.
• restrictedSpectrum — the exponents realized by nonzero vectors of W x, as a sub-Finset of lyapunovSpectrum A T x.

Main results

• restrictedSpectrum_subset / restrictedSpectrum_subset_ae — the restricted spectrum is a subset of the ambient spectrum (immediate from lambdaBar_mem_lyapunovSpectrum).
• restricted_finrank_le — the dimension interlacing finrank (W x ⊓ vflag A T x i) ≤ finrank (vflag A T x i) (a sub-multiplicity bound).
• restricted_inf_lambdaSublevel_equivariant — the intersections W ⊓ vflag are themselves A-equivariant a.e., so the restricted multiplicities finrank (W ⊓ vflag i) are a.e. T-invariant.
• restricted_inf_measurableSubspace — each restricted level x ↦ W x ⊓ V i x is everywhere measurable.
• restricted_inf_witness_equivariant / restricted_inf_witness_finrank_invariant_ae — the restricted levels are A-equivariant a.e., so their dimensions are a.e. T-invariant.
• restricted_inf_finrank_ae_eq — for ergodic T, the restricted dimension profile i ↦ finrank (W ⊓ V i) is a.e. a deterministic antitone sequence m.
• restricted_flag_structure_ae — the non-strict Fin (k+1)-indexed flag i ↦ W ⊓ V i a.e. runs from W (level 0) to ⊥ (level last k), is equivariant and antitone, with exact growth rate lam i on each non-strict stratum.
• restricted_strict_filtration — collapsing the constant-dimension levels (via the first-occurrence survivingSet of m, enumerated by Finset.orderEmbOfFin) yields a strict Oseledets filtration realized inside W: a StrictAnti exponent list lam', an everywhere-measurable strictly descending equivariant flag from W to ⊥ with exact growth rates, and all levels ≤ W.

Implementation notes

The "interlacing" here means that the restricted exponents form a sub-multiset of the ambient exponent multiset (with multiplicities bounded by finrank monotonicity of W ⊓ vflag inside vflag). This is not classical Cauchy eigenvalue interlacing. The restricted dimension profile is antitone but not strictly so: W may capture the same dimension at consecutive ambient levels.

The full restricted filtration intersects W with the forward Oseledets witness V of an IsOseledetsFiltration (the everywhere-measurable family — not the a.e.-only vflag, which has no MeasurableSubspace instance). Measurability of x ↦ W x ⊓ V i x then follows from MeasurableSubspace.inf (Oseledets/TwoSided/MeasurableInf.lean).

The top level of the restricted strict flag is W, which equals the ambient ⊤ only when W = ⊤. Since IsOseledetsFiltration hard-codes V 0 = ⊤, a strict restricted flag with all levels ≤ W for a proper subbundle cannot satisfy that predicate (it would force ⊤ ≤ W). restricted_strict_filtration therefore states the restricted-filtration content directly (top = W) rather than reusing IsOseledetsFiltration.

All standing hypotheses match the rest of the development (hT : Ergodic T μ, hA : ∀ x, (A x).det ≠ 0, hAmeas : Measurable A, hint : IntegrableLogNorm A μ, hint' : IntegrableLogNorm (fun x => (A x)⁻¹) μ, [IsProbabilityMeasure μ]).

References

• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

The invariant subbundle structure

structure Oseledets.InvariantSubbundle {X : Type u_1} {d : ℕ} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (T : X → X) (A : X → Matrix (Fin d) (Fin d) ℝ) : Type u_1

A measurable, cocycle-invariant subbundle of the ambient bundle EuclideanSpace ℝ (Fin d) over the base X, relative to a measure μ, dynamics T, and linear cocycle generator A.

The invariance is the a.e. equivariance Submodule.map (toEuclideanCLM (A x)).toLinearMap (W x) = W (T x), the exact shape used by Oseledets.IsOseledetsFiltration and vflag_equivariant.

• W : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))

  The fibre subspace at each base point.

• meas : MeasurableSubspace self.W

  The fibre varies measurably in the base point.

• invariant_ae : ∀ᵐ (x : X) ∂μ, Submodule.map (↑(Matrix.toEuclideanCLM (A x))) (self.W x) = self.W (T x)

  The subbundle is A-invariant almost everywhere.

The restricted spectrum

noncomputable def Oseledets.restrictedSpectrum {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (W : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))) (x : X) : Finset ℝ

The restricted limsup spectrum at x: the sub-Finset of the ambient spectrum lyapunovSpectrum A T x consisting of the exponents realized by some nonzero vector of W x.

Equations

• Oseledets.restrictedSpectrum A T W x = {r ∈ Oseledets.lyapunovSpectrum A T x | ∃ v ∈ W x, v ≠ 0 ∧ Oseledets.lambdaBar A T x v = r}

theorem Oseledets.mem_restrictedSpectrum {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X → X} {W : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {x : X} {r : ℝ} : r ∈ restrictedSpectrum A T W x ↔ r ∈ lyapunovSpectrum A T x ∧ ∃ v ∈ W x, v ≠ 0 ∧ lambdaBar A T x v = r

A value lies in the restricted spectrum iff it is in the ambient spectrum and realized by a nonzero vector of W x.

theorem Oseledets.restrictedSpectrum_subset {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (W : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))) (x : X) : restrictedSpectrum A T W x ⊆ lyapunovSpectrum A T x

The restricted spectrum is a subset of the ambient spectrum (pointwise, no hypotheses): every exponent realized inside W x is realized in the ambient space.

theorem Oseledets.lambdaBar_mem_restrictedSpectrum {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X → X} {W : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {x : X} (hx : IsUltrametricGrowth (lambdaBar A T x)) {v : EuclideanSpace ℝ (Fin d)} (hvW : v ∈ W x) (hv : v ≠ 0) : lambdaBar A T x v ∈ restrictedSpectrum A T W x

Every nonzero vector of W x realizes an exponent of the restricted spectrum (under the IsUltrametricGrowth hypothesis that makes the ambient spectrum well-behaved).

theorem Oseledets.restrictedSpectrum_subset_ae {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (A : X → Matrix (Fin d) (Fin d) ℝ) (W : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))) : ∀ᵐ (x : X) ∂μ, restrictedSpectrum A T W x ⊆ lyapunovSpectrum A T x

The restricted spectrum is a.e. a subset of the ambient spectrum. This is immediate from the pointwise restrictedSpectrum_subset.

Dimension interlacing (sub-multiplicity bound)

The restricted multiplicities are bounded by the ambient multiplicities: at each flag level vflag A T x i, the part captured by W x is the intersection W x ⊓ vflag A T x i, whose dimension is at most that of the ambient level by finrank monotonicity. The "interlacing" is that the restricted exponents form a sub-multiset of the ambient exponent multiset.

theorem Oseledets.restricted_finrank_le {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (W : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))) (x : X) (i : Fin (specCard A T x + 1)) : Module.finrank ℝ ↥(W x ⊓ vflag A T x i) ≤ Module.finrank ℝ ↥(vflag A T x i)

Dimension interlacing. At each ambient flag level, the dimension captured by the subbundle is at most the ambient dimension.

theorem Oseledets.restricted_multiplicity_le {X : Type u_1} {d : ℕ} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} {W : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {x : X} (hx : IsUltrametricGrowth (lambdaBar A T x)) (i : Fin (specCard A T x)) : Module.finrank ℝ ↥(W x ⊓ vflag A T x i.castSucc) - Module.finrank ℝ ↥(W x ⊓ vflag A T x i.succ) ≤ Module.finrank ℝ ↥(vflag A T x i.castSucc) - Module.finrank ℝ ↥(vflag A T x i.succ)

The restricted multiplicity at a stratum is bounded by the ambient multiplicity: dim (W ⊓ V i) - dim (W ⊓ V (i+1)) ≤ dim (V i) - dim (V (i+1)). This is the sub-multiset interlacing of the exponent multisets (not Cauchy interlacing).

Mathematically: (W ⊓ V i) / (W ⊓ V (i+1)) embeds into (V i) / (V (i+1)), so the restricted stratum dimension is at most the ambient one. This is the modular-law identity dim ((W⊓Vᵢ) ⊔ Vₛ) + dim (W⊓Vₛ) = dim (W⊓Vᵢ) + dim Vₛ combined with (W⊓Vᵢ) ⊔ Vₛ ≤ Vᵢ.

Equivariance of the restricted sublevels

The intersections W ⊓ lambdaSublevel … t are themselves A-equivariant a.e.: the map A x is injective (invertible matrix), so it commutes with ⊓ (Submodule.map_inf), and both W (by InvariantSubbundle.invariant_ae) and the sublevels (by vflag_equivariant) are equivariant. Indexing by a real threshold t (rather than by Fin (specCard …)) sidesteps the index-type transport specCard A T x = specCard A T (T x); the flag levels vflag A T x i on the interior are exactly such sublevels (vflag_of_lt).

Hence the restricted multiplicities finrank (W ⊓ lambdaSublevel … t) are a.e. T-invariant. Their a.e. constancy by ergodicity is obtained via the forward witness V below, whose levels carry a MeasurableSubspace instance.

theorem Oseledets.restricted_inf_lambdaSublevel_equivariant {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (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)⁻¹) μ) (Wb : InvariantSubbundle μ T A) : ∀ᵐ (x : X) ∂μ, ∀ (t : ℝ), Submodule.map (↑(Matrix.toEuclideanCLM (A x))) (Wb.W x ⊓ lambdaSublevel A T x t) = Wb.W (T x) ⊓ lambdaSublevel A T (T x) t

A-equivariance of the restricted sublevels (a.e.). For a.e. x and every threshold t, the action of A x maps the restricted sublevel W x ⊓ lambdaSublevel A T x t onto W (T x) ⊓ lambdaSublevel A T (T x) t. Since interior flag levels are sublevels (vflag_of_lt), this is the equivariance of the restricted flag.

theorem Oseledets.restricted_finrank_invariant_ae {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (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)⁻¹) μ) (Wb : InvariantSubbundle μ T A) : ∀ᵐ (x : X) ∂μ, ∀ (t : ℝ), Module.finrank ℝ ↥(Wb.W (T x) ⊓ lambdaSublevel A T (T x) t) = Module.finrank ℝ ↥(Wb.W x ⊓ lambdaSublevel A T x t)

A.e. T-invariance of the restricted multiplicities. For a.e. x and every threshold t, the dimension of the restricted sublevel is preserved by T: finrank (W (T x) ⊓ lambdaSublevel A T (T x) t) = finrank (W x ⊓ lambdaSublevel A T x t).

This is the invariance underlying ergodic constancy; the constancy is obtained via the forward witness V below, whose levels carry a MeasurableSubspace instance.

The full restricted Oseledets filtration

Intersecting the invariant subbundle W with the forward Oseledets witness V (the everywhere-measurable family from IsOseledetsFiltration, not the a.e.-only vflag) gives a Fin (k+1)-indexed non-strict flag i ↦ W ⊓ V i. By MeasurableSubspace.inf this is everywhere measurable, and it inherits equivariance, a.e. constancy of dimensions, and the exact growth clause. Collapsing the levels where the dimension does not drop produces a strict flag, which is a genuine IsOseledetsFiltration whose levels lie inside W.

theorem Oseledets.restricted_inf_measurableSubspace {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} {k : ℕ} {V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (Wb : InvariantSubbundle μ T A) (hVmeas : ∀ (i : Fin (k + 1)), MeasurableSubspace fun (x : X) => V i x) (i : Fin (k + 1)) : MeasurableSubspace fun (x : X) => Wb.W x ⊓ V i x

(A) Measurability of the restricted level W ⊓ V i. For an everywhere-measurable forward witness family V, the intersection with the subbundle W is everywhere measurable (via MeasurableSubspace.inf).

theorem Oseledets.restricted_inf_witness_equivariant {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) {k : ℕ} {lam : Fin k → ℝ} {V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (Wb : InvariantSubbundle μ T A) (hV : IsOseledetsFiltration μ T A k lam V) : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (k + 1)), Submodule.map (↑(Matrix.toEuclideanCLM (A x))) (Wb.W x ⊓ V i x) = Wb.W (T x) ⊓ V i (T x)

Equivariance of the restricted level W ⊓ V i (a.e.). Mirrors restricted_inf_lambdaSublevel_equivariant, but intersecting with the equivariant forward witness V of an IsOseledetsFiltration instead of with the sublevels.

theorem Oseledets.restricted_inf_witness_finrank_invariant_ae {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) {k : ℕ} {lam : Fin k → ℝ} {V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (Wb : InvariantSubbundle μ T A) (hV : IsOseledetsFiltration μ T A k lam V) : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (k + 1)), Module.finrank ℝ ↥(Wb.W (T x) ⊓ V i (T x)) = Module.finrank ℝ ↥(Wb.W x ⊓ V i x)

A.e. T-invariance of the restricted level dimension finrank (W ⊓ V i). Mirrors restricted_finrank_invariant_ae, intersecting with the forward witness V.

theorem Oseledets.restricted_inf_finrank_ae_eq {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) {k : ℕ} {lam : Fin k → ℝ} {V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (Wb : InvariantSubbundle μ T A) (hV : IsOseledetsFiltration μ T A k lam V) : ∃ (m : Fin (k + 1) → ℕ), Antitone m ∧ ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (k + 1)), Module.finrank ℝ ↥(Wb.W x ⊓ V i x) = m i

(B) A.e.-constant restricted level dimensions. For ergodic T, the restricted multiplicity profile i ↦ finrank (W ⊓ V i) is a.e. equal to a deterministic antitone sequence m : Fin (k+1) → ℕ. The sequence is antitone but not strictly so: W may capture the same dimension at consecutive levels.

theorem Oseledets.restricted_flag_structure_ae {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) {k : ℕ} {lam : Fin k → ℝ} {V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (Wb : InvariantSubbundle μ T A) (hV : IsOseledetsFiltration μ T A k lam V) : (∀ (i : Fin (k + 1)), MeasurableSubspace fun (x : X) => Wb.W x ⊓ V i x) ∧ ∀ᵐ (x : X) ∂μ, Wb.W x ⊓ V 0 x = Wb.W x ∧ Wb.W x ⊓ V (Fin.last k) x = ⊥ ∧ (Antitone fun (i : Fin (k + 1)) => Wb.W x ⊓ V i x) ∧ (∀ (i : Fin (k + 1)), Submodule.map (↑(Matrix.toEuclideanCLM (A x))) (Wb.W x ⊓ V i x) = Wb.W (T x) ⊓ V i (T x)) ∧ ∀ (i : Fin k), ∀ v ∈ ↑(Wb.W x) ⊓ ↑(V i.castSucc x), v ∉ Wb.W x ⊓ 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 restricted non-strict flag structure (a.e.). The Fin (k+1)-indexed family i ↦ W ⊓ V i (intersection of the subbundle with the forward Oseledets witness) is everywhere measurable, and a.e. forms an A-equivariant antitone flag from W (level 0) to ⊥ (level last k), on which every vector of stratum i (in W ⊓ V i.castSucc but not in W ⊓ V i.succ) grows at the exact rate lam i. This is the non-strict precursor of the restricted Oseledets filtration; collapsing the constant-dimension levels turns it into a strict flag (restricted_strict_filtration).

Level-collapse of an antitone profile to a strict flag

Reindexing infrastructure for restricted_strict_filtration. Given the antitone dimension profile m : Fin (k+1) → ℕ of the non-strict restricted flag, the surviving levels are the first-occurrence indices of each distinct value (survivingSet). Enumerating them in order via Finset.orderEmbOfFin selects a strictly nested subflag.

The full restricted Oseledets filtration (strict flag)

The full restricted (strict) Oseledets filtration: a strict Oseledets filtration realized inside the invariant subbundle W. Its top level is W (not the ambient ⊤), so it is the Oseledets filtration of the restricted sub-cocycle, with all levels lying in W.

The non-strict precursor i ↦ W ⊓ V i has W ⊓ V 0 = W. Hence the top level of the strict restricted flag is W, which is ⊤ only when W = ⊤. The IsOseledetsFiltration predicate hard-codes V 0 = ⊤ (the ambient top), so a strict flag with all levels ≤ W for a proper subbundle W cannot satisfy IsOseledetsFiltration (that would force ⊤ ≤ W). The statement below therefore expresses the restricted-filtration content directly (top = W, strict descending flag to ⊥, equivariance, exact growth rates, all levels ≤ W) rather than reusing IsOseledetsFiltration.

theorem Oseledets.restricted_strict_filtration {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (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)⁻¹) μ) (Wb : InvariantSubbundle μ T A) : ∃ (k' : ℕ) (lam' : Fin k' → ℝ) (vprime : Fin (k' + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin d))), StrictAnti lam' ∧ (∀ (i : Fin (k' + 1)), MeasurableSubspace fun (x : X) => vprime i x) ∧ ∀ᵐ (x : X) ∂μ, vprime 0 x = Wb.W x ∧ vprime (Fin.last k') x = ⊥ ∧ (∀ (i : Fin k'), vprime i.succ x < vprime i.castSucc x) ∧ (∀ (i : Fin (k' + 1)), Submodule.map (↑(Matrix.toEuclideanCLM (A x))) (vprime i x) = vprime i (T x)) ∧ (∀ (i : Fin k'), ∀ v ∈ ↑(vprime i.castSucc x), v ∉ vprime i.succ x → Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A T n x)) v‖) Filter.atTop (nhds (lam' i))) ∧ ∀ (i : Fin (k' + 1)), vprime i x ≤ Wb.W x

The full restricted (strict) Oseledets filtration. Collapsing the constant-dimension levels of the non-strict precursor i ↦ W ⊓ V i (via the first-occurrence survivingSet of its antitone dimension profile, enumerated by Finset.orderEmbOfFin) yields a genuine strict Oseledets filtration realized inside the invariant subbundle W. There is a StrictAnti exponent list lam' : Fin k' → ℝ and an everywhere-measurable family vprime such that, μ-a.e., the flag vprime is strictly descending (vprime i.succ x < vprime i.castSucc x) from its top level vprime 0 x = W x down to vprime (last k') x = ⊥, is A-equivariant, has exact growth rate lam' i on each stratum, and has all levels lying inside W (vprime i x ≤ W x).

The top level of the restricted strict flag is W, which equals the ambient ⊤ only when W = ⊤. Since IsOseledetsFiltration hard-codes V 0 = ⊤, a strict restricted flag with all levels ≤ W for a proper subbundle cannot satisfy that predicate (it would force ⊤ ≤ W), so the statement expresses the restricted-filtration content directly (top = W) rather than reusing IsOseledetsFiltration.