Lax Lean Archive

Nowhere dense classes have subpolynomial weak coloring numbers

Lax199508.NowhereDenseWcol · concepts/Lax199508/NowhereDenseWcol.lean · lax-199508

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    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^ε.

    This is Theorem 3.4 of Chapter 2 of the source lecture notes (2019/20 edition).

    Concept map
    4 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax199508.NowhereDenseClasses
    2import Lax199508.ColoringNumbers
    3
    4/-!
    5---
    6title: Nowhere dense classes have subpolynomial weak coloring numbers
    7type: theorem
    8---
    9Every nowhere dense graph class has subpolynomial weak coloring
    10numbers: for every radius *r* and every ε > 0 there is a constant *c*
    11such that every subgraph *H* of a member, on *m* vertices, satisfies
    12wcol_r(*H*) ≤ *c* · *m*^ε.
    13
    14This is Theorem 3.4 of Chapter 2 of the source lecture notes (2019/20
    15edition).
    16
    17# Formalization notes
    18
    19The hypothesis is the shallow-minor definition of the nowhere dense
    20concept; the conclusion is the shared predicate `HasSubpolynomialWcol`
    21of the coloring-number concept. The notes state the bound for the
    22members of the class only, whereas the predicate used here demands it
    23uniformly for all subgraphs of members; the two are equivalent, because
    24the subgraphs of the members of a nowhere dense class again form a
    25nowhere dense class, and the subgraph-uniform form is what downstream
    26localization arguments consume. This is the headline of the submission
    27and is the composition of the four preceding theorem concepts:
    28subpolynomial shallow-minor density, the admissibility bound, and the
    29two links of the coloring-number chain.
    30-/
    31
    32namespace Lax199508.NowhereDenseWcol
    33
    34open Lax199508.GraphClasses Lax199508.NowhereDenseClasses Lax199508.ColoringNumbers
    35
    36/-- Nowhere dense graph classes have subpolynomial weak coloring
    37numbers. -/
    38axiom hasSubpolynomialWcol_of_nowhereDense
    39 (C : GraphClass) (h : NowhereDense C) :
    40 HasSubpolynomialWcol C
    41
    42end Lax199508.NowhereDenseWcol
    43
    Show Proof
    Formalization notes

    The hypothesis is the shallow-minor definition of the nowhere dense concept; the conclusion is the shared predicate HasSubpolynomialWcolHasSubpolynomialWcol of the coloring-number concept. The notes state the bound for the members of the class only, whereas the predicate used here demands it uniformly for all subgraphs of members; the two are equivalent, because the subgraphs of the members of a nowhere dense class again form a nowhere dense class, and the subgraph-uniform form is what downstream localization arguments consume. This is the headline of the submission and is the composition of the four preceding theorem concepts: subpolynomial shallow-minor density, the admissibility bound, and the two links of the coloring-number chain.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…