Mathesis

Dhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z

DeclHasVCDimLE.vcGrowth_le_exp

∀ {α : Type u_1} {n d : ℕ} {𝒜 : Set (Set α)}, HasVCDimLE d 𝒜 → d ≤ n → ↑(vcGrowth n 𝒜) ≤ (Real.exp 1 / ↑d * ↑n) ^ d

TopicTraces and shattering

ThesisStepHypothesisDefinitionCited result

DeclHasVCDimLE.vcGrowth_le_expDeclaration kindtheorem

∀ {α : Type u_1} {n d : ℕ} {𝒜 : Set (Set α)}, HasVCDimLE d 𝒜 → d ≤ n → ↑(vcGrowth n 𝒜) ≤ (Real.exp 1 / ↑d * ↑n) ^ d

HasVCDimLE vcGrowth

Uses

HasVCDimLE.vcGrowth_le_sum_range
sum_choose_le_exp_pow

Declsum_choose_le_exp_powDeclaration kindtheorem
```
∀ (d m : ℕ), 0 < d → d ≤ m → ∑ i ∈ Finset.range (d + 1), ↑(m.choose i) ≤ (Real.exp 1 / ↑d * ↑m) ^ d
```
Uses
Used by
- HasVCDimLE.vcGrowth_le_exp
Declsum_choose_mul_pow_le_add_one_powDeclaration kindtheorem
Truncating a binomial expansion at degree d can only decrease it, for t ≥ 0.
```
∀ {m d : ℕ} {t : ℝ}, 0 ≤ t → d ≤ m → ∑ i ∈ Finset.range (d + 1), ↑(m.choose i) * t ^ i ≤ (1 + t) ^ m
```
Used by
- sum_choose_le_exp_pow

Declsum_choose_le_mul_sum_choose_mul_powDeclaration kindtheorem

Undoing the weighting t ^ i costs a single factor (m / d) ^ d, since t = d / m and each i in range is at most d.

∀ {m d : ℕ},
  0 < ↑d →
    0 < ↑m →
      ↑d ≤ ↑m →
        ∑ i ∈ Finset.range (d + 1), ↑(m.choose i) ≤
          (↑m / ↑d) ^ d * ∑ i ∈ Finset.range (d + 1), ↑(m.choose i) * (↑d / ↑m) ^ i

Used by

sum_choose_le_exp_pow

Declone_add_div_pow_le_exp_powDeclaration kindtheorem
At t = d / m, the binomial base is bounded by exp 1 raised to the degree.
```
∀ {m d : ℕ}, 0 < ↑m → (1 + ↑d / ↑m) ^ m ≤ Real.exp 1 ^ d
```
Used by
- sum_choose_le_exp_pow
DeclHasVCDimLE.vcGrowth_le_sum_rangeDeclaration kindtheorem
The Sauer-Shelah inequality, with the sum indexed by Finset.range (d + 1).
```
∀ {α : Type u_1} {n d : ℕ} {𝒜 : Set (Set α)}, HasVCDimLE d 𝒜 → vcGrowth n 𝒜 ≤ ∑ k ∈ Finset.range (d + 1), n.choose k
```
HasVCDimLE vcGrowth
Uses
- HasVCDimLE.vcGrowth_le
Used by
- HasVCDimLE.vcGrowth_le_exp
DeclHasVCDimLE.vcGrowth_leDeclaration kindtheorem
```
∀ {α : Type u_1} {n d : ℕ} {𝒜 : Set (Set α)}, HasVCDimLE d 𝒜 → vcGrowth n 𝒜 ≤ ∑ k ∈ Finset.Iic d, n.choose k
```
HasVCDimLE vcGrowth vcGrowth_le_iff
Uses
- HasVCDimLE.ncard_image_inter_le
Used by
- HasVCDimLE.vcGrowth_le_sum_range
DeclHasVCDimLE.ncard_image_inter_leDeclaration kindtheorem
The Sauer-Shelah inequality: a family of VC dimension at most d traces at most ∑ k ≤ d, n.choose k sets on any finite set of size at most n. The proof here derives it from Pajor's inequality.
Simon, A Guide to NIP Theories, states the same bound as his Lemma 6.4, for the growth function of a class of VC dimension at most k, and records in the notes to that chapter that the lemma is implicit in Vapnik and Chervonenkis (1971) and was rediscovered independently by Shelah (1972) and by Sauer (1972). Dvir, Filmus and Moran state it in the introduction to A Sauer-Shelah-Perles Lemma for Lattices and cite the same three sources. Perles is carried in the name they give the lemma; a publication of his is cited by neither source.
```
∀ {α : Type u_1} {n d : ℕ} {𝒜 : Set (Set α)} {A : Set α},
  HasVCDimLE d 𝒜 → A.Finite → A.ncard ≤ n → ((fun x => A ∩ x) '' 𝒜).ncard ≤ ∑ k ∈ Finset.Iic d, n.choose k
```
HasVCDimLE Shatters
Uses
Used by
- HasVCDimLE.vcGrowth_le
Declncard_setOf_ncard_leDeclaration kindtheorem
```
∀ {α : Type u_1} {A : Set α},
  A.Finite → ∀ (d : ℕ), {B | B ⊆ A ∧ B.ncard ≤ d}.ncard = ∑ k ∈ Finset.Iic d, A.ncard.choose k
```
Uses
Used by
- HasVCDimLE.ncard_image_inter_le

DeclsetOf_subset_and_ncard_le_zeroDeclaration kindtheorem

∀ {α : Type u_1} {A : Set α}, A.Finite → {B | B ⊆ A ∧ B.ncard ≤ 0} = {∅}

Used by

ncard_setOf_ncard_le

DeclsetOf_subset_and_ncard_le_succDeclaration kindtheorem
The subsets of A of size at most d + 1 split into those of size at most d and those of size exactly d + 1.
```
∀ {α : Type u_1} (d : ℕ) (A : Set α),
  {B | B ⊆ A ∧ B.ncard ≤ d + 1} = {B | B ⊆ A ∧ B.ncard ≤ d} ∪ {B | B ⊆ A ∧ B.ncard = d + 1}
```
Used by
- ncard_setOf_ncard_le

Decldisjoint_setOf_ncard_le_setOf_ncard_eqDeclaration kindtheorem

∀ {α : Type u_1} (d : ℕ) (A : Set α), Disjoint {B | B ⊆ A ∧ B.ncard ≤ d} {B | B ⊆ A ∧ B.ncard = d + 1}

Used by

ncard_setOf_ncard_le

Declncard_image_inter_le_ncard_setOf_shattersDeclaration kindtheorem
The ncard transfer of encard_image_inter_le_encard_shatters, for A finite. Internal: the general statement is the encard one, which needs no hypothesis.
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α},
  A.Finite → ((fun x => A ∩ x) '' 𝒜).ncard ≤ {B | B ⊆ A ∧ Shatters 𝒜 B}.ncard
```
Shatters
Uses
- encard_image_inter_le_encard_shatters
- finite_setOf_subset_and
Used by
- HasVCDimLE.ncard_image_inter_le
Declencard_image_inter_le_encard_shattersDeclaration kindtheorem
Pajor's inequality, with no finiteness assumptions: the traces of 𝒜 on A are at most as many as the subsets of A shattered by 𝒜. For a finite trace family this is a descent on the number of traces that never consumes the ground set; an infinite trace family forces infinitely many shattered singletons, and both sides are ⊤.
Dvir, Filmus and Moran, A Sauer-Shelah-Perles Lemma for Lattices, credit the Boolean lattice case to Pajor (Sous-espaces ℓ₁ⁿ des espaces de Banach, Travaux en Cours 16, Hermann, Paris, 1985) and to Aharoni and Holzman, unpublished. Their Theorem 1.2 is the lattice form, for finite lattices with nonvanishing Möbius function: a family shatters at least as many elements as it has members. Reading that for a family of traces on a ground set is the standard translation into the language of set families, and the statement here carries no finiteness hypothesis, which theirs does.
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α}, ((fun x => A ∩ x) '' 𝒜).encard ≤ {B | B ⊆ A ∧ Shatters 𝒜 B}.encard
```
Shatters
Uses
- infinite_setOf_shatters
- pajor_encard_aux
Used by
- ncard_image_inter_le_ncard_setOf_shatters
Declpajor_encard_auxDeclaration kindtheorem
```
∀ {α : Type u_1} {A : Set α} (N : ℕ) (𝒜 : Set (Set α)),
  ((fun x => A ∩ x) '' 𝒜).Finite →
    ((fun x => A ∩ x) '' 𝒜).ncard ≤ N → ((fun x => A ∩ x) '' 𝒜).encard ≤ {B | B ⊆ A ∧ Shatters 𝒜 B}.encard
```
Shatters Shatters.mono shatters_bot
Uses
Used by
- encard_image_inter_le_encard_shatters

Decltrace_sep_unionDeclaration kindtheorem

∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α} {x : α},
  (fun x => A ∩ x) '' {C | C ∈ 𝒜 ∧ x ∉ C} ∪ (fun x => A ∩ x) '' {C | C ∈ 𝒜 ∧ x ∈ C} = (fun x => A ∩ x) '' 𝒜

Used by

pajor_encard_aux

Decltrace_sep_disjointDeclaration kindtheorem

∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α} {x : α},
  x ∈ A → Disjoint ((fun x => A ∩ x) '' {C | C ∈ 𝒜 ∧ x ∉ C}) ((fun x => A ∩ x) '' {C | C ∈ 𝒜 ∧ x ∈ C})

Used by

pajor_encard_aux

DeclnotMem_of_shatters_sep_rightDeclaration kindtheorem
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {B : Set α} {x : α}, Shatters {C | C ∈ 𝒜 ∧ x ∈ C} B → x ∉ B
```
Shatters Shatters.preimage_compl
Uses
- notMem_of_forall_notMem
Used by
- pajor_encard_aux

DeclnotMem_of_shatters_sep_leftDeclaration kindtheorem

∀ {α : Type u_1} {𝒜 : Set (Set α)} {B : Set α} {x : α}, Shatters {C | C ∈ 𝒜 ∧ x ∉ C} B → x ∉ B

Shatters

Uses

notMem_of_forall_notMem

Used by

pajor_encard_aux

DeclnotMem_of_forall_notMemDeclaration kindtheorem
A family whose members all avoid x shatters only sets avoiding x.
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {B : Set α} {x : α}, (∀ C ∈ 𝒜, x ∉ C) → Shatters 𝒜 B → x ∉ B
```
Shatters Shatters.exists_ge
Used by
- notMem_of_shatters_sep_left
- notMem_of_shatters_sep_right
Declinsert_injOn_notMemDeclaration kindtheorem
Inserting a fixed element is injective on the sets avoiding it: the element can be removed again, recovering the argument.
```
∀ {α : Type u_1} (x : α), Set.InjOn (insert x) {B | x ∉ B}
```
Used by
- pajor_encard_aux

Declexists_splitterDeclaration kindtheorem

∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α},
  ((fun x => A ∩ x) '' 𝒜).Nontrivial → ∃ x ∈ A, (∃ C ∈ 𝒜, x ∈ C) ∧ ∃ C ∈ 𝒜, x ∉ C

Uses

exists_splitter_of_not_subset

Used by

pajor_encard_aux

Declexists_splitter_of_not_subsetDeclaration kindtheorem

A point of A witnessing that one trace fails to contain another is a point at which 𝒜 splits.

∀ {α : Type u_1} {𝒜 : Set (Set α)} {A C C' : Set α},
  C ∈ 𝒜 → C' ∈ 𝒜 → ¬A ∩ C ⊆ A ∩ C' → ∃ x ∈ A, (∃ D ∈ 𝒜, x ∈ D) ∧ ∃ D ∈ 𝒜, x ∉ D

Used by

exists_splitter

Decldisjoint_image_insertDeclaration kindtheorem
A family whose members all avoid x is disjoint from any family of sets containing x.
```
∀ {α : Type u_1} {x : α} {𝒮 𝒯 : Set (Set α)}, (∀ B ∈ 𝒮, x ∉ B) → Disjoint 𝒮 (insert x '' 𝒯)
```
Used by
- pajor_encard_aux
DeclShatters.insertDeclaration kindtheorem
If B is shattered both by the members of 𝒜 avoiding x and by the members of 𝒜 containing x, then 𝒜 shatters insert x B. This is the exchange step in the proof of Pajor's inequality.
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {B : Set α} {x : α},
  Shatters {C | C ∈ 𝒜 ∧ x ∉ C} B → Shatters {C | C ∈ 𝒜 ∧ x ∈ C} B → Shatters 𝒜 (insert x B)
```
Shatters
Uses
- Shatters.exists_inter_eq
- Shatters.of_forall_subset
Used by
- pajor_encard_aux
Declinfinite_setOf_shattersDeclaration kindtheorem
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α}, ((fun x => A ∩ x) '' 𝒜).Infinite → {B | B ⊆ A ∧ Shatters 𝒜 B}.Infinite
```
Shatters splitPoints
Uses
- finite_image_inter_of_finite_splitPoints
- singleton_image_splitPoints_subset
Used by
- encard_image_inter_le_encard_shatters
Declsingleton_image_splitPoints_subsetDeclaration kindtheorem
The singleton of a point at which 𝒜 splits is shattered by 𝒜.
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α}, (fun x => {x}) '' splitPoints✝ 𝒜 A ⊆ {B | B ⊆ A ∧ Shatters 𝒜 B}
```
Shatters splitPoints
Uses
- shatters_singleton
Used by
- infinite_setOf_shatters
Declshatters_singletonDeclaration kindtheorem
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {x : α}, Shatters 𝒜 {x} ↔ (∃ C ∈ 𝒜, x ∈ C) ∧ ∃ C ∈ 𝒜, x ∉ C
```
Shatters
Uses
- Shatters.exists_inter_eq
- Shatters.of_forall_subset
Used by
- singleton_image_splitPoints_subset
DeclShatters.of_forall_subsetDeclaration kindtheorem
Shatters read at Set α, as an introduction rule; the ∩-shaped companion of Shatters.of_forall_le.
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α}, (∀ ⦃B : Set α⦄, B ⊆ A → ∃ C ∈ 𝒜, A ∩ C = B) → Shatters 𝒜 A
```
Shatters
Used by
- Shatters.insert
- shatters_singleton
DeclShatters.exists_inter_eqDeclaration kindtheorem
Shatters read at Set α, where ⊓ is ∩ and ≤ is ⊆: every subset of A is the intersection of A with a member of 𝒜. Definitionally the same statement, stated in the shape every use site wants, so that consumers obtain an ∩-typed equation directly.
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {A B : Set α}, Shatters 𝒜 A → B ⊆ A → ∃ C ∈ 𝒜, A ∩ C = B
```
Shatters
Used by
- Shatters.insert
- shatters_singleton
Declfinite_image_inter_of_finite_splitPointsDeclaration kindtheorem
A family splitting A at finitely many elements has finitely many traces on A.
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α}, (splitPoints✝ 𝒜 A).Finite → ((fun x => A ∩ x) '' 𝒜).Finite
```
splitPoints
Uses
- injOn_inter_splitPoints
Used by
- infinite_setOf_shatters
DeclinjOn_inter_splitPointsDeclaration kindtheorem
A trace of 𝒜 on A is determined by its restriction to the elements at which 𝒜 splits: elsewhere, membership in the trace is decided by A alone.
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α}, Set.InjOn (fun x => x ∩ splitPoints✝ 𝒜 A) ((fun x => A ∩ x) '' 𝒜)
```
splitPoints
Used by
- finite_image_inter_of_finite_splitPoints
Declfinite_setOf_subset_andDeclaration kindtheorem
Any collection of subsets of a finite set is finite.
```
∀ {α : Type u_1} {A : Set α}, A.Finite → ∀ (p : Set α → Prop), {B | B ⊆ A ∧ p B}.Finite
```
Used by
DeclHasVCDimLE.ncard_le_of_shattersDeclaration kindtheorem
A family of VC dimension at most d shatters only sets of size at most d.
```
∀ {α : Type u_1} {d : ℕ} {𝒜 : Set (Set α)} {B : Set α}, HasVCDimLE d 𝒜 → Shatters 𝒜 B → B.ncard ≤ d
```
HasVCDimLE Shatters
Uses
- HasVCDimLE.finite_of_shatters
Used by
- HasVCDimLE.ncard_image_inter_le
DeclHasVCDimLE.finite_of_shattersDeclaration kindtheorem
A family of VC dimension at most d shatters only finite sets.
```
∀ {α : Type u_1} {d : ℕ} {𝒜 : Set (Set α)} {B : Set α}, HasVCDimLE d 𝒜 → Shatters 𝒜 B → B.Finite
```
HasVCDimLE Shatters Shatters.subset
Used by
- HasVCDimLE.ncard_le_of_shatters
Hypothesish𝒜
```
HasVCDimLE d 𝒜
```
Hypothesishdn
```
d ≤ n
```
DefinitionHasVCDimLEdefYaël Dillies
A set family 𝒜 has VC dimension at most d if all the sets it shatters have size at most d.
```
{α : Type u_1} → ℕ → Set (Set α) → Prop
```
DefinitionShattersdefYaël Dillies
A set family 𝒜 shatters a set A if all subsets of A can be obtained as the intersection of A with some element of the set family. We also say that A is traced by 𝒜.
```
{α : Type u_1} → [SemilatticeInf α] → Set α → α → Prop
```

Cited resultShatters.exists_getheoremYaël Dillies

∀ {α : Type u_1} [inst : SemilatticeInf α] {𝒜 : Set α} {A : α}, Shatters 𝒜 A → ∃ B ∈ 𝒜, A ≤ B

Cited resultShatters.monotheoremYaël Dillies

∀ {α : Type u_1} [inst : SemilatticeInf α] {𝒜 ℬ : Set α} {A : α}, 𝒜 ⊆ ℬ → Shatters 𝒜 A → Shatters ℬ A

Cited resultShatters.preimage_compltheoremYaël Dillies

∀ {α : Type u_1} [inst : BooleanAlgebra α] {𝒜 : Set α} {A : α}, Shatters 𝒜 A → Shatters ((fun x => xᶜ) ⁻¹' 𝒜) A

Cited resultShatters.subsettheoremYaël Dillies

∀ {α : Type u_1} {𝒜 : Set (Set α)} {A B : Set α}, A ⊆ B → Shatters 𝒜 B → Shatters 𝒜 A

Cited resultshatters_bottheoremYaël Dillies

∀ {α : Type u_1} [inst : SemilatticeInf α] {𝒜 : Set α} [inst_1 : OrderBot α], Shatters 𝒜 ⊥ ↔ 𝒜.Nonempty

DefinitionsplitPointsdef
The elements of A at which 𝒜 splits: some member of 𝒜 contains them and some does not. These are exactly the elements whose singleton 𝒜 shatters.
```
{α : Type u_1} → Set (Set α) → Set α → Set α
```
DefinitionvcGrowthdefYaël Dillies
The growth of a set family is the maximum number of sets it cuts out from any set of size at most n.
```
{α : Type u_1} → ℕ → Set (Set α) → ℕ
```

Cited resultvcGrowth_le_ifftheoremYaël Dillies

∀ {α : Type u_1} {n : ℕ} {𝒜 : Set (Set α)} {d : ℕ},
  vcGrowth n 𝒜 ≤ d ↔ ∀ ⦃A : Set α⦄, A.Finite → A.ncard ≤ n → ((fun x => A ∩ x) '' 𝒜).ncard ≤ d

DOIMTH.R-2026-6002

Cite

Verification

Replay: accepted
Axioms: Classical.choiceQuot.soundpropext
Statement identity: not-applicable
Substrate: Lean 4 kernel v4.31.0
Dictionary pin: design-lab@5802df4 · initial
Frozen export: 600ed63e389a
Verified: 2026-09-24T00:00:00Z