Submatrix-robust matrices

A matrix is submatrix-robust with deficiency t (Matrix.SubmatrixRobust) when every square block of it, with k rows and k columns, has rank at least k - t; then every block has rank at least its smaller side minus t (Matrix.SubmatrixRobust.min_le).

Existence by counting (Matrix.exists_submatrixRobust). A square block of an m × m matrix over 𝔽₂ with k rows and rank r has r columns spanning all of its columns. So the matrix is determined by those columns, the coefficients expressing each other column of the block in terms of them, and its entries outside the remaining k × (k - r) block. Counting these descriptions, at most 2 ^ (m² - (k - r)²) matrices are deficient by k - r on given sets of rows and columns with a given spanning set. A union bound over the fewer than 2 ^ (3 m) choices shows that some matrix has every square block of rank at least k - t once (t + 1)² > 3 m. The deficiency t = 2 ⌊√m⌋ + 1 qualifies.

Cut ranks of bilinear forms (Matrix.SubmatrixRobust.le_cutRank_add). Place a robust k × k matrix R on a block of a square matrix M whose rows and columns are disjoint sets of indices, with zeros elsewhere, so that the quadratic form of M is a bilinear form xᵀ R y. A set U of indices cuts the rows of R into x ∩ U and x \ U, and its columns likewise; the block of the polar matrix M + Mᵀ with rows U and columns Uᶜ contains, on disjoint sets of columns, the block of R with rows x ∩ U and columns y \ U and the transpose of the block with rows x \ U and columns y ∩ U (Matrix.add_blockRank_le_cutRank_add_transpose). If there are at most 2 k + 1 indices and |U| = k, the two blocks have total rank at least k - 1 - 2 t.

Main definitions

• Matrix.SubmatrixRobust M t: every square block of M with k rows has rank at least k - t.

Main results

• Matrix.SubmatrixRobust.min_le: every block of a robust matrix has nearly full rank.
• Matrix.exists_submatrixRobust_of_lt, Matrix.exists_submatrixRobust: robust matrices over 𝔽₂ exist, by counting.
• Matrix.add_blockRank_le_cutRank_add_transpose: the cut rank of a bilinear form.
• Matrix.SubmatrixRobust.le_cutRank_add: bisections of a robust bilinear form have nearly full cut rank.

def Matrix.SubmatrixRobust {m : Type u_1} {n : Type u_2} {K : Type u_6} [Field K] (M : Matrix m n K) (t : ℕ) : Prop

M is submatrix-robust with deficiency t: every square block of M, with k rows and k columns, has rank at least k - t.

theorem Matrix.SubmatrixRobust.mono {m : Type u_1} {n : Type u_2} {K : Type u_6} [Field K] {M : Matrix m n K} {t t' : ℕ} (hM : M.SubmatrixRobust t) (ht : t ≤ t') : M.SubmatrixRobust t'

A larger deficiency is weaker.

theorem Matrix.SubmatrixRobust.min_le {m : Type u_1} {n : Type u_2} {K : Type u_6} [Field K] [Finite n] {M : Matrix m n K} {t : ℕ} (hM : M.SubmatrixRobust t) (S : Set m) (T : Set n) : min S.ncard T.ncard ≤ M.blockRank S T + t

Every block of a robust matrix has rank at least its smaller side minus the deficiency.

Existence by counting

theorem Matrix.exists_submatrixRobust_of_lt {k t : ℕ} (ht : 3 * k < (t + 1) ^ 2) : ∃ (R : Matrix (Fin k) (Fin k) (ZMod 2)), R.SubmatrixRobust t

Robust matrices exist, by counting. If 3 k < (t + 1)², some k × k matrix over 𝔽₂ is submatrix-robust with deficiency t.

theorem Matrix.exists_submatrixRobust (k : ℕ) : ∃ (R : Matrix (Fin k) (Fin k) (ZMod 2)), R.SubmatrixRobust (2 * k.sqrt + 1)

Robust matrices exist. For every k, some k × k matrix over 𝔽₂ has every square block with j rows of rank at least j - (2 ⌊√k⌋ + 1).

Cut ranks of bilinear forms

theorem Matrix.add_blockRank_le_cutRank_add_transpose {ι : Type u_3} {κ : Type u_4} {κ' : Type u_5} {K : Type u_6} [Field K] [Finite ι] {R : Matrix κ κ' K} {M : Matrix ι ι K} {f : κ → ι} {g : κ' → ι} (hf : Function.Injective f) (hg : Function.Injective g) (hfg : Disjoint (Set.range f) (Set.range g)) (hMR : M.submatrix f g = R) (hM : ∀ (i j : ι), i ∉ Set.range f ∨ j ∉ Set.range g → M i j = 0) (U : Set ι) : R.blockRank (f ⁻¹' U) (g ⁻¹' Uᶜ) + R.blockRank (f ⁻¹' Uᶜ) (g ⁻¹' U) ≤ (M + M.transpose).cutRank U

The cut rank of a bilinear form. Let f and g place the rows and the columns of R injectively among the indices of a square matrix M, with disjoint ranges, and let M carry R on that block and vanish elsewhere. Then at every set U of indices, the cut rank of the polar matrix M + Mᵀ is at least the rank of the block of R with rows f⁻¹ U and columns g⁻¹ Uᶜ plus the rank of the block with rows f⁻¹ Uᶜ and columns g⁻¹ U.

theorem Matrix.SubmatrixRobust.le_cutRank_add {ι : Type u_3} {K : Type u_6} [Field K] [Finite ι] {k t : ℕ} {R : Matrix (Fin k) (Fin k) K} (hR : R.SubmatrixRobust t) {M : Matrix ι ι K} {f g : Fin k → ι} (hf : Function.Injective f) (hg : Function.Injective g) (hfg : Disjoint (Set.range f) (Set.range g)) (hMR : M.submatrix f g = R) (hM : ∀ (i j : ι), i ∉ Set.range f ∨ j ∉ Set.range g → M i j = 0) (hι : Nat.card ι ≤ 2 * k + 1) {U : Set ι} (hU : U.ncard = k) : k ≤ (M + M.transpose).cutRank U + (2 * t + 1)

Bisections of a robust bilinear form. Let M carry a k × k matrix R that is submatrix-robust with deficiency t on a block whose rows and columns are disjoint sets of indices, and vanish elsewhere, with at most 2 k + 1 indices in all. Then every set U of k indices has cut rank at least k - (2 t + 1) in the polar matrix M + Mᵀ.