Compatibility import: VC dimension #
The implementation lives in FormalSLT.VC.Dimension. This alias preserves the
earlier verbose namespace and import path.
theorem
FormalSLT.VC.VCDimension.sauerShelahFiniteSetFamily
{α : Type u_1}
[DecidableEq α]
[Fintype α]
(𝒜 : Finset (Finset α))
:
Alias of FormalSLT.VC.Dimension.sauerShelahFiniteSetFamily.
Sauer-Shelah lemma for finite set families, binomial-sum form.
This claim-facing wrapper is the finite combinatorial core behind the
vc-dimension page's growth-function statement. A hypothesis class restricted
to a fixed finite sample is represented as a finite family of subsets of the
sample. Mathlib's Finset.card_le_card_shatterer gives Pajor's trace bound,
and Finset.card_shatterer_le_sum_vcDim gives the Sauer-Shelah binomial
bound in terms of the VC dimension of that finite family.