Sauer-Shelah for binary matrices #
Quantitative binomial-sum bound on the number of distinct rows in a binary
matrix, derived from Mathlib's Finset.card_shatterer_le_sum_vcDim.
theorem
BinaryMatrix.card_toFinsetFamily_le
{m n : ℕ}
(M : BinaryMatrix m n)
{d : ℕ}
(hd : M.toFinsetFamily.vcDim ≤ d)
:
Sauer-Shelah for binary matrices: the number of distinct rows in
the Finset family is bounded by ∑ k ∈ Iic d, n.choose k whenever the VC
dimension is at most d.