Lax Lean Archive

Lax12.NowhereDenseWcol

Nowhere dense classes have subpolynomial weak coloring numbers

concepts/Lax12/NowhereDenseWcol.lean · lax-12

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    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).

    Lean source view on GitHub

    1import Lax12.NowhereDenseClasses
    2import Lax12.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 Lax12.NowhereDenseWcol
    33
    34open Lax12.GraphClasses Lax12.NowhereDenseClasses Lax12.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 Lax12.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

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…