Mathesis

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

The cardinal Pajor inequality for determined traces: the traces of 𝒜 on A that are determined by finitely many points inject into the shattered subsets, with no hypotheses. Unlike the ℕ∞-valued encard_determined_le_encard_shatters, this bounds genuine cardinalities; the full trace family cannot replace the determined traces (not_mk_image_inter_le_mk_shatters).

Declmk_determined_le_mk_shatters

∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α},
  Cardinal.mk ↑{t | t ∈ (fun x => A ∩ x) '' 𝒜 ∧ ∃ F, F.Finite ∧ ∀ t' ∈ (fun x => A ∩ x) '' 𝒜, t' ∩ F = t ∩ F → t' = t} ≤
    Cardinal.mk ↑{B | B ⊆ A ∧ Shatters 𝒜 B}

TopicTraces and shattering

Relations

Limited byMTH.C-2026-6004
The full trace family cannot replace the determined traces: the half-line cuts over the rationals trace continuum-many sets while shattering only countably many.
Asserted by Dhruv Gupta

ThesisStepDefinitionCited result

Declmk_determined_le_mk_shattersDeclaration kindtheorem

∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α},
  Cardinal.mk ↑{t | t ∈ (fun x => A ∩ x) '' 𝒜 ∧ ∃ F, F.Finite ∧ ∀ t' ∈ (fun x => A ∩ x) '' 𝒜, t' ∩ F = t ∩ F → t' = t} ≤
    Cardinal.mk ↑{B | B ⊆ A ∧ Shatters 𝒜 B}

Shatters diag

Uses

encard_determined_le_encard_shatters
finite_image_inter_of_finite_diag
mk_determined_le_of_infinite_diag
mk_diag_le_mk_shatters

Declmk_diag_le_mk_shattersDeclaration kindtheorem

∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α}, Cardinal.mk ↑(diag✝ 𝒜 A) ≤ Cardinal.mk ↑{B | B ⊆ A ∧ Shatters 𝒜 B}

Shatters diag

Uses

shatters_singleton

Used by

mk_determined_le_mk_shatters

Declmk_determined_le_of_infinite_diagDeclaration kindtheorem

∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α},
  (diag✝ 𝒜 A).Infinite →
    Cardinal.mk
        ↑{t | t ∈ (fun x => A ∩ x) '' 𝒜 ∧ ∃ F, F.Finite ∧ ∀ t' ∈ (fun x => A ∩ x) '' 𝒜, t' ∩ F = t ∩ F → t' = t} ≤
      Cardinal.mk ↑(diag✝ 𝒜 A)

diag

Uses

witness_diag

Used by

mk_determined_le_mk_shatters

Declwitness_diagDeclaration kindtheorem

∀ {α : Type u_1} {𝒜 : Set (Set α)} {A t F : Set α},
  (∀ t' ∈ (fun x => A ∩ x) '' 𝒜, t' ∩ F = t ∩ F → t' = t) →
    t ∈ (fun x => A ∩ x) '' 𝒜 → ∀ t' ∈ (fun x => A ∩ x) '' 𝒜, t' ∩ (F ∩ diag✝ 𝒜 A) = t ∩ (F ∩ diag✝ 𝒜 A) → t' = t

diag

Uses

mem_iff_mem_of_notMem_diag

Used by

mk_determined_le_of_infinite_diag

Declfinite_image_inter_of_finite_diagDeclaration kindtheorem
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α}, (diag✝ 𝒜 A).Finite → ((fun x => A ∩ x) '' 𝒜).Finite
```
diag
Uses
- mem_iff_mem_of_notMem_diag
Used by
- mk_determined_le_mk_shatters

Declmem_iff_mem_of_notMem_diagDeclaration kindtheorem

∀ {α : Type u_1} {𝒜 : Set (Set α)} {A t t' : Set α},
  t ∈ (fun x => A ∩ x) '' 𝒜 → t' ∈ (fun x => A ∩ x) '' 𝒜 → ∀ {y : α}, y ∉ diag✝ 𝒜 A → (y ∈ t ↔ y ∈ t')

diag

Used by

finite_image_inter_of_finite_diag
witness_diag

Declencard_determined_le_encard_shattersDeclaration kindtheorem
The traces of 𝒜 on A that are determined by finitely many points are at most as many as the shattered subsets: the restriction of encard_image_inter_le_encard_shatters to the determined traces. Its cardinal-valued sharpening, which is genuinely stronger than the ℕ∞ statement, is mk_determined_le_mk_shatters.
```
∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α},
  {t | t ∈ (fun x => A ∩ x) '' 𝒜 ∧ ∃ F, F.Finite ∧ ∀ t' ∈ (fun x => A ∩ x) '' 𝒜, t' ∩ F = t ∩ F → t' = t}.encard ≤
    {B | B ⊆ A ∧ Shatters 𝒜 B}.encard
```
Shatters
Uses
- encard_image_inter_le_encard_shatters
Used by
- mk_determined_le_mk_shatters
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
- encard_determined_le_encard_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
- mk_diag_le_mk_shatters
- 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

Definitiondiagdef
The points of A on which 𝒜 is not constant.
```
{α : Type u_1} → Set (Set α) → Set α → Set α
```

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-6003

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