Binary matrices: shattering, transpose, VC dimension

Basic definitions for BinaryMatrix m n := Fin m → Fin n → Bool: the row-centric shatters predicate, transpose, the Finset-family view, and VC dimension via Mathlib's Finset.vcDim.

@[reducible, inline]

abbrev BinaryMatrix (m n : ℕ) : Type

An m × 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

M shatters a column set S if every subset t ⊆ S arises as the set of true columns within S for some row.

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