Assouad's dual VC bound

If a binary matrix M has VC dimension at most d, then its transpose has VC dimension at most 2^(d+1) - 1. Proof by the bitstring coding argument (Assouad 1983): from a shattered set of size 2^(d+1) in Mᵀ, extract d + 1 shattered columns of M, contradicting M.vcDim ≤ d.

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): M.vcDim ≤ d implies M.transpose.vcDim ≤ 2^(d+1) - 1.