Assouad's dual VC bound

Given a family of sets 𝒜 : Finset (Finset α) and a ground set X : Finset α, the dual family of 𝒜 relative to X assigns to each x ∈ X the subfamily {A ∈ 𝒜 | x ∈ A} of elements of 𝒜 containing x. This file establishes Assouad's 1983 dual VC bound: if 𝒜.vcDim ≤ d, then (𝒜.dualFamily X).vcDim ≤ 2 ^ (d + 1) - 1.

The proof is Assouad's original bitstring-coding argument. This bound works well for small d.

Main definitions

• Finset.dualFamily: the dual family of a set family relative to a ground set.
• Finset.mem_dualFamily: membership characterisation.
• Finset.exists_shatters_of_dualFamily_shatters: the bitstring-coding lemma. A subfamily of size 2 ^ n shattered by the dual family yields an n-element subset of the ground set shattered by the original family.
• Finset.vcDim_dualFamily_le: Assouad's VC bound for the dual family.

References

• P. Assouad, Densité et dimension, Ann. Inst. Fourier 33 (3) (1983), Theorem 2.13
• J. Matoušek, Lectures on Discrete Geometry, Graduate Texts in Mathematics 212, Springer, 2002, §10.3 Lemma 10.3.3

Tags

VC dimension, dual VC dimension, shattering, Assouad

def Finset.dualFamily {α : Type u_1} [DecidableEq α] (𝒜 : Finset (Finset α)) (X : Finset α) : Finset (Finset (Finset α))

The dual family of 𝒜 : Finset (Finset α) relative to a ground set X : Finset α: for each x ∈ X, the subfamily {A ∈ 𝒜 | x ∈ A}.

Viewing 𝒜 as rows of a binary incidence matrix indexed by X × 𝒜, the dual family is the collection of its columns.

Equations

• 𝒜.dualFamily X = Finset.image (fun (x : α) => {A ∈ 𝒜 | x ∈ A}) X

@[simp]

theorem Finset.mem_dualFamily {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {X : Finset α} {𝒞 : Finset (Finset α)} : 𝒞 ∈ 𝒜.dualFamily X ↔ ∃ x ∈ X, {A ∈ 𝒜 | x ∈ A} = 𝒞

theorem Finset.exists_shatters_of_dualFamily_shatters {α : Type u_1} [DecidableEq α] (𝒜 : Finset (Finset α)) (X : Finset α) {S : Finset (Finset α)} (hS : (𝒜.dualFamily X).Shatters S) {n : ℕ} (hcard : 2 ^ n ≤ S.card) : ∃ T ⊆ X, T.card = n ∧ 𝒜.Shatters T

Bitstring coding (Assouad 1983, Theorem 2.13). If 𝒜.dualFamily X shatters a subfamily S of size at least 2 ^ n, then 𝒜 shatters some n-element subset of X.

This is the combinatorial side of the dual VC bound: embed the 2 ^ n bit-patterns of length n into S; for each coordinate, shattering provides a ground-set element distinguishing the patterns with that bit set; these n elements are then shattered by 𝒜.

theorem Finset.vcDim_dualFamily_le {α : Type u_1} [DecidableEq α] (𝒜 : Finset (Finset α)) (X : Finset α) {d : ℕ} (hvc : 𝒜.vcDim ≤ d) : (𝒜.dualFamily X).vcDim ≤ 2 ^ (d + 1) - 1

Assouad's dual VC bound. If 𝒜 : Finset (Finset α) has VC dimension at most d, then for any ground set X : Finset α the dual family has VC dimension at most 2 ^ (d + 1) - 1.

This is the Finset-level form of the standard statement vcDim(𝒞*) ≤ 2 ^ (vcDim(𝒞) + 1) - 1 (Assouad 1983, Theorem 2.13; Matoušek, Lectures on Discrete Geometry, §10.3 Lemma 10.3.3).