Version history

Submission versions

  1. lax-199508current version

    Sparsity Lectures: Nowhere Denseness, Quasi-Wideness, and Generalized Coloring Numbers

  2. lax-12viewing

    Sparsity Lectures: Nowhere Denseness, Quasi-Wideness, and Generalized Coloring Numbers

    GitHub sourceShown on this page

Environment v4.30.0. The archive's epoch is v4.33.0; only submissions in v4.30.0 can cite this work.

Nowhere dense classes have subpolynomial weak coloring numbers

Lax12.NowhereDenseWcol · concepts/Lax12/NowhereDenseWcol.lean · lax-12

proven

Loading review…

Sign in with ORCID

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

    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

    Discussion

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

    Loading discussion…