Catalog/Sparsity/ColoringNumbers/Full.lean

1	import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
2	import Mathlib.Combinatorics.SimpleGraph.Paths
3	import Mathlib.Data.Set.Card
4
5	namespace Catalog.Sparsity.ColoringNumbers
6
7	variable {V : Type*} [DecidableEq V] [Fintype V] [LinearOrder V]
8
9	/-- The set of vertices strongly r-reachable from `v` with respect to the
10	linear order on `V`. A vertex `u ≤ v` is in `SReach G r v` when there
11	exists a path of length ≤ r from `v` to `u` whose internal vertices
12	are all strictly greater than `v`. (Def 2.1) -/
13	def SReach (G : SimpleGraph V) (r : ℕ) (v : V) : Set V :=
14	{u \| u ≤ v ∧ ∃ p : G.Walk v u, p.IsPath ∧ p.length ≤ r ∧
15	∀ i : ℕ, 0 < i → i < p.length → v < p.getVert i}
16
17	/-- The set of vertices weakly r-reachable from `v` with respect to the
18	linear order on `V`. A vertex `u ≤ v` is in `WReach G r v` when there
19	exists a path of length ≤ r from `v` to `u` whose internal vertices
20	are all strictly greater than `u`. (Def 2.1) -/
21	def WReach (G : SimpleGraph V) (r : ℕ) (v : V) : Set V :=
22	{u \| u ≤ v ∧ ∃ p : G.Walk v u, p.IsPath ∧ p.length ≤ r ∧
23	∀ i : ℕ, 0 < i → i < p.length → u < p.getVert i}
24
25	open Classical in
26	/-- The weak r-coloring number of `G` (per ordering). (Def 2.3) -/
27	noncomputable def wcol (G : SimpleGraph V) (r : ℕ) : ℕ :=
28	Finset.sup Finset.univ (fun v => (WReach G r v).ncard)
29
30	open Classical in
31	/-- The strong r-coloring number of `G` (per ordering). (Def 2.3) -/
32	noncomputable def scol (G : SimpleGraph V) (r : ℕ) : ℕ :=
33	Finset.sup Finset.univ (fun v => (SReach G r v).ncard)
34
35	end Catalog.Sparsity.ColoringNumbers
36