Mathesis

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

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.

Declencard_image_inter_le_encard_shatters

∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α}, ((fun x => A ∩ x) '' 𝒜).encard ≤ {B | B ⊆ A ∧ Shatters 𝒜 B}.encard

TopicTraces and shattering

Relations

Generalised byMTH.C-2026-6005
At Y = Bool this specialises to Pajor's inequality.
Asserted by Dhruv Gupta

ThesisStepDefinitionCited result

Declencard_image_inter_le_encard_shattersDeclaration kindtheorem

∀ {α : 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

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
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_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 α
```

DOIMTH.R-2026-6001

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: 5a0bbcf25324
Verified: 2026-09-24T00:00:00Z