Linear Neighbourhood Complexity

Lax9.NeighborhoodComplexity · concepts/Lax9/NeighborhoodComplexity.lean · lax-9

definition

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

    Definition

    For a finite simple graph GG and a natural number pp, the neighbourhood complexity πG(p)π_G(p) is the maximum, over sets XX of pp vertices, of the number of distinct traces on XX of the neighbourhoods of vertices outside XX. A graph class has linear neighbourhood complexity if πG(p)π_G(p) is bounded by a constant multiple of pp for every positive pp.

    Concept map
    2 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    Lean source view on GitHub

    1import Lax9.MergeWidth
    2
    3/-!
    4---
    5title: Linear Neighbourhood Complexity
    6type: definition
    7---
    8For a finite simple graph GG and a natural number pp, the neighbourhood
    9complexity πG(p)π_G(p) is the maximum, over sets XX of pp vertices, of the number
    10of distinct traces on XX of the neighbourhoods of vertices outside XX. A
    11graph class has linear neighbourhood complexity if πG(p)π_G(p) is bounded by a
    12constant multiple of pp for every positive pp.
    13-/
    14
    15namespace Lax9.NeighborhoodComplexity
    16
    17open Lax9.MergeWidth
    18open scoped Classical
    19
    20universe u
    21
    22variable {V : Type u} [Fintype V]
    23
    24/-- The neighbourhood complexity πG(p)π_G(p) of a finite simple graph GG. -/
    25noncomputable def neighborhoodComplexity (G : SimpleGraph V) (p : ℕ) : ℕ :=
    26 (Finset.univ.powersetCard p).sup fun X =>
    27 ((Finset.univ \ X).image fun v => X.filter fun u => G.Adj v u).card
    28
    29/-- A graph class has linear neighbourhood complexity if πG(p)≤cpπ_G(p) ≤ c p for
    30some constant cc and every positive pp. -/
    31def LinearNeighborhoodComplexity (C : GraphClass) : Prop :=
    32 ∃ c : ℕ, ∀ ⦃V : Type⦄ [Fintype V] (G : SimpleGraph V), C G → ∀ p, 1 ≤ p →
    33 neighborhoodComplexity G p ≤ c * p
    34
    35end Lax9.NeighborhoodComplexity
    36

    Discussion

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

    Loading discussion…