Submatrix-robust matrices exist

A square block of an m × m matrix over GF(2) with k rows and rank r has r columns spanning all of its columns. So it is determined by those columns, the subsets of them that sum to each other column, and the entries outside the remaining k × (k - r) block. Counting these descriptions, at most 2^{m² - (k - r)²} matrices are deficient by k - r on a given set of rows and columns of size k with a given spanning set. A union bound over the < 2^{3m} choices shows that when (t + 1)² > 3m, some matrix has every square block of rank at least k - t. The deficiency t = 2 ⌊√m⌋ + 1 qualifies.

def Complexity.Correlation.colVec {m : ℕ} (R : Matrix (Fin m) (Fin m) (ZMod 2)) (S : Set (Fin m)) (j : Fin m) : ↑S → ZMod 2

The column j of R, restricted to the rows S.

Equations

• Complexity.Correlation.colVec R S j i = R (↑i) j

theorem Complexity.Correlation.exists_spanning_columns {m : ℕ} (R : Matrix (Fin m) (Fin m) (ZMod 2)) (S T : Finset (Fin m)) : ∃ T' ⊆ T, T'.card = blockRank R ↑S ↑T ∧ ∀ j ∈ T, colVec R (↑S) j ∈ Submodule.span (ZMod 2) (colVec R ↑S '' ↑T')

Column bases. The columns of a block contain a spanning set of the block's rank.

noncomputable def Complexity.Correlation.spannedBy {m : ℕ} (S T T' : Finset (Fin m)) : Finset (Matrix (Fin m) (Fin m) (ZMod 2))

The matrices whose columns in T, restricted to the rows S, lie in the span of their columns in T'.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.Correlation.spanCoeff {m : ℕ} (R : Matrix (Fin m) (Fin m) (ZMod 2)) (S T' : Finset (Fin m)) (j : Fin m) : ↥T' → ZMod 2

Chosen coefficients expressing a column in terms of the columns in T'.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.Correlation.spanCoeff_spec {m : ℕ} {R : Matrix (Fin m) (Fin m) (ZMod 2)} {S T' : Finset (Fin m)} {j : Fin m} (h : colVec R (↑S) j ∈ Submodule.span (ZMod 2) (colVec R ↑S '' ↑T')) : ∑ l : ↥T', spanCoeff R S T' j l • colVec R ↑S ↑l = colVec R (↑S) j

theorem Complexity.Correlation.card_spannedBy_mul_le {m : ℕ} (S T T' : Finset (Fin m)) : (spannedBy S T T').card * 2 ^ (S.card * (T \ T').card) ≤ 2 ^ ((T \ T').card * T'.card) * 2 ^ (m * m)

Counting spanned matrices. A matrix in spannedBy S T T' is determined by the coefficients for the columns in T \ T' and by its entries outside S × (T \ T').

noncomputable def Complexity.Correlation.deficientOn {m : ℕ} (t : ℕ) (S T : Finset (Fin m)) : Finset (Matrix (Fin m) (Fin m) (ZMod 2))

The matrices with a deficient square block on the rows S and the columns T.

Equations

• Complexity.Correlation.deficientOn t S T = {R : Matrix (Fin m) (Fin m) (ZMod 2) | S.card = T.card ∧ Complexity.Correlation.blockRank R ↑S ↑T + t < S.card}

theorem Complexity.Correlation.card_deficientOn_mul_le {m : ℕ} (t : ℕ) (S T : Finset (Fin m)) : (deficientOn t S T).card * 2 ^ (t + 1) ^ 2 ≤ 2 ^ m * 2 ^ (m * m)

Each block is deficient for at most a 2^{m - (t+1)²} fraction of all matrices.

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

Existence by counting. If 3m < (t + 1)², some m × m matrix over GF(2) is submatrix-robust with deficiency t.

theorem Complexity.Correlation.three_mul_lt_robustDeficiency_add_one_sq (m : ℕ) : 3 * m < (robustDeficiency m + 1) ^ 2