Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax9.NeighborhoodComplexity

Linear Neighbourhood Complexity

concepts/Lax9/NeighborhoodComplexity.lean · lax-9

definition

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

    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.

    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

    Builds on

    Used by

    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…