Catalog.Sparsity.NDSubpolynomialWcol

Theorem

Let \(\operatorname{wcol}_r\) be as in Definition ColoringNumbers and nowhere dense as in Definition NowhereDense.

Let \(\mathcal{C}\) be a nowhere dense class of graphs. Then there is a function \(f \colon \mathbb{N} \times \mathbb{R}_{>0} \to \mathbb{N}\) such that \[\operatorname{wcol}_r(G) \leq f(r, \varepsilon) \cdot |V(G)|^\varepsilon\] for all \(r \in \mathbb{N}\), \(\varepsilon > 0\), and \(G \in \mathcal{C}\).

Review notes

The source text presents Theorem 3.4 without an explicit proof block; it follows from the preceding discussion. The proof given in proof.tex makes the argument explicit: it chains the subpolynomial \(\nabla\) bound (Theorem NDSubpolynomialDensity), the admissibility–topological-grad bridge (Lemma AdmBoundByTopGrad), and the polynomial equivalence of coloring numbers (Lemma ColoringNumberEquivalence). Each step is a polynomial transformation, so subpolynomial inputs yield subpolynomial outputs.

The key subtlety is that \(\widetilde{\nabla}_d(G) \leq \nabla_d(G)\) (every topological minor is a minor), which bridges the \(\nabla\)-based bound from Theorem NDSubpolynomialDensity to the \(\widetilde{\nabla}\)-based input of Lemma AdmBoundByTopGrad.

Lean encoding.

The constant \(f\) is existentially quantified as a positive real. The graph-level \(\operatorname{wcol}_r(G)\) is encoded as an existential over orderings: \(\exists\;\sigma,\; \operatorname{wcol}_r(G,\sigma) \leq f \cdot n^\varepsilon\). The ordering is introduced via letI := ord to provide a local LinearOrder V instance for the wcol definition.

Catalog/Sparsity/NDSubpolynomialWcol/Contract.lean (full)

1	import Catalog.Sparsity.Preliminaries.Contract
2	import Catalog.Sparsity.ColoringNumbers.Contract
3	import Catalog.Sparsity.NowhereDense.Contract
4	import Mathlib.Analysis.SpecialFunctions.Pow.Real
5
6	open Catalog.Sparsity.ColoringNumbers
7	open Catalog.Sparsity.NowhereDense
8	open Catalog.Sparsity.Preliminaries
9
10	namespace Catalog.Sparsity.NDSubpolynomialWcol
11
12	/-- Theorem 3.4/ch2: Nowhere dense classes have subpolynomial weak coloring
13	number.
14
15	For any ND class C, r ∈ ℕ, ε > 0, there exists a constant f such that
16	every G ∈ C admits an ordering with wcol_r(G,σ) ≤ f · \|V(G)\|^ε. -/
17	axiom nd_subpolynomial_wcol (C : GraphClass) (hC : IsNowhereDense C)
18	(r : ℕ) (ε : ℝ) (hε : 0 < ε) :
19	∃ f : ℝ, 0 < f ∧ ∀ {V : Type} [DecidableEq V] [Fintype V]
20	(G : SimpleGraph V),
21	C G → ∃ (ord : LinearOrder V),
22	letI := ord; (↑(wcol G r) : ℝ) ≤ f * (Fintype.card V : ℝ) ^ ε
23
24	end Catalog.Sparsity.NDSubpolynomialWcol
25

Dependencies

Statement

Proof