Lax12.NeighborhoodComplexity

Neighborhood complexity

concepts/Lax12/NeighborhoodComplexity.lean · lax-12

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

The neighborhood complexity of a graph G on a vertex set A counts the distinct traces of vertex neighborhoods on A, that is, the sets N(v) ∩ A for v ranging over all vertices of G. A graph class has almost linear neighborhood complexity if for every ε > 0 there is a constant c such that every member G and every nonempty vertex subset A leave at most c · |A|^(1+ε) traces — neighborhood complexity |A|^(1+o(1)).

Lean source view on GitHub

1	import Lax12.GraphClasses
2	import Mathlib.Data.Set.Card
3	import Mathlib.Analysis.SpecialFunctions.Pow.Real
4
5	/-!
6	---
7	title: Neighborhood complexity
8	type: definition
9	---
10	The neighborhood complexity of a graph G on a vertex set A counts
11	the distinct traces of vertex neighborhoods on A, that is, the sets
12	N(v) ∩ A for v ranging over all vertices of G. A graph class has
13	almost linear neighborhood complexity if for every ε > 0 there is a
14	constant c such that every member G and every nonempty vertex subset
15	A leave at most c · \|A\|^(1+ε) traces — neighborhood complexity
16	\|A\|^(1+o(1)).
17
18	# Formalization notes
19
20	The trace count is the natural cardinality (`Set.ncard`) of the set of
21	traces; on the finite carriers where it is used this is the exact count.
22	(Over an infinite vertex type with infinitely many traces `ncard` takes
23	the junk value 0; every use in this submission is on `Fin n`.) Working
24	with `Set` rather than `Finset` keeps the trace literally `N(v) ∩ A`
25	and needs no decidability instances.
26
27	The bound is stated for nonempty `A` only: the empty set always has
28	exactly one trace (the empty trace), while `c · 0^(1+ε) = 0`, so the
29	literal inequality must exclude `A = ∅` — and nothing is lost by doing
30	so. The exponent is a real power of the cast cardinality, and the
31	constant `c` is real.
32
33	The class-level predicate follows the shape of the other asymptotic
34	predicates of this submission (`HasSubpolynomialDensity`,
35	`HasSubpolynomialWcol`): the constant depends on ε alone and the bound
36	is uniform over the members of the class and over the vertex subsets of
37	each member.
38	-/
39
40	namespace Lax12.NeighborhoodComplexity
41
42	open Lax12.GraphClasses
43
44	/-- The number of distinct neighborhood traces `N(v) ∩ A` that the
45	vertices of `G` leave on the vertex set `A`. -/
46	noncomputable def traceCount {V : Type*} (G : SimpleGraph V)
47	(A : Set V) : ℕ :=
48	{S : Set V \| ∃ v : V, S = G.neighborSet v ∩ A}.ncard
49
50	/-- Every graph in the class leaves at most `c · \|A\|^(1+ε)` neighborhood
51	traces on every nonempty vertex subset `A`, where `c` depends only on
52	`ε > 0`: neighborhood complexity `\|A\|^(1+o(1))`. -/
53	def HasAlmostLinearNC (C : GraphClass) : Prop :=
54	∀ ε : ℝ, 0 < ε → ∃ c : ℝ,
55	∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G →
56	∀ A : Set (Fin n), A.Nonempty →
57	(traceCount G A : ℝ) ≤ c * (A.ncard : ℝ) ^ (1 + ε)
58
59	end Lax12.NeighborhoodComplexity
60

Formalization notes

The trace count is the natural cardinality ( $Set.ncard$ ) of the set of traces; on the finite carriers where it is used this is the exact count. (Over an infinite vertex type with infinitely many traces $ncard$ takes the junk value 0; every use in this submission is on $Fin n$ .) Working with $Set$ rather than $Finset$ keeps the trace literally $N(v) ∩ A$ and needs no decidability instances.

The bound is stated for nonempty $A$ only: the empty set always has exactly one trace (the empty trace), while $c · 0^(1+ε) = 0$ , so the literal inequality must exclude $A = ∅$ — and nothing is lost by doing so. The exponent is a real power of the cast cardinality, and the constant $c$ is real.

The class-level predicate follows the shape of the other asymptotic predicates of this submission ( $HasSubpolynomialDensity$ , $HasSubpolynomialWcol$ ): the constant depends on ε alone and the bound is uniform over the members of the class and over the vertex subsets of each member.

Builds on

Lax12.GraphClasses

Used by

From Mathlib

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…

Lax Lean Archive

Neighborhood complexity

Flags

Flag this concept