Catalog/Sparsity/NowhereDense/Full.lean
| 1 | import Catalog.Sparsity.ShallowMinor.Full |
| 2 | import Catalog.Sparsity.Preliminaries.Full |
| 3 | |
| 4 | open Catalog.Sparsity.ShallowMinor |
| 5 | open Catalog.Sparsity.Preliminaries |
| 6 | |
| 7 | namespace Catalog.Sparsity.NowhereDense |
| 8 | |
| 9 | /-- A uniform excluded-clique bound on depth-`d` minors of graphs in `C`. |
| 10 | The parameter `t` is the allowed clique size, so the excluded graph is |
| 11 | `K_{t+1}`. -/ |
| 12 | def HasShallowCliqueBound (C : GraphClass) (d t : ℕ) : Prop := |
| 13 | ∀ {V : Type} [DecidableEq V] [Fintype V] (G : SimpleGraph V), |
| 14 | C G → ¬IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) G d |
| 15 | |
| 16 | /-- A class `C` of graphs is nowhere dense if for every depth `d` there is a |
| 17 | bound `t` such that no graph in `C` contains `K_{t+1}` as a depth-`d` |
| 18 | minor. (Def 2.6) -/ |
| 19 | def IsNowhereDense (C : GraphClass) : Prop := |
| 20 | ∀ d : ℕ, ∃ t : ℕ, HasShallowCliqueBound C d t |
| 21 | |
| 22 | end Catalog.Sparsity.NowhereDense |
| 23 |