Greedy colouring

This file proves the greedy colouring bound χ(G) ≤ Δ(G) + 1: a finite simple graph whose vertices all have degree at most d can be properly coloured with d + 1 colours.

Main statements

• exists_color_not_used: a vertex of degree at most d always leaves one of d + 1 colours unused among its coloured neighbours.
• exists_coloring_on: every finite set of vertices admits a proper colouring with d + 1 colours.
• chromaticNumber_le_maxDegree_add_one: the bound χ(G) ≤ d + 1 for any d ≥ Δ(G), and chromaticNumber_le_maxDegree_add_one' for the usual form χ(G) ≤ Δ(G) + 1.

theorem SimpleGraph.exists_color_not_used {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {d : ℕ} (hd : G.maxDegree ≤ d) (a : V) (s : Finset V) (c : V → Fin (d + 1)) : ∃ (x : Fin (d + 1)), ∀ v ∈ s, G.Adj a v → c v ≠ x

A vertex a has at most d neighbours, so among d + 1 colours there is always one that no neighbour of a lying in s uses.

theorem SimpleGraph.exists_coloring_on {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {d : ℕ} (hd : G.maxDegree ≤ d) (s : Finset V) : ∃ (c : V → Fin (d + 1)), ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v

Greedy colouring. Every finite set of vertices can be properly coloured with d + 1 colours, by induction on the set of vertices coloured so far.

theorem SimpleGraph.chromaticNumber_le_maxDegree_add_one {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {d : ℕ} (hd : G.maxDegree ≤ d) : G.chromaticNumber ≤ ↑d + 1

Any upper bound d on the maximum degree bounds the chromatic number by d + 1.

theorem SimpleGraph.chromaticNumber_le_maxDegree_add_one' {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.chromaticNumber ≤ ↑G.maxDegree + 1

The usual form of the greedy bound: χ(G) ≤ Δ(G) + 1.