Catalog/VC/UnitDistanceGraphEdges/Contract.lean
| 1 | import Catalog.VC.VCDimension.Contract |
| 2 | import Mathlib.Order.SymmDiff |
| 3 | |
| 4 | namespace Catalog.VC.UnitDistanceGraphEdges |
| 5 | |
| 6 | /-- The unit distance graph of a set family with VC-dimension `dโ` has at |
| 7 | most `dโ ยท |๐|` edges. Equivalently, the number of ordered pairs |
| 8 | `(S, S')` in `๐` with `|S โณ S'| = 1` is at most `2 ยท dโ ยท |๐|`. |
| 9 | (Lemma 5.15) -/ |
| 10 | axiom unitDistEdgeBound {ฮฑ : Type*} [DecidableEq ฮฑ] [Fintype ฮฑ] |
| 11 | (๐ : Finset (Finset ฮฑ)) : |
| 12 | (๐.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card |
| 13 | โค 2 * ๐.vcDim * ๐.card |
| 14 | |
| 15 | end Catalog.VC.UnitDistanceGraphEdges |
| 16 |