Dual VC Dimension (Assouad's Lemma)

The dual concept class and the bound VCDim*(C) ≤ 2^(d+1) - 1 where d = VCDim(C). This is Assouad's (1983) coding lemma.

The dual class of a concept class C ⊆ (X → Bool) is the concept class on the domain ↥C where each point x : X induces a concept c ↦ c x.

Main results

• DualClass - the dual concept class
• dual_shatters_imp_original_shatters - coding lemma: if the dual shatters 2^(d+1) concepts, then the original class shatters d+1 points
• dual_vcdim_le_pow - Assouad's bound: VCDim*(C) ≤ 2^(VCDim(C)+1) - 1

def DualClass (X : Type u) (C : ConceptClass X Bool) : ConceptClass (↑C) Bool

The dual concept class: for each point x : X, the evaluation map c ↦ c x is a concept on the domain ↥C. The dual class collects all such evaluation concepts.

Equations

• DualClass X C = {f : Concept (↑C) Bool | ∃ (x : X), ∀ (c : ↑C), f c = ↑c x}

def DualVC.evalConcept {X : Type u} {C : ConceptClass X Bool} (x : X) : ↑C → Bool

A dual concept is determined by a point: the evaluation-at-x function.

Equations

• DualVC.evalConcept x c = ↑c x

theorem DualVC.evalConcept_mem_dualClass {X : Type u} {C : ConceptClass X Bool} (x : X) : evalConcept x ∈ DualClass X C

Membership lemma for Assouad's dual VC construction: the evaluation function fun c => c x belongs to the dual class C^T of C. Used in the bitstring coding step of the dual bound vcDim(C^T) ≤ 2^(vcDim(C) + 1) - 1, the standard inequality that lets compression arguments switch between primal and dual without losing dimension control.

theorem DualVC.dual_shatters_imp_original_shatters {X : Type u} {C : ConceptClass X Bool} {d : ℕ} (S : Finset ↑C) (hS : Shatters (↑C) (DualClass X C) S) (hcard : 2 ^ (d + 1) ≤ S.card) : ∃ (T : Finset X), T.card = d + 1 ∧ Shatters X C T

Core coding lemma (Assouad 1983): if the dual class shatters a set S of concepts with |S| ≥ 2^(d+1), then the original class shatters some set of d+1 points.

Proof: index 2^(d+1) concepts by bitstrings b : Fin (d+1) → Bool. For each coordinate j, dual shattering provides a point x_j that "reads off" the j-th bit. Then {x_0, ..., x_d} is shattered by C.

theorem DualVC.dual_vcdim_le_pow {X : Type u} {C : ConceptClass X Bool} {d : ℕ} (hd : VCDim X C ≤ ↑d) : VCDim (↑C) (DualClass X C) ≤ 2 ^ (d + 1) - 1

Assouad's dual VC bound: if VCDim(C) ≤ d, then the VC dimension of the dual class is at most 2^(d+1) - 1.

This is tight: the class of all subsets of {1,...,d} achieves equality.