The limsup flag (Lyapunov filtration)

This module builds, at each point x, the limsup flag associated to the upper Lyapunov growth function lambdaBar A T x of Oseledets.Lyapunov.GrowthFunction.

For a.e. x the function lambdaBar A T x is an IsUltrametricGrowth function (isUltrametricGrowth_lambdaBar); its values on nonzero vectors then form a finite set (IsUltrametricGrowth.finite_range), the limsup spectrum lyapunovSpectrum A T x. Enumerating the spectrum descending as λ₀ > λ₁ > ⋯ > λ_{k-1} (specList), the sublevel sets {v | v = 0 ∨ lambdaBar A T x v ≤ λᵢ} form a strictly decreasing flag

⊤ = vflag x 0 ⊋ vflag x 1 ⊋ ⋯ ⊋ vflag x k = ⊥

along which the cocycle grows at exactly the rate λᵢ on each stratum.

All objects are defined totally (with a ⊥/∅ junk value off the a.e. good set where lambdaBar A T x is IsUltrametricGrowth), so the structural theorems carry an explicit hypothesis hx : IsUltrametricGrowth (lambdaBar A T x).

Main results

• spectrum, specCard, specList — the finite, descending limsup spectrum;
• vflag — the limsup flag, indexed by Fin (specCard A T x + 1);
• vflag_zero / vflag_last — the extremal levels are ⊤ / ⊥;
• vflag_strictAnti — strict decrease between consecutive levels;
• lambdaBar_eq_on_stratum — on each stratum lambdaBar equals the exact exponent λᵢ;
• lyapunovSpectrum_equivariant_ae / vflag_equivariant — A-equivariance of the spectrum and the flag, a.e. in x.

References

• D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58.
• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

The limsup spectrum

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

The (finite) limsup spectrum at x: the set of values of lambdaBar A T x on nonzero vectors. Defined totally, with junk value ∅ off the set where lambdaBar A T x is an IsUltrametricGrowth function.

Equations

• Oseledets.lyapunovSpectrum A T x = if h : Oseledets.IsUltrametricGrowth (Oseledets.lambdaBar A T x) then ⋯.toFinset else ∅

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

Membership in the spectrum: a value lies in lyapunovSpectrum A T x iff it is realized by some nonzero vector.

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

Every value of lambdaBar A T x on a nonzero vector is in the spectrum.

noncomputable def Oseledets.specCard {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) : ℕ

The number of distinct exponents at x.

Equations

• Oseledets.specCard A T x = (Oseledets.lyapunovSpectrum A T x).card

noncomputable def Oseledets.specList {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) : Fin (specCard A T x) → ℝ

The descending enumeration of the limsup spectrum, specList A T x : Fin (specCard …) → ℝ. Index 0 is the largest exponent; the listing is strictly antitone.

Equations

• Oseledets.specList A T x i = ((Oseledets.lyapunovSpectrum A T x).orderEmbOfFin ⋯) i.rev

theorem Oseledets.specList_strictAnti {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) : StrictAnti (specList A T x)

The descending enumeration is strictly antitone.

theorem Oseledets.specList_mem {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (i : Fin (specCard A T x)) : specList A T x i ∈ lyapunovSpectrum A T x

Each enumerated exponent lies in the spectrum.

theorem Oseledets.exists_specList_eq {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {x : X} {r : ℝ} (hr : r ∈ lyapunovSpectrum A T x) : ∃ (i : Fin (specCard A T x)), specList A T x i = r

Every spectrum value is specList A T x i for some index i.

The limsup flag

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

The sublevel submodule of lambdaBar A T x at threshold t, defined totally with junk value ⊥ off the IsUltrametricGrowth set.

Equations

• Oseledets.lambdaSublevel A T x t = if h : Oseledets.IsUltrametricGrowth (Oseledets.lambdaBar A T x) then h.sublevel t else ⊥

theorem Oseledets.mem_lambdaSublevel {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {x : X} (hx : IsUltrametricGrowth (lambdaBar A T x)) (t : ℝ) (v : EuclideanSpace ℝ (Fin d)) : v ∈ lambdaSublevel A T x t ↔ v = 0 ∨ lambdaBar A T x v ≤ t

Membership in the sublevel submodule (under the IsUltrametricGrowth hypothesis).

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

The limsup flag at x, indexed by Fin (specCard A T x + 1). Interior levels are sublevel sets of lambdaBar A T x at the spectrum values; the last level (index specCard) is ⊥. With the descending enumeration specList, level j (for j < specCard) is the sublevel at exponent λ_j, so vflag x 0 = ⊤ and vflag x (last) = ⊥.

Equations

• Oseledets.vflag A T x j = if h : ↑j < Oseledets.specCard A T x then Oseledets.lambdaSublevel A T x (Oseledets.specList A T x ⟨↑j, h⟩) else ⊥

theorem Oseledets.vflag_of_lt {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {x : X} {j : Fin (specCard A T x + 1)} (h : ↑j < specCard A T x) : vflag A T x j = lambdaSublevel A T x (specList A T x ⟨↑j, h⟩)

On the interior, vflag is a sublevel set at the corresponding spectrum value.

theorem Oseledets.mem_vflag {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {x : X} (hx : IsUltrametricGrowth (lambdaBar A T x)) {j : Fin (specCard A T x + 1)} {v : EuclideanSpace ℝ (Fin d)} (hv : v ≠ 0) : v ∈ vflag A T x j ↔ ∃ (h : ↑j < specCard A T x), lambdaBar A T x v ≤ specList A T x ⟨↑j, h⟩

Unified membership criterion for a flag level (under the IsUltrametricGrowth hypothesis), for a nonzero vector.

Extremal levels

theorem Oseledets.vflag_zero {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {x : X} (hx : IsUltrametricGrowth (lambdaBar A T x)) : vflag A T x 0 = ⊤

The top level of the flag is everything.

theorem Oseledets.vflag_last {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) : vflag A T x (Fin.last (specCard A T x)) = ⊥

The bottom level of the flag is trivial.

Strict decrease and stratum exactness

theorem Oseledets.vflag_strictAnti {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {x : X} (hx : IsUltrametricGrowth (lambdaBar A T x)) (i : Fin (specCard A T x)) : vflag A T x i.succ < vflag A T x i.castSucc

Strict decrease of the flag.

theorem Oseledets.lambdaBar_eq_on_stratum {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {x : X} (hx : IsUltrametricGrowth (lambdaBar A T x)) (i : Fin (specCard A T x)) {v : EuclideanSpace ℝ (Fin d)} (hmem : v ∈ vflag A T x i.castSucc) (hnot : v ∉ vflag A T x i.succ) : lambdaBar A T x v = specList A T x i

On the stratum between consecutive levels, lambdaBar equals the exact exponent λᵢ.

A-equivariance

The invertible matrix A x acts on EuclideanSpace ℝ (Fin d) as the bijective continuous linear map Matrix.toEuclideanCLM (A x). Since lambdaBar A T x v = lambdaBar A T (T x) (A x · v) a.e. (by lambdaBar_equivariant_ae), this bijection identifies the spectrum and the sublevel sets at x with those at T x.

theorem Oseledets.lyapunovSpectrum_equivariant_ae {X : Type u_1} {T : X → X} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure 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)⁻¹) μ) : ∀ᵐ (x : X) ∂μ, lyapunovSpectrum A T x = lyapunovSpectrum A T (T x)

A-equivariance of the spectrum (a.e.). For a.e. x, lyapunovSpectrum A T x = lyapunovSpectrum A T (T x), hence specCard and specList agree (the latter as indexed functions over Fin (specCard …)).

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

A-equivariance of the flag (a.e.). For a.e. x, the action of A x maps each flag level at x onto the corresponding level at T x (the indices transport via the a.e. equality lyapunovSpectrum A T x = lyapunovSpectrum A T (T x), which makes specCard A T x = specCard A T (T x) and specList A T x = specList A T (T x) after that rewrite).