Catalog.Sparsity.NowhereDense
Definition
Let \(\nabla_d\) and \(\omega_d\) be as in Definition ShallowMinor.
A class \(\mathcal{C}\) of graphs has bounded expansion if \[\nabla_d(\mathcal{C}) < +\infty \qquad \text{for every } d \in \mathbb{N}.\] Equivalently, there is a function \(f \colon \mathbb{N} \to \mathbb{N}\) such that for all \(d \in \mathbb{N}\) and \(G \in \mathcal{C}\), we have \(\nabla_d(G) \leq f(d)\).
A class \(\mathcal{C}\) of graphs is nowhere dense if \[\omega_d(\mathcal{C}) < +\infty \qquad \text{for every } d \in \mathbb{N}.\] Equivalently, there is a function \(t \colon \mathbb{N} \to \mathbb{N}\) such that for all \(d \in \mathbb{N}\) and \(G \in \mathcal{C}\), we have \(\omega_d(G) \leq t(d)\).
A class that is not nowhere dense is called somewhere dense. Every bounded expansion class is nowhere dense.
Review notes
The source defines nowhere denseness via \(\omega_d(\mathcal{C}) < +\infty\) for all \(d\), where \(\omega_d(G) = \sup\{t : K_t \preccurlyeq_d G\}\). We encode this directly as: for every \(d\) there exists \(t\) such that \(K_{t+1}\) is not a depth-\(d\) minor of any \(G \in \mathcal{C}\).
The shift by \(+1\) (\(K_{t+1}\) rather than \(K_t\)) makes \(t\) the largest clique that can occur, so the bound reads naturally: “cliques up to size \(t\) are allowed.”
Omissions.
The source also defines bounded expansion (Def 2.5) via
\(\nabla_d(\mathcal{C}) < +\infty\). This is not formalized here because no
downstream entry in the densification argument uses it. If it is needed later, it
can be added as a new definition using HasShallowDensityBound (a linear
edge-count bound on depth-\(d\) reducts), following the pattern in the old codebase.
The source also states “every bounded expansion class is nowhere dense” and defines “somewhere dense.” These are omitted for the same reason.
Catalog/Sparsity/NowhereDense/Contract.lean (full)
| 1 | import Catalog.Sparsity.ShallowMinor.Contract |
| 2 | import Catalog.Sparsity.Preliminaries.Contract |
| 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 |