Catalog.Sparsity.NDSubpolynomialDensity
Theorem
Let \(\nabla_d\) and the depth-\(d\) reduct \(\mathcal{C} \nabla r\) be as in Definition ShallowMinor. Let nowhere dense be as in Definition NowhereDense.
Suppose \(\mathcal{C}\) is a nowhere dense class of graphs. Then for every \(r \in \mathbb{N}\) and every \(\varepsilon > 0\) there exists a constant \(N = N(r, \varepsilon)\) such that for every graph \(G \in \mathcal{C} \nabla r\) with \(n \geq N\) vertices, \(G\) has less than \(n^{1+\varepsilon}\) edges.
Equivalently, there is a function \(f \colon \mathbb{N} \times \mathbb{R}_{>0} \to \mathbb{N}\) such that for all \(r \in \mathbb{N}\), \(\varepsilon > 0\), and \(G \in \mathcal{C}\): \[\nabla_r(G) \leq f(r, \varepsilon) \cdot |V(G)|^{\varepsilon}.\]
Review notes
The “equivalent” restatement in statement.tex using
\(\nabla_r(G) \leq f(r,\varepsilon)|V(G)|^\varepsilon\) follows from the original
formulation: for \(G \in \mathcal{C}\) and any \(H \preccurlyeq_r G\), we have
\(H \in \mathcal{C} \nabla r\) with \(|V(H)| \leq |V(G)|\), so
\(|E(H)|/|V(H)| \leq f(r,\varepsilon)|V(H)|^\varepsilon
\leq f(r,\varepsilon)|V(G)|^\varepsilon\).
Lemma 3.2 of chapter 1 (dense subgraph extraction) is bundled into this entry’s proof rather than given its own catalog entry, as it is a short one-paragraph auxiliary fact used only here.
Lean encoding.
The hypothesis \(H \in \mathcal{C} \nabla r\) uses ShallowReduct from
Lemma ShallowMinorComposition. This required widening the
dependencies: Lemma ShallowMinorComposition was moved from
proof_deps to statement_deps.
The threshold form (\(|E(H)| < n^{1+\varepsilon}\) for \(n \geq N\)) is used
rather than the grad form, avoiding the need to define \(\nabla_r\).
The comparison uses \(\mathbb{R}\)-valued rpow.
Catalog/Sparsity/NDSubpolynomialDensity/Contract.lean (full)
| 1 | import Catalog.Sparsity.Preliminaries.Contract |
| 2 | import Catalog.Sparsity.ShallowMinor.Contract |
| 3 | import Catalog.Sparsity.NowhereDense.Contract |
| 4 | import Mathlib.Combinatorics.SimpleGraph.Finite |
| 5 | import Mathlib.Analysis.SpecialFunctions.Pow.Real |
| 6 | |
| 7 | open Catalog.Sparsity.ShallowMinor |
| 8 | open Catalog.Sparsity.NowhereDense |
| 9 | open Catalog.Sparsity.Preliminaries |
| 10 | |
| 11 | namespace Catalog.Sparsity.NDSubpolynomialDensity |
| 12 | |
| 13 | /-- Theorem 3.1/ch1: Nowhere dense classes have subpolynomial edge density. |
| 14 | |
| 15 | For every ND class C, r ∈ ℕ, ε > 0, every graph H that is a depth-r |
| 16 | shallow minor of some graph in C and has n ≥ N vertices has fewer than |
| 17 | n^{1+ε} edges. -/ |
| 18 | axiom nd_subpolynomial_density (C : GraphClass) (hC : IsNowhereDense C) |
| 19 | (r : ℕ) (ε : ℝ) (hε : 0 < ε) : |
| 20 | ∃ N : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V] |
| 21 | (H : SimpleGraph V) [DecidableRel H.Adj], |
| 22 | (∃ (W : Type) (_ : DecidableEq W) (_ : Fintype W) (G : SimpleGraph W), |
| 23 | C G ∧ IsShallowMinor H G r) → |
| 24 | N ≤ Fintype.card V → |
| 25 | (H.edgeFinset.card : ℝ) < (Fintype.card V : ℝ) ^ (1 + ε) |
| 26 | |
| 27 | end Catalog.Sparsity.NDSubpolynomialDensity |
| 28 |