Bounded-VC duality
Lax185574.VCDuality · concepts/Lax185574/VCDuality.lean · lax-185574
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Lemma
For a graph G and sets S, X ⊆ V(G), the set S dominates X if every vertex of X ∖ S has a neighbor in S, and S antidominates X if every vertex of X ∖ S has a nonneighbor in S.
For every d ∈ ℕ there is some k ∈ ℕ with the following property. Let G be a graph of VC-dimension at most d, and let X, Y ⊆ V(G) be two (possibly overlapping) sets with at least one of X, Y finite. Then there exists a set sample(X, Y) of size at most k such that at least one of the following holds:
- sample(X, Y) is contained in Y and dominates X,
- sample(X, Y) is contained in X and antidominates Y.
This is a corollary of the (p, q)-theorem for bounded VC-dimension.
Concept map
In the paper
- page 24 of this submission's paper
Lean source view on GitHub
| 1 | import Lax185574.VCDimension |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Bounded-VC duality |
| 6 | type: lemma |
| 7 | --- |
| 8 | For a graph G and sets S, X ⊆ V(G), the set S *dominates* X if every |
| 9 | vertex of X ∖ S has a neighbor in S, and S *antidominates* X if every |
| 10 | vertex of X ∖ S has a nonneighbor in S. |
| 11 | |
| 12 | For every d ∈ ℕ there is some k ∈ ℕ with the following property. Let G |
| 13 | be a graph of VC-dimension at most d, and let X, Y ⊆ V(G) be two |
| 14 | (possibly overlapping) sets with at least one of X, Y finite. Then there |
| 15 | exists a set sample(X, Y) of size at most k such that at least one of |
| 16 | the following holds: |
| 17 | |
| 18 | 1. sample(X, Y) is contained in Y and dominates X, |
| 19 | 2. sample(X, Y) is contained in X and antidominates Y. |
| 20 | |
| 21 | This is a corollary of the (p, q)-theorem for bounded VC-dimension. |
| 22 | |
| 23 | # Formalization notes |
| 24 | |
| 25 | The graph is finite, so the hypothesis that X or Y is finite always |
| 26 | holds and is omitted. The paper also allows infinite graphs. Every |
| 27 | application in the paper, through the ball-flip lemma inside the proof |
| 28 | of the closure theorem, is to a finite graph. The bound k is chosen |
| 29 | before the graph. VC-dimension is `VCDimension.vcDim`. |
| 30 | -/ |
| 31 | |
| 32 | namespace Lax185574.VCDuality |
| 33 | |
| 34 | open Lax185574.VCDimension |
| 35 | |
| 36 | universe u |
| 37 | |
| 38 | variable {V : Type u} |
| 39 | |
| 40 | /-- `S` dominates `X` in `G`: every vertex of `X ∖ S` has a neighbor in |
| 41 | `S`. -/ |
| 42 | def Dominates (G : SimpleGraph V) (S X : Set V) : Prop := |
| 43 | ∀ x ∈ X \ S, ∃ y ∈ S, G.Adj x y |
| 44 | |
| 45 | /-- `S` antidominates `X` in `G`: every vertex of `X ∖ S` has a |
| 46 | nonneighbor in `S`. -/ |
| 47 | def Antidominates (G : SimpleGraph V) (S X : Set V) : Prop := |
| 48 | ∀ x ∈ X \ S, ∃ y ∈ S, ¬ G.Adj x y |
| 49 | |
| 50 | /-- **Bounded-VC duality.** In a finite graph of VC-dimension at most |
| 51 | `d`, for any two vertex sets `X` and `Y`, some set of at most `k(d)` |
| 52 | vertices of `Y` dominates `X`, or some set of at most `k(d)` vertices of |
| 53 | `X` antidominates `Y`. -/ |
| 54 | axiom vc_duality (d : ℕ) : |
| 55 | ∃ k : ℕ, ∀ (V : Type u) [Finite V] (G : SimpleGraph V), vcDim G ≤ d → |
| 56 | ∀ X Y : Set V, ∃ S : Finset V, S.card ≤ k ∧ |
| 57 | (((S : Set V) ⊆ Y ∧ Dominates G S X) ∨ |
| 58 | ((S : Set V) ⊆ X ∧ Antidominates G S Y)) |
| 59 | |
| 60 | end Lax185574.VCDuality |
| 61 |
Formalization notes
The graph is finite, so the hypothesis that X or Y is finite always holds and is omitted. The paper also allows infinite graphs. Every application in the paper, through the ball-flip lemma inside the proof of the closure theorem, is to a finite graph. The bound k is chosen before the graph. VC-dimension is .
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments