A small VC dimension family has few edges in the L¹ metric

This file proves that set families over a finite type that have small VC dimension have a number of pairs (A, B) with #(A ∆ B) = 1 linear in their size.

References

• Sphere Packing Numbers for Subsets of the Boolean n-Cube with Bounded Vapnik-Chervonenkis Dimension, David Haussler
• Write-up by Thomas Bloom: http://www.thomasbloom.org/notes/vc.html

noncomputable def SetFamily.hypercubeEdgeFinset {α : Type u_1} (𝓕 : Finset (Set α)) : Finset (Set α × Set α)

The edges of the subgraph of the hypercube Set α induced by a finite set of vertices 𝓕 : Finset (Set α).

Equations

• SetFamily.hypercubeEdgeFinset 𝓕 = {AB ∈ 𝓕 ×ˢ 𝓕 | (symmDiff AB.1 AB.2).ncard = 1}

@[simp]

theorem SetFamily.prodMk_mem_hypercubeEdgeFinset {α : Type u_1} {𝓕 : Finset (Set α)} {A B : Set α} : (A, B) ∈ hypercubeEdgeFinset 𝓕 ↔ A ∈ 𝓕 ∧ B ∈ 𝓕 ∧ (symmDiff A B).ncard = 1

noncomputable def SetFamily.finiteSymmDiffFinpartition {α : Type u_1} (𝓕 : Finset (Set α)) : Finpartition 𝓕

Partition a set family into its components of finite symmetric difference.

Equations

• SetFamily.finiteSymmDiffFinpartition 𝓕 = { parts := Finset.image (fun (A : Set α) => {B ∈ 𝓕 | (symmDiff A B).Finite}) 𝓕, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }

theorem SetFamily.finite_symmDiff_of_mem_finiteSymmDiffFinpartition {α : Type u_1} {𝓕 𝓒 : Finset (Set α)} {A B : Set α} (h𝓒 : 𝓒 ∈ (finiteSymmDiffFinpartition 𝓕).parts) (hA : A ∈ 𝓒) (hB : B ∈ 𝓒) : (symmDiff A B).Finite

theorem SetFamily.finite_iUnion_sdiff_iInter_of_mem_finiteSymmDiffFinpartition {α : Type u_1} {𝓕 𝓒 : Finset (Set α)} (h𝓒 : 𝓒 ∈ (finiteSymmDiffFinpartition 𝓕).parts) : ((⋃ A ∈ 𝓒, A) \ ⋂ A ∈ 𝓒, A).Finite

@[simp]

theorem SetFamily.sup_finiteSymmDiffFinpartition_hypercubeEdgeFinset {α : Type u_1} (𝓕 : Finset (Set α)) : (finiteSymmDiffFinpartition 𝓕).parts.sup hypercubeEdgeFinset = hypercubeEdgeFinset 𝓕

noncomputable def SetFamily.restrictFiniteSymmDiffComponent {α : Type u_1} (𝓒 : Finset (Set α)) : Finset (Set ↑((⋃ A ∈ 𝓒, A) \ ⋂ A ∈ 𝓒, A))

Restrict a component of finite symmetric difference to a set family over a finite type.

Equations

• SetFamily.restrictFiniteSymmDiffComponent 𝓒 = Finset.image (fun (A : Set α) => Subtype.val ⁻¹' symmDiff A (⋂ B ∈ 𝓒, B)) 𝓒

@[simp]

theorem SetFamily.card_restrictFiniteSymmDiffComponent {α : Type u_1} (𝓒 : Finset (Set α)) : (restrictFiniteSymmDiffComponent 𝓒).card = 𝓒.card

theorem IsNIPWith.restrictFiniteSymmDiffComponent {α : Type u_1} {𝓒 : Finset (Set α)} {d : ℕ} (h𝓒 : IsNIPWith d ↑𝓒) : IsNIPWith d ↑(SetFamily.restrictFiniteSymmDiffComponent 𝓒)

theorem SetFamily.IsNIPWith.card_hypercubeEdgeFinset_le {α : Type u_1} {𝓕 : Finset (Set α)} {d : ℕ} (h𝓕 : IsNIPWith d ↑𝓕) : (hypercubeEdgeFinset 𝓕).card ≤ d * 𝓕.card