Mathesis

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

Assouad's dual VC bound. If VCDim X C ≤ d, then VCDim(dualClass C) ≤ 2^(d+1) − 1.

DeclvcDim_dualClass_le

∀ {X : Type u} {C : ConceptClass X Bool} {d : ℕ}, VCDim X C ≤ ↑d → VCDim (↑C) (dualClass C) ≤ ↑(2 ^ (d + 1) - 1)

TopicVC dimension

ThesisStepHypothesisDefinition

DeclvcDim_dualClass_leDeclaration kindtheorem

∀ {X : Type u} {C : ConceptClass X Bool} {d : ℕ}, VCDim X C ≤ ↑d → VCDim (↑C) (dualClass C) ≤ ↑(2 ^ (d + 1) - 1)

ConceptClass FLT.Concept Shatters VCDim dualClass

Uses

dualClass_shatters_imp_shatters

DecldualClass_shatters_imp_shattersDeclaration kindtheorem
Assouad's coding lemma. If the dual class shatters a set S of concepts with 2^(d+1) ≤ S.card, then C shatters some set of d + 1 points.
Index 2^(d+1) of the shattered concepts by bitstrings; for each coordinate k, dual shattering realizes the labelling "is this codeword in the k-th bit slice", which supplies a point x k reading off exactly that bit. These d + 1 points are then shattered by C.
```
∀ {X : Type u} {C : ConceptClass X Bool} {d : ℕ} (S : Finset ↑C),
  Shatters (↑C) (dualClass C) S → 2 ^ (d + 1) ≤ S.card → ∃ T, T.card = d + 1 ∧ Shatters X C T
```
ConceptClass FLT.Concept Shatters cubeBitSlice cubeEmbedding dualClass
Uses
- mem_cubeBitSlice_iff
Used by
- vcDim_dualClass_le

Declmem_cubeBitSlice_iffDeclaration kindtheorem

Codeword (cube b).val is in cubeBitSlice cube k iff b k = true.

∀ {X : Type u} {C : ConceptClass X Bool} {n : ℕ} {S : Finset ↑C} (cube : (Fin n → Bool) ↪ ↥S) (b : Fin n → Bool)
  (k : Fin n), ↑(cube b) ∈ cubeBitSlice✝ cube k ↔ b k = true

ConceptClass FLT.Concept cubeBitSlice

Used by

dualClass_shatters_imp_shatters

Hypothesishd
```
VCDim X C ≤ ↑d
```
DefinitionConceptClassdef
A concept class is a set of concepts. Used by every paradigm, complexity measure, and criterion.
Primary definition: Set of functions. Used for PAC/agnostic PAC where concept classes are sets over which VC dimension, Rademacher complexity, covering numbers, etc. are measured. Alternative definitions below for contexts requiring decidability, enumerability, or measurability.
```
Type u → Type v → Type (max v u)
```
DefinitionFLT.Conceptdef
A concept is a function from domain to label. This is the atomic unit that concept classes collect and learners try to approximate.
```
Type u → Type v → Type (max u v)
```
DefinitionShattersdefYaël Dillies
A set S ⊆ X is shattered by concept class C if every labeling of S is realized by some concept in C.
```
(X : Type u) → ConceptClass X Bool → Finset X → Prop
```
DefinitionVCDimdef
VC dimension of a concept class: the size of the largest shattered set. Returns ℕ∞ = WithTop ℕ.
```
(X : Type u) → ConceptClass X Bool → WithTop ℕ
```

DefinitioncubeBitSlicedef

The image of {b : Fin n → Bool | b k = true} under a cube embedding: the codewords whose k-th bit is set.

{X : Type u} → {C : ConceptClass X Bool} → {n : ℕ} → {S : Finset ↑C} → ((Fin n → Bool) ↪ ↥S) → Fin n → Finset ↑C

DefinitioncubeEmbeddingdef
Embedding (Fin n → Bool) ↪ ↥S when 2 ^ n ≤ S.card, via (Fin n → Bool) ≃ Fin (2 ^ n) ↪ Fin S.card ≃ ↥S.
```
{X : Type u} → {C : ConceptClass X Bool} → {n : ℕ} → (S : Finset ↑C) → 2 ^ n ≤ S.card → (Fin n → Bool) ↪ ↥S
```
DefinitiondualClassdef
The dual concept class: each point x : X gives the evaluation concept c ↦ c x on the new domain ↥C. The dual class collects these over all points.
```
{X : Type u} → (C : ConceptClass X Bool) → ConceptClass (↑C) Bool
```

DOIMTH.R-2026-6031

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