Binary Matrix VC Dimension and Sauer-Shelah

Pure combinatorics: VC dimension on binary matrices, bridged to Mathlib's Finset.Shatters infrastructure. No learning theory types.

@[reducible, inline]

abbrev BinaryMatrix (m n : ℕ) : Type

An m x n binary matrix, represented as Fin m -> Fin n -> Bool.

Equations

• BinaryMatrix m n = (Fin m → Fin n → Bool)

def BinaryMatrix.shatters {m n : ℕ} (M : BinaryMatrix m n) (S : Finset (Fin n)) : Prop

A binary matrix M shatters a column set S if for every subset t ⊆ S, there is a row i whose true columns within S are exactly t.

Equations

• M.shatters S = ∀ t ⊆ S, ∃ (i : Fin m), ∀ j ∈ S, M i j = true ↔ j ∈ t

def BinaryMatrix.transpose {m n : ℕ} (M : BinaryMatrix m n) : BinaryMatrix n m

Transpose of a binary matrix.

Equations

• M.transpose j i = M i j

def BinaryMatrix.toFinsetFamily {m n : ℕ} (M : BinaryMatrix m n) : Finset (Finset (Fin n))

Convert a binary matrix to a Finset family: each row becomes the set of columns where that row is true.

Equations

• M.toFinsetFamily = Finset.image (fun (i : Fin m) => {j : Fin n | M i j = true}) Finset.univ

noncomputable def BinaryMatrix.vcDim {m n : ℕ} (M : BinaryMatrix m n) : ℕ

The VC dimension of a binary matrix, defined via the Mathlib Finset family.

Equations

• M.vcDim = M.toFinsetFamily.vcDim

theorem BinaryMatrix.shatters_iff {m n : ℕ} (M : BinaryMatrix m n) (S : Finset (Fin n)) : M.shatters S ↔ M.toFinsetFamily.Shatters S

Our shatters coincides with Mathlib's Finset.Shatters on the associated family.

theorem BinaryMatrix.bool_fun_eq_of_filter_eq {n : ℕ} (f g : Fin n → Bool) (h : {j : Fin n | f j = true} = {j : Fin n | g j = true}) : f = g

Two Bool-valued functions on Fin n that agree on which indices are true (as witnessed by equal univ.filter) are equal.

theorem BinaryMatrix.card_toFinsetFamily_le {m n : ℕ} (M : BinaryMatrix m n) {d : ℕ} (hd : M.toFinsetFamily.vcDim ≤ d) : M.toFinsetFamily.card ≤ ∑ k ∈ Finset.Iic d, n.choose k

Sauer-Shelah lemma for binary matrices: the number of distinct rows in the Finset family is bounded by the sum of binomial coefficients up to the VC dimension.

Assouad's Dual VC Bound for Matrices

If M has VC dimension ≤ d, then M.transpose has VC dimension ≤ 2^(d+1) - 1.

The proof uses the bitstring coding argument: index 2^(d+1) shattered rows by Fin (d+1) → Bool, extract d+1 columns via coordinate projections, and show these columns are shattered by M.

theorem BinaryMatrix.transpose_shatters_imp_shatters {m n : ℕ} (M : BinaryMatrix m n) {d : ℕ} (S : Finset (Fin m)) (hS : M.transpose.shatters S) (hcard : 2 ^ (d + 1) ≤ S.card) : ∃ (T : Finset (Fin n)), T.card = d + 1 ∧ M.shatters T

Auxiliary: if M.transpose shatters S ⊆ Fin m with |S| ≥ 2^(d+1), then M shatters some set of d+1 columns.

theorem BinaryMatrix.assouad_transpose_vcDim {m n : ℕ} (M : BinaryMatrix m n) {d : ℕ} (hd : M.vcDim ≤ d) : M.transpose.vcDim ≤ 2 ^ (d + 1) - 1

Assouad's dual VC bound (matrix form): if M has VC dimension ≤ d, then M.transpose has VC dimension ≤ 2^(d+1) - 1.

This is the fundamental bridge between primal and dual shattering. Proved via the bitstring coding argument (Assouad 1983).