Catalog/Sparsity/ColoringNumbers/Contract.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): the maximum over
27	all vertices of the cardinality of the weak r-reachability set. (Def 2.3) -/
28	noncomputable def wcol (G : SimpleGraph V) (r : ℕ) : ℕ :=
29	Finset.sup Finset.univ (fun v => (WReach G r v).ncard)
30
31	open Classical in
32	/-- The strong r-coloring number of `G` (per ordering): the maximum over
33	all vertices of the cardinality of the strong r-reachability set. (Def 2.3) -/
34	noncomputable def scol (G : SimpleGraph V) (r : ℕ) : ℕ :=
35	Finset.sup Finset.univ (fun v => (SReach G r v).ncard)
36
37	end Catalog.Sparsity.ColoringNumbers
38