Lax Lean Archive

Nowhere dense classes have almost linear neighborhood complexity

Lax199508.NowhereDenseNC · concepts/Lax199508/NowhereDenseNC.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 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.

    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.NeighborhoodComplexity
    2import Lax199508.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 Lax199508.NowhereDenseNC
    33
    34open Lax199508.GraphClasses Lax199508.NeighborhoodComplexity Lax199508.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 Lax199508.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

    Discussion

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

    Loading discussion…