Lax9.NeighborhoodComplexity
Linear Neighbourhood Complexity
concepts/Lax9/NeighborhoodComplexity.lean · Lax9
Definition
For a finite simple graph and a natural number , the neighbourhood complexity is the maximum, over sets of vertices, of the number of distinct traces on of the neighbourhoods of vertices outside . A graph class has linear neighbourhood complexity if is bounded by a constant multiple of for every positive .
Lean source view on GitHub
| 1 | import Lax9.MergeWidth |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Linear Neighbourhood Complexity |
| 6 | type: definition |
| 7 | --- |
| 8 | For a finite simple graph $G$ and a natural number $p$, the neighbourhood |
| 9 | complexity $π_G(p)$ is the maximum, over sets $X$ of $p$ vertices, of the number |
| 10 | of distinct traces on $X$ of the neighbourhoods of vertices outside $X$. A |
| 11 | graph class has linear neighbourhood complexity if $π_G(p)$ is bounded by a |
| 12 | constant multiple of $p$ for every positive $p$. |
| 13 | -/ |
| 14 | |
| 15 | namespace Lax9.NeighborhoodComplexity |
| 16 | |
| 17 | open Lax9.MergeWidth |
| 18 | open scoped Classical |
| 19 | |
| 20 | universe u |
| 21 | |
| 22 | variable {V : Type u} [Fintype V] |
| 23 | |
| 24 | /-- The neighbourhood complexity $π_G(p)$ of a finite simple graph $G$. -/ |
| 25 | noncomputable 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) ≤ c p$ for |
| 30 | some constant $c$ and every positive $p$. -/ |
| 31 | def 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 | |
| 35 | end Lax9.NeighborhoodComplexity |
| 36 |
Imported
Mathlib imports
none