Degeneracy and greedy coloring
DefinitionDegeneracy on a vertex set#✓fully proved
Let \(G\) be a simple graph on a finite vertex type \(V\), let \(U \subseteq V\) and let \(k\) be a natural number. Then \(G\) is \(k\)-degenerate on \(U\) if every nonempty subset \(W \subseteq U\) contains a vertex \(v\) with at most \(k\) neighbors in \(W\).
def IsDegenerateOn {V : Type*} [Finite V] (G : SimpleGraph V) (U : Set V) (k : ℕ) : Prop :=
∀ W : Set V, W.Nonempty → W ⊆ U →
∃ v ∈ W, (G.neighborSet v ∩ W).ncard ≤ kUsed by 9
DefinitionDegenerate graph#✓fully proved
A simple graph \(G\) on a finite vertex type \(V\) is \(k\)-degenerate, for a natural number \(k\), if it is \(k\)-degenerate on the full vertex set \(V\): every nonempty set \(W\) of vertices contains a vertex with at most \(k\) neighbors in \(W\).
def IsDegenerate {V : Type*} [Finite V] (G : SimpleGraph V) (k : ℕ) : Prop :=
G.IsDegenerateOn Set.univ kUses 1 · Used by 8
TheoremDegeneracy on a vertex set is monotone in the degree bound#✓fully proved
Let \(G\) be a simple graph on a finite vertex type \(V\), let \(U \subseteq V\), and let \(k \le l\) be natural numbers. If \(G\) is \(k\)-degenerate on \(U\), then \(G\) is \(l\)-degenerate on \(U\).
theorem IsDegenerateOn.mono [Finite V] (h : G.IsDegenerateOn U k) (hkl : k ≤ l) :
G.IsDegenerateOn U lUses 1 · Used by 1
TheoremDegeneracy on a vertex set passes to subsets#✓fully proved
Let \(G\) be a simple graph on a finite vertex type \(V\), let \(T \subseteq U \subseteq V\) and let \(k\) be a natural number. If \(G\) is \(k\)-degenerate on \(U\), then \(G\) is \(k\)-degenerate on \(T\).
theorem IsDegenerateOn.of_subset [Finite V] (h : G.IsDegenerateOn U k) (hTU : T ⊆ U) :
G.IsDegenerateOn T kUses 1 · Used by 3
TheoremA degenerate graph is degenerate on every vertex set#✓fully proved
Let \(G\) be a simple graph on a finite vertex type \(V\) and let \(k\) be a natural number. If \(G\) is \(k\)-degenerate, then \(G\) is \(k\)-degenerate on every subset \(U \subseteq V\).
theorem IsDegenerate.isDegenerateOn [Finite V] (h : G.IsDegenerate k) (U : Set V) :
G.IsDegenerateOn U kUses 3 · Used by 2
TheoremA degenerate vertex set has a vertex of small degree#✓fully proved
Let \(G\) be a simple graph on a finite vertex set \(V\) and let \(s \subseteq V\) be nonempty. If \(G\) is \(k\)-degenerate on \(s\), then some vertex \(v \in s\) has at most \(k\) neighbors in \(s\).
theorem IsDegenerateOn.exists_small_vertex (s : Finset V)
(h : G.IsDegenerateOn (↑s : Set V) k) (hs : s.Nonempty) :
∃ v ∈ s, (G.neighborSet v ∩ ↑s).ncard ≤ kUses 1 · Used by 2
TheoremThe edgeless graph is degenerate#✓fully proved
For every natural number \(k\), the edgeless graph on a finite vertex set is \(k\)-degenerate.
theorem isDegenerate_bot (k : ℕ) : (⊥ : SimpleGraph V).IsDegenerate kUses 1
TheoremDegeneracy is monotone in the bound#✓fully proved
Let \(G\) be a simple graph on a finite vertex set. If \(G\) is \(k\)-degenerate and \(k \le l\), then \(G\) is \(l\)-degenerate.
theorem IsDegenerate.mono (h : G.IsDegenerate k) (hkl : k ≤ l) :
G.IsDegenerate lUses 2
TheoremBounded maximum degree implies degeneracy#✓fully proved
Let \(G\) be a simple graph on a finite vertex set. If every vertex of \(G\) has degree at most \(k\), then \(G\) is \(k\)-degenerate.
theorem IsDegenerate.of_forall_degree_le [Fintype V] [DecidableRel G.Adj]
(h : ∀ v, G.degree v ≤ k) : G.IsDegenerate kUses 1
DefinitionDegeneracy ordering#✓fully proved
Let \(G\) be a simple graph on a finite vertex set \(V\) and let \(k\) be a natural number. A map \(e : V \to \mathbb{N}\) is a degeneracy ordering of \(G\) with bound \(k\) if \(e\) is injective and every vertex \(v\) has at most \(k\) neighbors \(w\) with \(e(v) < e(w)\).
def IsDegeneracyOrdering (G : SimpleGraph V) (k : ℕ) (e : V → ℕ) : Prop :=
Function.Injective e ∧ ∀ v, (G.neighborSet v ∩ {w | e v < e w}).ncard ≤ kUsed by 1
TheoremDegeneracy orderings of a vertex set#✓fully proved
Let \(G\) be a simple graph on a finite vertex set \(V\) and let \(s \subseteq V\). If \(G\) is \(k\)-degenerate on \(s\), then there is a map \(e : V \to \mathbb{N}\), injective on \(s\), such that every \(v \in s\) has at most \(k\) neighbors \(w \in s\) with \(e(v) < e(w)\).
The proof removes a vertex of small degree in \(s\) and labels it \(0\).
theorem IsDegenerateOn.exists_injOn_ordering (s : Finset V)
(h : G.IsDegenerateOn (↑s : Set V) k) :
∃ e : V → ℕ, Set.InjOn e ↑s ∧
∀ v ∈ s, (G.neighborSet v ∩ {w ∈ (↑s : Set V) | e v < e w}).ncard ≤ kUses 3 · Used by 1
TheoremDegenerate graphs have degeneracy orderings#✓fully proved
If \(G\) is a \(k\)-degenerate simple graph on a finite vertex set \(V\), then \(G\) has a degeneracy ordering with bound \(k\): an injective map \(e : V \to \mathbb{N}\) such that every vertex \(v\) has at most \(k\) neighbors \(w\) with \(e(v) < e(w)\).
theorem IsDegenerate.exists_degeneracyOrdering (h : G.IsDegenerate k) :
∃ e : V → ℕ, G.IsDegeneracyOrdering k eUses 5
TheoremColoring a \(k\)-degenerate vertex set with \(k + 1\) colors#✓fully proved
Let \(G\) be a simple graph on a finite vertex set \(V\), let \(s \subseteq V\) and let \(k\) be a natural number. If \(G\) is \(k\)-degenerate on \(s\), then there is a map \(f : V \to \{0, 1, \dots, k\}\) such that \(f(a) \ne f(b)\) for all adjacent vertices \(a, b \in s\).
The proof removes a vertex of small degree and gives it a color absent from its neighborhood.
theorem IsDegenerateOn.exists_coloringFun (s : Finset V)
(h : G.IsDegenerateOn (↑s : Set V) k) :
∃ f : V → Fin (k + 1), ∀ a ∈ s, ∀ b ∈ s, G.Adj a b → f a ≠ f bUses 3 · Used by 1
Theorem\(k\)-degenerate graphs are \((k + 1)\)-colorable#✓fully proved
Let \(k\) be a natural number. Every \(k\)-degenerate simple graph on a finite vertex set is \((k + 1)\)-colorable.
theorem IsDegenerate.colorable (h : G.IsDegenerate k) : G.Colorable (k + 1)Sources
- Diestel, §5.1–5.2.
Uses 4 · Used by 1
TheoremChromatic number of a degenerate graph#✓fully proved
Let \(k\) be a natural number. If \(G\) is a \(k\)-degenerate simple graph on a finite vertex set, then the chromatic number of \(G\) is at most \(k + 1\).
theorem IsDegenerate.chromaticNumber_le (h : G.IsDegenerate k) :
G.chromaticNumber ≤ k + 1Uses 2
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.