Lax Lean Archive

Lax12.NowhereDenseNC

Nowhere dense classes have almost linear neighborhood complexity

concepts/Lax12/NowhereDenseNC.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 almost linear neighborhood complexity: for every ε > 0 there is a constant c such that every member G and every nonempty vertex subset A satisfy |{N(v) ∩ A : v ∈ V(G)}| ≤ c · |A|^(1+ε).

    This is the radius-1 case of the theorem of Eickmeyer, Giannopoulou, Kreutzer, Kwon, Pilipczuk, Rabinovich and Siebertz, who prove the corresponding bound for the traces of r-balls for every radius r. The source lecture notes discuss neighborhood complexity but cite the almost-linear bound as a result of the literature rather than proving it; the proof accompanying this submission derives the radius-1 case from the subpolynomial weak-coloring-number theorem stated here.

    Lean source view on GitHub

    1import Lax12.NeighborhoodComplexity
    2import Lax12.NowhereDenseClasses
    3
    4/-!
    5---
    6title: Nowhere dense classes have almost linear neighborhood complexity
    7type: theorem
    8---
    9Every nowhere dense graph class has almost linear neighborhood
    10complexity: for every ε > 0 there is a constant *c* such that every
    11member *G* and every nonempty vertex subset *A* satisfy
    12|{N(v) ∩ A : v ∈ V(G)}| ≤ *c* · |A|^(1+ε).
    13
    14This is the radius-1 case of the theorem of Eickmeyer, Giannopoulou,
    15Kreutzer, Kwon, Pilipczuk, Rabinovich and Siebertz, who prove the
    16corresponding bound for the traces of *r*-balls for every radius *r*.
    17The source lecture notes discuss neighborhood complexity but cite the
    18almost-linear bound as a result of the literature rather than proving
    19it; the proof accompanying this submission derives the radius-1 case
    20from the subpolynomial weak-coloring-number theorem stated here.
    21
    22# Formalization notes
    23
    24The conclusion is the shared predicate `HasAlmostLinearNC` of the
    25neighborhood complexity concept; the hypothesis is the shallow-minor
    26definition of the nowhere dense concept, so the statement adds nothing
    27of its own. Only radius 1 — traces of neighborhoods rather than of
    28*r*-balls — is claimed: the general radius is a separate statement with
    29a separate proof and is not stated here.
    30-/
    31
    32namespace Lax12.NowhereDenseNC
    33
    34open Lax12.GraphClasses Lax12.NeighborhoodComplexity Lax12.NowhereDenseClasses
    35
    36/-- Nowhere dense graph classes have almost linear neighborhood
    37complexity. -/
    38axiom hasAlmostLinearNC_of_nowhereDense
    39 (C : GraphClass) (h : NowhereDense C) :
    40 HasAlmostLinearNC C
    41
    42end Lax12.NowhereDenseNC
    43
    Show Proof

    Formalization notes

    The conclusion is the shared predicate HasAlmostLinearNCHasAlmostLinearNC of the neighborhood complexity concept; the hypothesis is the shallow-minor definition of the nowhere dense concept, so the statement adds nothing of its own. Only radius 1 — traces of neighborhoods rather than of r-balls — is claimed: the general radius is a separate statement with a separate proof and is not stated here.

    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…