Documentation

Oseledets.Lyapunov.Extensions.SingularLambdaBarFiltration

The algebraic forward filtration from the upper Lyapunov exponent lambdaBar #

For a (possibly singular) matrix cocycle generator A : X → Matrix (Fin d) (Fin d) ℝ over T : X → X, this module builds — purely algebraically, det-free and inverse-free — the forward sublevel filtration of the pointwise upper Lyapunov exponent lambdaBar A T x v = limsup_n (1/n)·log‖A⁽ⁿ⁾(x)·v‖ (Oseledets.lambdaBar, Oseledets/Lyapunov/GrowthFunction.lean).

The origin/kernel subtlety (and why we floor at 0) #

lambdaBar is ℝ-valued with the convention Real.log 0 = 0, so lambdaBar A T x 0 = 0 (not −∞). More importantly, for a singular cocycle a nonzero vector can be eventually killed: if v + w ∈ ker (A⁽ⁿ⁾(x)) for infinitely many n, then growthSeq (v+w) n = (1/n)·log 0 = 0 along that subsequence, so lambdaBar A T x (v + w) ≥ 0 even when lambdaBar A T x v and lambdaBar A T x w are both strictly negative. Concretely, for the constant cocycle A x = diag(1/2, 0) one has lambdaBar (e₁ + e₂) = lambdaBar (−e₁) = log(1/2) < 0 while lambdaBar ((e₁ + e₂) + (−e₁)) = lambdaBar e₂ = 0. Hence the naive sublevel set {v | lambdaBar A T x v ≤ c} ∪ {0} is not a submodule for c < 0: closure under addition fails at the kernel. This is the genuine −∞-vs-0 obstruction of the singular forward filtration.

The honest, unconditional non-Archimedean inequality is therefore the floored one:

lambdaBar A T x (v + w) ≤ max (max (lambdaBar A T x v) (lambdaBar A T x w)) 0

(lambdaBar_add_le_max_zero). Consequently the function v ↦ max (lambdaBar A T x v) 0 is a genuine IsUltrametricGrowth function (isUltrametricGrowth_max_lambdaBar), and its sublevel sets are honest submodules. For thresholds c ≥ 0 — the regime of the genuine nonnegative singular spectrum — the floored sublevel set coincides with the intended set {v | lambdaBar A T x v ≤ c} ∪ {0} (mem_lambdaBarSublevel_iff).

The mild det-free finiteness hypothesis #

Both the floored ultrametric inequality and the genuineness of lambdaBar (as opposed to the Real-junk value of an unbounded limsup) need the top growth sequence n ↦ (1/n)·log‖A⁽ⁿ⁾(x)‖ to be bounded above at x. This is the det-free, inverse-free finiteness hypothesis HasFiniteTopGrowth A T x; it holds a.e. by Furstenberg–Kesten, and holds everywhere whenever A has uniformly bounded norm (e.g. A continuous on a compact base). It is strictly weaker than det A ≠ 0.

Main results #

References #

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

Det-free top-growth finiteness at x. The defining hypothesis of this module: the top growth sequence n ↦ (1/n)·log‖A⁽ⁿ⁾(x)‖ is bounded above at x. This is inverse-free and det-free; it holds a.e. by Furstenberg–Kesten and everywhere when A has bounded norm.

Equations
Instances For

    A robust floored limsup bound #

    The single soft-analysis fact that makes the floored non-Archimedean inequality unconditional: an eventual upper bound by a nonnegative constant caps the limsup, with no boundedness side condition — the nonnegativity of the cap absorbs the Real-junk value of an unbounded limsup.

    The floored non-Archimedean inequality #

    source
    theorem Oseledets.lambdaBar_le_of_hasFiniteTopGrowth {X : Type u_1} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (hx : HasFiniteTopGrowth A T x) (v : EuclideanSpace ℝ (Fin d)) :
    Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A T n x)) v‖

    lambdaBar is bounded above by the top growth at every v under HasFiniteTopGrowth. Det-free: the upper bound (1/n)·log‖A⁽ⁿ⁾(x)‖ + (1/n)·log‖v‖, floored at 0, is eventually finite and convergent, so its limsup caps lambdaBar.

    source
    theorem Oseledets.lambdaBar_add_le_max_zero {X : Type u_1} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (hx : HasFiniteTopGrowth A T x) (v w : EuclideanSpace ℝ (Fin d)) :
    lambdaBar A T x (v + w) ≤ max (max (lambdaBar A T x v) (lambdaBar A T x w)) 0

    The floored non-Archimedean inequality (unconditional given finite top growth). lambdaBar A T x (v + w) ≤ max (max (lambdaBar A T x v) (lambdaBar A T x w)) 0. The floor at 0 is necessary (the kernel of a singular cocycle can make lambdaBar (v + w) = 0 while lambdaBar v, lambdaBar w < 0).

    The genuine ultrametric growth function max (lambdaBar ·) 0 #

    source
    theorem Oseledets.isUltrametricGrowth_max_lambdaBar {X : Type u_1} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (hx : HasFiniteTopGrowth A T x) :
    IsUltrametricGrowth fun (v : EuclideanSpace ℝ (Fin d)) => max (lambdaBar A T x v) 0

    v ↦ max (lambdaBar A T x v) 0 is an ultrametric growth function (under finite top growth). Scaling-invariance is the unconditional lambdaBar_smul; the non-Archimedean inequality is the floored lambdaBar_add_le_max_zero (the floor at 0 is what makes g genuinely non-Archimedean despite the singular kernel).

    The sublevel submodule #

    source
    noncomputable def Oseledets.lambdaBarSublevel {X : Type u_1} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (x : X) (hx : HasFiniteTopGrowth A T x) :
    Submodule ℝ (EuclideanSpace ℝ (Fin d))

    The algebraic forward sublevel submodule at threshold c: the sublevel set of the ultrametric growth function v ↦ max (lambdaBar A T x v) 0. For c ≥ 0 it is {v | lambdaBar A T x v ≤ c} ∪ {0} (mem_lambdaBarSublevel_iff); for c < 0 the floor collapses it to {0}. Det-free and inverse-free.

    Equations
    Instances For
      source
      @[simp]
      theorem Oseledets.mem_lambdaBarSublevel {X : Type u_1} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (x : X) (hx : HasFiniteTopGrowth A T x) (v : EuclideanSpace ℝ (Fin d)) :
      v ∈ lambdaBarSublevel A T c x hx ↔ v = 0 ∨ max (lambdaBar A T x v) 0 ≤ c
      source
      theorem Oseledets.lambdaBarSublevel_antitone {X : Type u_1} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (hx : HasFiniteTopGrowth A T x) {c c' : ℝ} (hcc : c ≤ c') :
      lambdaBarSublevel A T c x hx ≤ lambdaBarSublevel A T c' x hx

      Antitone in the threshold. c ≤ c' makes the level-c space a subspace of the level-c' space.

      source
      theorem Oseledets.mem_lambdaBarSublevel_iff {X : Type u_1} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) {c : ℝ} (hc : 0 ≤ c) (x : X) (hx : HasFiniteTopGrowth A T x) (v : EuclideanSpace ℝ (Fin d)) :
      v ∈ lambdaBarSublevel A T c x hx ↔ v = 0 ∨ lambdaBar A T x v ≤ c

      Membership in the genuine regime 0 ≤ c. For nonnegative thresholds the floor is invisible: v ∈ lambdaBarSublevel A T c x ↔ v = 0 ∨ lambdaBar A T x v ≤ c. (For c < 0 the right disjunct would over-count kernel directions whose lambdaBar is < 0, which is exactly why the construction floors at 0.)

      The cocycle-step inequality and equivariance #

      The cocycle reindexing A⁽ⁿ⁾(Tx)·(A x·v) = A⁽ⁿ⁺¹⁾(x)·v ties the image defining sequence at T x to a one-shifted copy of the defining sequence at x. Writing L n = log‖A⁽ⁿ⁾(Tx)·(A x·v)‖, the image sequence is f n = n⁻¹·L n (the defining sequence at T x) and the shifted source sequence is g n = (n+1)⁻¹·L n (the source sequence at n+1). They are related by f n = ((n+1)/n)·g n (for n ≥ 1). The full identity at the spectrum level needs f bounded on both sides (lower boundedness is the invertible/det data, see Oseledets.lambdaBar_equivariant). The one-sided inequality below — which is all the sublevel filtration requires — is det-free: where L n ≥ 0 we have f n = g n + g n/n with g bounded above by HasFiniteTopGrowth A T x, and where L n < 0 we have f n < 0, so the floor at 0 absorbs it.

      source
      theorem Oseledets.lambdaBar_step_le {X : Type u_1} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (hx : HasFiniteTopGrowth A T x) (v : EuclideanSpace ℝ (Fin d)) :
      lambdaBar A T (T x) ((Matrix.toEuclideanCLM (A x)) v) ≤ max (lambdaBar A T x v) 0

      The det-free cocycle-step inequality lambdaBar A T (T x) (A x · v) ≤ max (lambdaBar A T x v) 0. No invertibility: the image exponent at T x is dominated by the (floored) source exponent at x. The floor at 0 is what makes this hold without a lower bound on the image sequence.

      source
      theorem Oseledets.lambdaBarSublevel_equivariant {X : Type u_1} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (x : X) (hx : HasFiniteTopGrowth A T x) (hTx : HasFiniteTopGrowth A T (T x)) {v : EuclideanSpace ℝ (Fin d)} (hv : v ∈ lambdaBarSublevel A T c x hx) :
      (Matrix.toEuclideanCLM (A x)) v ∈ lambdaBarSublevel A T c (T x) hTx

      Equivariance of the algebraic sublevel filtration. The cocycle step A x · maps the level-c space at x into the level-c space at T x: if v ∈ lambdaBarSublevel A T c x, then A x · v ∈ lambdaBarSublevel A T c (T x). Det-free, from lambdaBar_step_le.