The Caro--Wei independence bound

carowei is the classical greedy/random-order bound: every finite graph has an independent set of size at least ∑ v, 1 / (deg v + 1). It is proved here by the standard induction that deletes the closed neighbourhood of a minimum-degree vertex.

exists_independent_five specialises it to the shape the main theorem needs. The tangent-line estimate 1 / (d + 1) ≥ (5 - d) / 9, valid because (d - 2) ^ 2 ≥ 0, converts a degree-sum bound into a lower bound on the independence number, and integrality upgrades n / 3 > 4 to an independent set of size 5 once n ≥ 13.

def Erdos132ThreeChain.degree {α : Type u_1} (adj : α → α → Prop) [DecidableRel adj] (V : Finset α) (v : α) : ℕ

The degree of v in the graph that adj induces on the vertex set V.

Equations

• Erdos132ThreeChain.degree adj V v = (Finset.filter (adj v) V).card

theorem Erdos132ThreeChain.degree_mono {α : Type u_1} {adj : α → α → Prop} [DecidableRel adj] {V W : Finset α} (h : W ⊆ V) (v : α) : degree adj W v ≤ degree adj V v

theorem Erdos132ThreeChain.carowei {α : Type u_1} (adj : α → α → Prop) [DecidableRel adj] (hsymm : ∀ (a b : α), adj a b → adj b a) (hirr : ∀ (a : α), ¬adj a a) (V : Finset α) : ∃ S ⊆ V, (∀ p ∈ S, ∀ q ∈ S, ¬adj p q) ∧ ∑ v ∈ V, 1 / (↑(degree adj V v) + 1) ≤ ↑S.card

Caro--Wei. Every finite graph has an independent set of size at least the sum over its vertices of the reciprocal of one more than the degree.

theorem Erdos132ThreeChain.exists_independent_five {α : Type u_1} (adj : α → α → Prop) [DecidableRel adj] (hsymm : ∀ (a b : α), adj a b → adj b a) (hirr : ∀ (a : α), ¬adj a a) (V : Finset α) (hcard : 13 ≤ V.card) (hdeg : ∑ v ∈ V, degree adj V v ≤ 2 * V.card) : ∃ S ⊆ V, S.card = 5 ∧ ∀ p ∈ S, ∀ q ∈ S, ¬adj p q

A graph on at least thirteen vertices whose degrees sum to at most twice the number of vertices has an independent set of five vertices. The degree sum is twice the number of edges, so the hypothesis is the edge bound #edges ≤ #vertices.