The collapsing-kernel submodule of a singular linear cocycle

For a non-invertible (singular) cocycle the Oseledets multiplicative ergodic theorem degenerates from a direct-sum decomposition to a filtration ℝ^d = V₁(ω) ⊃ V₂(ω) ⊃ ⋯ ⊃ V_k(ω) ⊃ {0}, and the bottom space of that flag is the eventual kernel — the directions the matrix products ultimately collapse. This file records the finite-n building block of that bottom space: the kernel submodule Oseledets.cocycleKer A T n x, the set of vectors annihilated by the n-step cocycle.

The headline result is kernel monotonicity along the orbit: once a direction is collapsed by the cocycle it stays collapsed, so the kernel can only grow as the cocycle composes (cocycleKer_le_add). Together with the rank–nullity identity finrank (cocycleKer) = d - cocycleRank (finrank_cocycleKer) this is the dimension data of the bottom stratum of the singular filtration. The full measurable flag V₁(ω) ⊃ ⋯ ⊃ {0} of the singular MET is not constructed here; see the module note below for the precise remaining gap.

Literature source (impl-i6-flag): 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]). There the non-invertible conclusion is the measurable filtration ℝ^d = V₁(ω) ⊃ V₂(ω) ⊃ ⋯ ⊃ V_{k+1}(ω) = {0} with A_ω V_j(ω) ⊆ V_j(σ ω); the bottom V_{k+1}(ω) = {0} together with the equivariance A_ω V_j(ω) ⊆ V_j(σ ω) is the abstraction the kernel submodule of this file makes concrete at finite n.

Main definitions

• Oseledets.cocycleKer: the kernel LinearMap.ker (cocycle A T n x).mulVecLin of the n-step cocycle — the directions collapsed after n steps.

Main results

• Oseledets.cocycleKer_zero: cocycleKer A T 0 x = ⊥ (the zero-step cocycle is the identity, with trivial kernel).
• Oseledets.cocycleKer_le_add: kernel monotonicity — cocycleKer A T n x ≤ cocycleKer A T (m + n) x: collapsed directions stay collapsed, so the kernel only grows as the cocycle composes along the orbit.
• Oseledets.finrank_cocycleKer: the rank–nullity identity finrank (cocycleKer A T n x) = d - (cocycle A T n x).rank — the kernel dimension is the corank of the n-step cocycle.

Remaining gap toward the full singular filtration

This module supplies the bottom of the flag at finite time: a single monotone family of kernel submodules with its dimension. The full Quas Theorem 2 conclusion additionally requires (i) the singular-value exponents λ₁ > ⋯ > λ_k from the Kingman/exterior-power machinery, (ii) the limiting slow spaces V_j(ω) = lim_n (span of the smallest singular vectors of cocycle A T n x) as a Cauchy sequence in the Grassmannian, and (iii) their measurability and equivariance A_ω V_j(ω) ⊆ V_j(σ ω)`. None of (i)–(iii) is formalized here; only the algebraic kernel/corank data is.

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

The kernel submodule of the n-step cocycle: the directions in ℝ^d (here Fin d → ℝ) collapsed to 0 by cocycle A T n x. In the non-invertible Oseledets theorem (Quas, Multiplicative Ergodic Theorems and Applications, 2013, Theorem 2; after Oseledec and Raghunathan) the eventual such kernel is the bottom of the singular filtration flag ℝ^d = V₁(ω) ⊃ ⋯ ⊃ {0}.

Equations

• Oseledets.cocycleKer A T n x = (Oseledets.cocycle A T n x).mulVecLin.ker

theorem Oseledets.mem_cocycleKer {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X → X} {n : ℕ} {x : X} {v : Fin d → ℝ} : v ∈ cocycleKer A T n x ↔ (cocycle A T n x).mulVec v = 0

Vector-level membership in the cocycle kernel: v is collapsed iff the matrix-vector product A⁽ⁿ⁾(x) ·ᵥ v vanishes. The bridge from the submodule to a usable pointwise condition.

@[simp]

theorem Oseledets.cocycleKer_zero {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) : cocycleKer A T 0 x = ⊥

The zero-step cocycle is the identity, so its kernel is trivial.

theorem Oseledets.cocycleKer_le_add {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (m n : ℕ) (x : X) : cocycleKer A T n x ≤ cocycleKer A T (m + n) x

Kernel monotonicity along the orbit. The kernel of the n-step cocycle is contained in the kernel of the (m + n)-step cocycle: once a direction is collapsed by cocycle A T n x it stays collapsed under the later block cocycle A T m (T^[n] x), so the kernel can only grow as the cocycle composes. This is the monotone bottom stratum of the singular Oseledets filtration.

theorem Oseledets.finrank_cocycleKer {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) : Module.finrank ℝ ↥(cocycleKer A T n x) = d - (cocycle A T n x).rank

Rank–nullity for the cocycle kernel. The kernel dimension is the corank of the n-step cocycle: finrank (cocycleKer A T n x) = d - (cocycle A T n x).rank.