The nonsingular-minor characterisation of rank, and the measurable rank flag

For the singular (non-invertible) multiplicative ergodic theorem the Oseledets decomposition degenerates to a measurable filtration ℝ^d = V₁(x) ⊃ V₂(x) ⊃ ⋯ ⊃ {0}, whose strata carry the dimension data (the multiplicities m_j) of the flag (A. Quas, Multiplicative Ergodic Theorems and Applications, lecture notes, Universidade de São Paulo, December 2013, Theorem 2 — the non-invertible Oseledets theorem after Oseledec [12] and Raghunathan [13]: in the non-invertible case the conclusion is a measurable filtration rather than a direct-sum decomposition). Assembling that measurable flag requires the dimension function x ↦ cocycleRank A T n x to be measurable, which rests on the determinantal characterisation of rank via minors.

Oseledets.Lyapunov.Extensions.SingularRankMeasurable2 supplied the easy half of that characterisation — a nonsingular r × r minor forces r ≤ M.rank (Matrix.le_rank_of_submatrix_det_ne_zero) — and exhibited the union of the nonsingular-minor sets as a measurable subset of {x | r ≤ cocycleRank A T n x}.

This file proves the classical hard half, absent from Mathlib:

r ≤ M.rank ⇒ ∃ s t : Fin r → n, (M.submatrix s t).det ≠ 0,

i.e. a matrix of rank at least r has a nonsingular r × r minor. Combined with the easy half it gives the full minor characterisation r ≤ M.rank ↔ ∃ s t, (M.submatrix s t).det ≠ 0, which upgrades the subset above to a set equality, yielding MeasurableSet {x | r ≤ cocycleRank A T n x}, then the measurability of the dimension function cocycleRank A T n and of the eventual-kernel dimension x ↦ d - ⨅ n, cocycleRank A T n x — the dimension datum of the measurable flag.

The classical proof of the hard half

The standard linear-algebra argument (chosen here because every step is supported by the Mathlib API):

1. M.rank is the dimension of the column span (rank_eq_finrank_span_cols); from a finite family whose span has dimension ≥ r one can select an injective family of r indices on which the family is linearly independent (Matrix.exists_submatrix_id_rank_eq, built from exists_linearIndependent' and finrank_span_eq_card). This produces t : Fin r → n with the tall m × r submatrix M.submatrix id t of rank r.
2. Applying the same column selection to the transpose of that tall submatrix selects r independent rows, giving s : Fin r → m so that the square r × r minor M.submatrix s t again has rank r.
3. A square matrix of full rank has nonzero determinant (Matrix.rank_eq_card_iff_det_ne_zero).

Main results

• Matrix.exists_submatrix_id_rank_eq: rank ≥ r selects t : Fin r → n with the tall column-submatrix M.submatrix id t of rank exactly r.
• Matrix.exists_submatrix_det_ne_zero_of_le_rank: the missing lemma — rank ≥ r yields a nonsingular r × r minor.
• Matrix.le_rank_iff_exists_submatrix_det_ne_zero: the full minor characterisation of rank (both directions).
• Oseledets.measurableSet_le_cocycleRank: {x | r ≤ cocycleRank A T n x} is measurable.
• Oseledets.measurable_cocycleRank: the cocycle-rank dimension function is measurable.

theorem Matrix.exists_submatrix_id_rank_eq {m : Type u_1} {n : Type u_2} {R : Type u_3} [Field R] [Finite m] [Fintype n] {r : ℕ} (M : Matrix m n R) (hr : r ≤ M.rank) : ∃ (t : Fin r → n), (M.submatrix id t).rank = r

Column selection from a rank bound. If r ≤ M.rank then there is an injective selection t : Fin r → n of r columns of M whose tall m × r submatrix M.submatrix id t has rank exactly r.

Proof: M.rank equals the dimension of the column span (rank_eq_finrank_span_cols). From the column family M.col : n → (m → R), exists_linearIndependent' selects an injective a : κ → n indexing a linearly independent subfamily with the same span, hence (finrank_span_eq_card) Fintype.card κ = M.rank ≥ r; choosing an injection Fin r ↪ κ and composing gives t. The columns of M.submatrix id t are exactly M.col ∘ t, a linearly independent Fin r-family, so the submatrix's rank is r.

theorem Matrix.exists_submatrix_det_ne_zero_of_le_rank {m : Type u_1} {n : Type u_2} {R : Type u_3} [Field R] [Finite m] [Fintype n] {r : ℕ} (M : Matrix m n R) (hr : r ≤ M.rank) : ∃ (s : Fin r → m) (t : Fin r → n), (M.submatrix s t).det ≠ 0

The missing nonsingular-minor lemma (classical hard half of the minor characterisation of rank). If r ≤ M.rank, then some r × r minor of M is nonsingular: there exist s t : Fin r → n with (M.submatrix s t).det ≠ 0.

Proof. First select r independent columns: exists_submatrix_id_rank_eq gives t : Fin r → n with the tall submatrix N := M.submatrix id t of rank r. The transpose Nᵀ has the same rank r (rank_transpose); selecting r independent columns of Nᵀ (again exists_submatrix_id_rank_eq) gives s : Fin r → m with (Nᵀ.submatrix id s).rank = r. That selection is the square minor M.submatrix s t up to transpose, and a square matrix of full rank has nonzero determinant (rank_eq_card_iff_det_ne_zero). The converse — a nonsingular minor forcing r ≤ M.rank — is Matrix.le_rank_of_submatrix_det_ne_zero.

theorem Matrix.le_rank_iff_exists_submatrix_det_ne_zero {n : Type u_2} {R : Type u_3} [Field R] [Fintype n] {r : ℕ} (M : Matrix n n R) : r ≤ M.rank ↔ ∃ (s : Fin r → n) (t : Fin r → n), (M.submatrix s t).det ≠ 0

The minor characterisation of rank. For a square matrix over a field, r ≤ M.rank iff some r × r minor is nonsingular. The forward direction is the hard exists_submatrix_det_ne_zero_of_le_rank; the reverse is the easy le_rank_of_submatrix_det_ne_zero.

theorem Oseledets.measurableSet_le_cocycleRank {X : Type u_1} {d : ℕ} [MeasurableSpace X] {r : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : Measurable A) {T : X → X} (hT : Measurable T) (n : ℕ) : MeasurableSet {x : X | r ≤ cocycleRank A T n x}

The rank level set is measurable. For a measurable matrix family A and a measurable base map T, the set {x | r ≤ cocycleRank A T n x} is measurable.

By the minor characterisation of rank (Matrix.le_rank_iff_exists_submatrix_det_ne_zero) this set equals the finite union over all minor selections of the measurable nonsingular-minor sets {x | ((cocycle A T n x).submatrix s t).det ≠ 0} (measurableSet_minor_det_ne_zero). This is the level set whose differences cut out the strata of the singular measurable filtration.

theorem Oseledets.measurable_cocycleRank {X : Type u_1} {d : ℕ} [MeasurableSpace X] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : Measurable A) {T : X → X} (hT : Measurable T) (n : ℕ) : Measurable fun (x : X) => cocycleRank A T n x

The cocycle-rank dimension function is measurable. The dimension datum x ↦ cocycleRank A T n x of the singular flag is measurable: a ℕ-valued function is measurable once every fibre {x | f x = k} is measurable, and each fibre is the difference {x | k ≤ f x} \ {x | k + 1 ≤ f x} of the (measurable) rank level sets from measurableSet_le_cocycleRank.