Lax5.NeighborhoodComplexity
Neighborhood complexity
concepts/Lax5/NeighborhoodComplexity.lean · Lax5
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 Lax5.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 | |
| 34 | namespace Lax5.NeighborhoodComplexity |
| 35 | |
| 36 | open Lax5.GraphClasses |
| 37 | |
| 38 | /-- The number of distinct neighborhood traces `N(v) ∩ A` that the |
| 39 | vertices of `G` leave on the vertex set `A`. -/ |
| 40 | noncomputable def traceCount {V : Type*} (G : SimpleGraph V) |
| 41 | (A : Set V) : ℕ := |
| 42 | {S : Set V | ∃ v : V, S = G.neighborSet v ∩ A}.ncard |
| 43 | |
| 44 | /-- Every graph in the class leaves at most `c · |A|^(1+ε)` neighborhood |
| 45 | traces on every nonempty vertex subset `A`, where `c` depends only on |
| 46 | `ε > 0`: neighborhood complexity `|A|^(1+o(1))`. -/ |
| 47 | def HasAlmostLinearNC (C : GraphClass) : Prop := |
| 48 | ∀ ε : ℝ, 0 < ε → ∃ c : ℝ, |
| 49 | ∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G → |
| 50 | ∀ A : Set (Fin n), A.Nonempty → |
| 51 | (traceCount G A : ℝ) ≤ c * (A.ncard : ℝ) ^ (1 + ε) |
| 52 | |
| 53 | end Lax5.NeighborhoodComplexity |
| 54 |
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.