Bitstring coding: transpose-shattering implies column-shattering

Assouad's technique for the dual VC bound: if the transpose Mᵀ shatters a set S with |S| ≥ 2^(d+1), then M itself shatters a column set of size d + 1. Each row is encoded as a bitstring over d+1 distinguished columns, extracted via Mᵀ-shattering of the coordinate projections.

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

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