Catalog/Sparsity/ColoringNumberEquivalence/Full.lean

1	import Catalog.Sparsity.ColoringNumbers.Full
2	import Catalog.Sparsity.Admissibility.Full
3	import Catalog.Sparsity.ColoringNumberOrdering.Full
4	import Catalog.Sparsity.StrongColoringBoundByAdm.Full
5	import Mathlib.Tactic
6
7	open Catalog.Sparsity.ColoringNumbers
8	open Catalog.Sparsity.Admissibility
9
10	namespace Catalog.Sparsity.ColoringNumberEquivalence
11
12	variable {V : Type*} [Fintype V] [LinearOrder V]
13
14	/-- Corollary 2.7: wcol_r ≤ 1 + r · (adm_r - 1)^(r²) per ordering. -/
15	theorem wcol_le_of_adm (G : SimpleGraph V) (r : ℕ) :
16	wcol G r ≤ 1 + r * (adm G r - 1) ^ (r ^ 2) := by
17	have hscol :
18	scol G r ≤ 1 + (adm G r - 1) ^ r :=
19	Catalog.Sparsity.StrongColoringBoundByAdm.scol_le_one_add_adm_sub_one_pow G r
20	have hsub : scol G r - 1 ≤ (adm G r - 1) ^ r := by
21	rw [Nat.sub_le_iff_le_add]
22	simpa [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] using hscol
23	calc
24	wcol G r ≤ 1 + r * (scol G r - 1) ^ r :=
25	Catalog.Sparsity.ColoringNumberOrdering.wcol_le_of_scol G r
26	_ ≤ 1 + r * ((adm G r - 1) ^ r) ^ r := by
27	apply Nat.add_le_add_left
28	apply Nat.mul_le_mul_left
29	apply Nat.pow_le_pow_left
30	exact hsub
31	_ = 1 + r * (adm G r - 1) ^ (r * r) := by
32	rw [← Nat.pow_mul]
33	_ = 1 + r * (adm G r - 1) ^ (r ^ 2) := by
34	simp [pow_two]
35
36	end Catalog.Sparsity.ColoringNumberEquivalence
37