sauer_shelah_card_le_mul_pow

theoremverifiedoriginal

Polynomial 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 𝒜 is at most d, then |𝒜| ≤ (d + 1)·n^d.

Statement

theorem sauer_shelah_card_le_mul_pow {α : Type*} [Fintype α] [DecidableEq α] (𝒜 : Finset (Finset α))
    (d : ℕ) (hn : 1 ≤ Fintype.card α) (h : 𝒜.vcDim ≤ d) :
    𝒜.card ≤ (d + 1) * (Fintype.card α) ^ d

Source

Corollary of the Sauer–Shelah lemma (Sauer 1972; Shelah 1972); KB node sauer_shelah_card_le_sum_choose and Mathlib's Finset.card_shatterer_le_sum_vcDim. This polynomial growth-function form is the one standard in statistical learning theory (the `learning` topic of this domain is empty).

Verified

10 Sep 2026

Axioms

Classical.choiceQuot.soundpropext

Built on 1

sauer_shelah_card_le_sum_chooseSauer-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…

Read back from the Lean

For every type α equipped with a Fintype instance and a DecidableEq instance, for every finite family 𝒜 : Finset (Finset α) and every natural number d, if α is nonempty (1 ≤ Fintype.card α) and the VC dimension of 𝒜 is at most d, then the number of sets in 𝒜 is at most (d + 1) · (Fintype.card α)^d. In explicit quantifier order: ∀ {α : Type*} [Fintype α] [DecidableEq α], ∀ (𝒜 : Finset (Finset α)) (d : ℕ), 1 ≤ Fintype.card α → 𝒜.vcDim ≤ d → 𝒜.card ≤ (d + 1) * (Fintype.card α)^d. The typeclass arguments restrict α to finite types with decidable equality. The two explicit hypotheses are exactly: α is nonempty, and the VC dimension of 𝒜 is bounded by d. The conclusion is a non-strict inequality in ℕ, giving the coarse Sauer–Shelah-style bound (d + 1) times |α|^d.

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

/-- Polynomial form of Sauer–Shelah: a set family of VC-dimension at most d on n ≥ 1 points has at most (d+1)·n^d members. -/
theorem sauer_shelah_card_le_mul_pow {α : Type*} [Fintype α] [DecidableEq α] (𝒜 : Finset (Finset α))
    (d : ℕ) (hn : 1 ≤ Fintype.card α) (h : 𝒜.vcDim ≤ d) :
    𝒜.card ≤ (d + 1) * (Fintype.card α) ^ d := by
  calc 𝒜.card ≤ ∑ k ∈ Finset.Iic d, (Fintype.card α).choose k :=
        sauer_shelah_card_le_sum_choose 𝒜 d h
    _ ≤ ∑ k ∈ Finset.Iic d, (Fintype.card α) ^ k :=
        Finset.sum_le_sum (fun k _ => Nat.choose_le_pow (Fintype.card α) k)
    _ ≤ (d + 1) * (Fintype.card α) ^ d := by
        have hs := Finset.sum_le_card_nsmul (Finset.Iic d)
          (fun k => (Fintype.card α) ^ k) ((Fintype.card α) ^ d) ?_
        · simp only [smul_eq_mul] at hs
          simpa using hs
        · intro k hk
          simp only [Finset.mem_Iic] at hk
          exact Nat.pow_le_pow_right hn hk

Discuss this result Challenge it