Documentation

Oseledets.Lyapunov.Extensions.SingularRank

Rank of a linear cocycle and its drop along the dynamics #

For a non-invertible cocycle the Oseledets decomposition degenerates to a filtration whose strata can lose dimension as the cocycle composes: the matrix products cocycle A T n x may have strictly decreasing rank in n. This file records that rank as the function Oseledets.cocycleRank, together with the basic dimension bounds and the headline rank-drop monotonicity: the rank of an (m + n)-step cocycle is bounded by the rank of each of its two composing factors, so it can only fall as the orbit advances. This is the dimension data underlying the singular (non-invertible) multiplicative ergodic theorem.

Literature source: A. Quas, Multiplicative Ergodic Theorems and Applications (lecture notes, Universidade de São Paulo, 2013), Theorem 2 (Oseledets theorem, non-invertible form, after Oseledec [12] and Raghunathan [13]): in the non-invertible case the conclusion is a filtration ℝ^d = V₁ ⊃ V₂ ⊃ ⋯ ⊃ {0} rather than a direct-sum decomposition, and the cocycle-rank measures the number of directions not yet collapsed by the matrix products.

Main definitions #

Main results #

noncomputable def Oseledets.cocycleRank {X : Type u_1} {d : } (A : XMatrix (Fin d) (Fin d) ) (T : XX) (n : ) (x : X) :

The rank of the n-step cocycle: the dimension of the image of cocycle A T n x, i.e. the number of directions in ℝ^d not yet collapsed after n steps of the cocycle. In the non-invertible Oseledets theorem (Quas, Multiplicative Ergodic Theorems and Applications, 2013, Theorem 2; after Oseledec and Raghunathan) this rank can strictly drop along the dynamics, producing the singular filtration rather than a direct-sum decomposition.

Equations
Instances For
    theorem Oseledets.cocycleRank_le {X : Type u_1} {d : } (A : XMatrix (Fin d) (Fin d) ) (T : XX) (n : ) (x : X) :
    cocycleRank A T n x d

    The cocycle rank is bounded by the ambient dimension d.

    @[simp]
    theorem Oseledets.cocycleRank_zero {X : Type u_1} {d : } (A : XMatrix (Fin d) (Fin d) ) (T : XX) (x : X) :
    cocycleRank A T 0 x = d

    The zero-step cocycle is the identity, so it has full rank d.

    theorem Oseledets.cocycleRank_add_le_left {X : Type u_1} {d : } (A : XMatrix (Fin d) (Fin d) ) (T : XX) (m n : ) (x : X) :
    cocycleRank A T (m + n) x cocycleRank A T m (T^[n] x)

    Rank drop, future factor. The rank of the (m + n)-step cocycle is bounded by the rank of its left factor cocycle A T m (T^[n] x): the rank cannot increase past the later block.

    theorem Oseledets.cocycleRank_add_le_right {X : Type u_1} {d : } (A : XMatrix (Fin d) (Fin d) ) (T : XX) (m n : ) (x : X) :
    cocycleRank A T (m + n) x cocycleRank A T n x

    Rank drop, past factor. The rank of the (m + n)-step cocycle is bounded by the rank of its right factor cocycle A T n x: the rank cannot exceed that of the earlier block, so it is non-increasing as the cocycle composes.

    theorem Oseledets.cocycleRank_add_le_min {X : Type u_1} {d : } (A : XMatrix (Fin d) (Fin d) ) (T : XX) (m n : ) (x : X) :
    cocycleRank A T (m + n) x min (cocycleRank A T m (T^[n] x)) (cocycleRank A T n x)

    Rank-drop monotonicity (combined). The rank of the (m + n)-step cocycle is at most the minimum of the ranks of its two composing factors. This is the dimension drop of the singular filtration: as the cocycle composes along the orbit its rank can only fall.