Lax5.NowhereDenseWcol
Nowhere dense classes have subpolynomial weak coloring numbers
concepts/Lax5/NowhereDenseWcol.lean · Lax5
Theorem
Fix a linear ordering of the vertices of a graph G. A vertex u is weakly r-reachable from v if some path from v to u of length at most r has u as its smallest vertex. The weak r-coloring number wcol_r(G) is the minimum over all orderings of the maximum number of vertices weakly r-reachable from a single vertex. Every nowhere dense graph class has subpolynomial weak coloring numbers: for every radius r and every ε > 0 there is a constant c such that every subgraph H of a member, on m vertices, satisfies wcol_r(H) ≤ c · m^ε.
Lean source view on GitHub
| 1 | import Lax5.NowhereDenseClasses |
| 2 | import Mathlib.Combinatorics.SimpleGraph.Copy |
| 3 | import Mathlib.Data.Set.Card |
| 4 | import Mathlib.Data.Nat.Lattice |
| 5 | import Mathlib.Analysis.SpecialFunctions.Pow.Real |
| 6 | |
| 7 | /-! |
| 8 | --- |
| 9 | title: Nowhere dense classes have subpolynomial weak coloring numbers |
| 10 | type: theorem |
| 11 | --- |
| 12 | Fix a linear ordering of the vertices of a graph *G*. A vertex *u* is |
| 13 | weakly *r*-reachable from *v* if some path from *v* to *u* of length |
| 14 | at most *r* has *u* as its smallest vertex. The weak *r*-coloring |
| 15 | number wcol_r(*G*) is the minimum over all orderings of the maximum |
| 16 | number of vertices weakly *r*-reachable from a single vertex. Every |
| 17 | nowhere dense graph class has subpolynomial weak coloring numbers: for |
| 18 | every radius *r* and every ε > 0 there is a constant *c* such that |
| 19 | every subgraph *H* of a member, on *m* vertices, satisfies |
| 20 | wcol_r(*H*) ≤ *c* · *m*^ε. |
| 21 | |
| 22 | # Formalization notes |
| 23 | |
| 24 | An ordering of the vertices is a permutation `π` of `Fin m` assigning |
| 25 | each vertex its position. Weak reachability is stated with walks, as |
| 26 | in the nowhere dense concept: shortcutting a walk to a path only |
| 27 | shrinks its support, so walks of length at most `r` with `π`-minimal |
| 28 | endpoint reach exactly the vertices that such paths do. `wcol` is the |
| 29 | least achievable bound `k`, a `Nat.sInf` (attained: `k = m` works for |
| 30 | any ordering); the count is `Set.ncard` as in the neighborhood |
| 31 | complexity concept. |
| 32 | |
| 33 | The bound is uniform over subgraph copies (`⊑`, as in the weakly |
| 34 | sparse concept) of members, each measured by its own vertex count `m`. |
| 35 | Since nowhere denseness survives taking subgraphs, this is the |
| 36 | literature statement for subgraph-closed classes, and the uniformity |
| 37 | is what localization arguments downstream consume. At `m = 0` both |
| 38 | sides vanish, so no nonemptiness hypothesis is needed. The theorem |
| 39 | combines Zhu's bounds relating weak coloring numbers to densities of |
| 40 | shallow minors with the subpolynomial density bounds for nowhere dense |
| 41 | classes (Nešetřil, Ossona de Mendez); see chapters 2 and 5 of the |
| 42 | sparsity lecture notes of Pilipczuk, Pilipczuk, Siebertz. |
| 43 | -/ |
| 44 | |
| 45 | namespace Lax5.NowhereDenseWcol |
| 46 | |
| 47 | open scoped SimpleGraph |
| 48 | open Lax5.GraphClasses Lax5.NowhereDenseClasses |
| 49 | |
| 50 | /-- The set of vertices weakly `r`-reachable from `v` in `G` under the |
| 51 | vertex ordering `π` (vertex `u` sits at position `π u`): the endpoints |
| 52 | `u` of walks from `v` of length at most `r` on whose support `u` is |
| 53 | `π`-minimal. Contains `v` itself. -/ |
| 54 | def wreach {n : ℕ} (G : SimpleGraph (Fin n)) (π : Equiv.Perm (Fin n)) |
| 55 | (r : ℕ) (v : Fin n) : Set (Fin n) := |
| 56 | {u | ∃ w : G.Walk v u, w.length ≤ r ∧ ∀ y ∈ w.support, π u ≤ π y} |
| 57 | |
| 58 | /-- The weak `r`-coloring number of `G`: the least `k` such that under |
| 59 | some vertex ordering every vertex weakly `r`-reaches at most `k` |
| 60 | vertices. -/ |
| 61 | noncomputable def wcol {n : ℕ} (G : SimpleGraph (Fin n)) (r : ℕ) : ℕ := |
| 62 | sInf {k | ∃ π : Equiv.Perm (Fin n), ∀ v, (wreach G π r v).ncard ≤ k} |
| 63 | |
| 64 | /-- Every subgraph of every member of the class, on `m` vertices, has |
| 65 | weak `r`-coloring number at most `c · m^ε`, where `c` depends only on |
| 66 | the radius `r` and on `ε > 0`: weak coloring numbers `m^{o(1)}`. -/ |
| 67 | def HasSubpolynomialWcol (C : GraphClass) : Prop := |
| 68 | ∀ (r : ℕ) (ε : ℝ), 0 < ε → ∃ c : ℝ, |
| 69 | ∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G → |
| 70 | ∀ (m : ℕ) (H : SimpleGraph (Fin m)), H ⊑ G → |
| 71 | (wcol H r : ℝ) ≤ c * (m : ℝ) ^ ε |
| 72 | |
| 73 | /-- Nowhere dense graph classes have subpolynomial weak coloring |
| 74 | numbers. -/ |
| 75 | axiom hasSubpolynomialWcol_of_nowhereDense |
| 76 | (C : GraphClass) (h : NowhereDense C) : |
| 77 | HasSubpolynomialWcol C |
| 78 | |
| 79 | end Lax5.NowhereDenseWcol |
| 80 |
Formalization notes
An ordering of the vertices is a permutation π of Fin m assigning
each vertex its position. Weak reachability is stated with walks, as
in the nowhere dense concept: shortcutting a walk to a path only
shrinks its support, so walks of length at most r with π-minimal
endpoint reach exactly the vertices that such paths do. wcol is the
least achievable bound k, a Nat.sInf (attained: k = m works for
any ordering); the count is Set.ncard as in the neighborhood
complexity concept.
The bound is uniform over subgraph copies (⊑, as in the weakly
sparse concept) of members, each measured by its own vertex count m.
Since nowhere denseness survives taking subgraphs, this is the
literature statement for subgraph-closed classes, and the uniformity
is what localization arguments downstream consume. At m = 0 both
sides vanish, so no nonemptiness hypothesis is needed. The theorem
combines Zhu's bounds relating weak coloring numbers to densities of
shallow minors with the subpolynomial density bounds for nowhere dense
classes (Nešetřil, Ossona de Mendez); see chapters 2 and 5 of the
sparsity lecture notes of Pilipczuk, Pilipczuk, Siebertz.
Imported
Imported by
none