sauer_shelah_card_le_sum_choose
Sauer-Shelah lemma: let α be a finite set with n elements and let A be a finite family of subsets of α. If the VC-dimension of A, that is the largest size of a set s such that every subset of s occurs as s ∩ u for some u ∈ A, is at most d, then A has at most ∑_{k=0}^{d} binom(n,k) members.
Statement
theorem sauer_shelah_card_le_sum_choose {α : Type*} [Fintype α] [DecidableEq α] (𝒜 : Finset (Finset α)) (d : ℕ) (h : 𝒜.vcDim ≤ d) : 𝒜.card ≤ ∑ k ∈ Finset.Iic d, (Fintype.card α).choose k
- Source
- Sauer (1972), Shelah (1972), Vapnik-Chervonenkis (1971); VC dimension as in Mathlib's `Finset.Shatters` / `Finset.vcDim` (Mathlib/Combinatorics/SetFamily/Shatter.lean). Mathlib only proves the weaker bound `Finset.card_shatterer_le_sum_vcDim`, which bounds the *shatterer* of the family, not the family itself.
- Verified
- 10 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Used by 1
- sauer_shelah_card_le_mul_powPolynomial form of the Sauer–Shelah lemma. Let 𝒜 be a finite family of subsets of a finite set α with n = |α| ≥ 1. If the VC-dimension of…
Read back from the Lean
Let α be any type equipped with a Fintype instance and a DecidableEq instance (so α is finite and has decidable equality). Let 𝒜 be a Finset of Finsets of α — i.e. a finite, duplicate-free family of finite subsets of α, so |𝒜| counts distinct subsets. Let d be a natural number, and assume the hypothesis h : 𝒜.vcDim ≤ d, i.e. that the VC dimension of the family 𝒜 is at most d. The conclusion is: 𝒜.card ≤ ∑ k ∈ Finset.Iic d, (Fintype.card α).choose k that is, the number of distinct subsets in the family 𝒜 is at most the sum, over all natural numbers k with k ≤ d, of the binomial coefficient (|α| choose k). This is the Sauer–Shelah bound: a family of subsets of an n-element set whose VC dimension is at most d contains at most Σ_{k=0}^{d} C(n, k) sets. Quantifiers and hypotheses, in order: ∀ (α : Type) [Fintype α] [DecidableEq α] (𝒜 : Finset (Finset α)) (d : ℕ), (𝒜.vcDim ≤ d) → (𝒜.card ≤ Σ_{k=0}^{d} C(|α|, k)). The Fintype and DecidableEq instances are hypotheses too: the theorem only applies to finite types with decidable equality, and α is universally quantified (together with its instances), not fixed.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- Sauer-Shelah lemma: a set family of VC-dimension at most `d` on an `n`-element ground set has at most `∑_{k ≤ d} n.choose k` members. -/ theorem sauer_shelah_card_le_sum_choose {α : Type*} [Fintype α] [DecidableEq α] (𝒜 : Finset (Finset α)) (d : ℕ) (h : 𝒜.vcDim ≤ d) : 𝒜.card ≤ ∑ k ∈ Finset.Iic d, (Fintype.card α).choose k := by calc 𝒜.card ≤ 𝒜.shatterer.card := Finset.card_le_card_shatterer 𝒜 _ ≤ ∑ k ∈ Finset.Iic 𝒜.vcDim, (Fintype.card α).choose k := Finset.card_shatterer_le_sum_vcDim _ ≤ ∑ k ∈ Finset.Iic d, (Fintype.card α).choose k := by apply Finset.sum_le_sum_of_subset_of_nonneg · exact Finset.Iic_subset_Iic.2 h · intro k _ _ positivity