Mathesis

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

Assouad's lower bound. For a finite-VC class, ⌊log₂ VCDim⌋ ≤ VCDim(dualClass): the exponential blow-up under dualization is necessary, not merely permitted. Together with the proven upper bound vcDim_dualClass_le (VCDim(dual) ≤ 2^(VCDim+1) − 1) this sandwiches the dual VC dimension between ⌊log₂ d⌋ and 2^(d+1) − 1.

Stated with d := VCDim C extracted as a natural number (finite by hypothesis). The proof picks a shattered set T with 2^(log₂ d) ≤ |T| (which exists because 2^(log₂ d) ≤ d ≤ |T| for the supremal shattered set) and applies pow_le_vcDim_imp_le_vcDim_dualClass.

Decllog₂_vcDim_le_vcDim_dualClass

∀ {X : Type u} {C : ConceptClass X Bool} {d : ℕ}, VCDim X C = ↑d → 0 < d → ↑(Nat.log 2 d) ≤ VCDim (↑C) (dualClass C)

TopicVC dimension

ThesisStepHypothesisDefinition

Decllog₂_vcDim_le_vcDim_dualClassDeclaration kindtheorem
```
∀ {X : Type u} {C : ConceptClass X Bool} {d : ℕ}, VCDim X C = ↑d → 0 < d → ↑(Nat.log 2 d) ≤ VCDim (↑C) (dualClass C)
```
ConceptClass FLT.Concept Shatters VCDim dualClass
Uses
- pow_le_vcDim_imp_le_vcDim_dualClass
Declpow_le_vcDim_imp_le_vcDim_dualClassDeclaration kindtheorem
Assouad's lower construction. If C shatters a set T of at least 2^k points, then dualClass C shatters a set of k evaluation concepts, so k ≤ VCDim(dualClass C).
Bitstrings index a 2^k-subset of T; coordinate j is realized by a concept c_j ∈ C reading off the j-th bit, and the dual class shatters {c_j} because the evaluation point indexed by a bitstring σ realizes exactly the labelling σ of the c_j.
```
∀ {X : Type u} {C : ConceptClass X Bool} {k : ℕ} (T : Finset X),
  Shatters X C T → 2 ^ k ≤ T.card → ↑k ≤ VCDim (↑C) (dualClass C)
```
ConceptClass FLT.Concept Shatters VCDim dualClass evalConcept
Uses
- evalConcept_mem
Used by
- log₂_vcDim_le_vcDim_dualClass
DeclevalConcept_memDeclaration kindtheorem
Each evaluation concept belongs to the dual class.
```
∀ {X : Type u} (C : ConceptClass X Bool) (x : X), evalConcept C x ∈ dualClass C
```
ConceptClass FLT.Concept dualClass evalConcept
Used by
- pow_le_vcDim_imp_le_vcDim_dualClass
Hypothesishd
```
VCDim X C = ↑d
```
Hypothesishd0
```
0 < 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 ℕ
```
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
```
DefinitionevalConceptdef
The evaluation concept at a point x: the map c ↦ c x on ↥C.
```
{X : Type u} → (C : ConceptClass X Bool) → X → ↑C → Bool
```

DOIMTH.R-2026-6032

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