English
If a graph G is K_r+1-free on n vertices and its minimum degree exceeds a specified bound, then G is r+1-colourable.
Русский
Если граф G не содержит K_r+1 и имеет n вершин, и его минимальная степень выше заданного предела, то G цветуется в r+1 цветов.
LaTeX
$$$$ \\text{If } G.CliqueFree(r+1) \\text{ and } (3r-4)\\,n/(3r-1) < G.minDegree, \\text{ then } G.Colorable(r). $$$$
Lean4
/-- If `G` is a `Kᵣ₊₂`-free graph with `n` vertices containing a `Wᵣ,ₖ` but no `Wᵣ,ₖ₊₁`
then `G.minDegree ≤ (2 * r + k) * n / (2 * r + k + 3)`
-/
theorem minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ [Fintype α] (hm : G.FiveWheelLikeFree r (k + 1)) :
G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3) :=
by
let X : Finset α := {x | ∀ ⦃y⦄, y ∈ s ∩ t → G.Adj x y}
let W :=
{ v } ∪
({ w₁ } ∪ ({ w₂ } ∪ (s ∪ t)))
-- Any vertex in `X` has at least 3 non-neighbors in `W` (otherwise we could build a bigger wheel)
have dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z}) := by
intro _ hx
by_contra! h
obtain ⟨_, _, hW⟩ :=
hw.exists_isFiveWheelLike_succ_of_not_adj_le_two hcf (by simpa [X] using hx) <| Nat.le_of_succ_le_succ h
exact hm hW
have one_le (x : α) : 1 ≤ #({z ∈ { v } ∪ ({ w₁ } ∪ ({ w₂ } ∪ (s ∪ t))) | ¬G.Adj x z}) :=
let ⟨_, hz⟩ := hw.isNClique_fst_left.exists_not_adj_of_cliqueFree_succ hcf x
card_pos.2
⟨_, mem_filter.2 ⟨by grind, hz.2⟩⟩
-- Since every vertex has at least one non-neighbor in `W` we now have the following upper bound
-- `∑ w ∈ W, H.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)`
have bdW :=
sum_degree_le_of_le_not_adj dXle
(fun y _ ↦ one_le y)
-- By the definition of `X`, any `x ∈ Xᶜ` has at least one non-neighbour in `X`.
have xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z}) :=
by
intro x hx
apply card_pos.2
obtain ⟨_, hy⟩ : ∃ y ∈ s ∩ t, ¬G.Adj x y := by
contrapose! hx
simpa [X] using hx
exact
⟨_, mem_filter.2 hy⟩
-- So we also have an upper bound on the degree sum over `s ∩ t`
-- `∑ w ∈ s ∩ t, H.degree w ≤ #Xᶜ * (#(s ∩ t) - 1) + #X * #(s ∩ t)`
have bdX := sum_degree_le_of_le_not_adj xcle (fun _ _ ↦ Nat.zero_le _)
rw [compl_compl, tsub_zero, add_comm] at bdX
rw [Nat.le_div_iff_mul_le <| Nat.add_pos_right _ zero_lt_three]
have Wc : #W + k = 2 * r + 3 := by
change #(insert _ <| insert _ <| insert _ _) + _ = _
grind [card_inter_add_card_union]
-- The sum of the degree sum over `W` and twice the degree sum over `s ∩ t`
-- is at least `G.minDegree * (#W + 2 * #(s ∩ t))` which implies the result
calc
_ ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w :=
by
simp_rw [add_assoc, add_comm k, ← add_assoc, ← Wc, add_assoc, ← two_mul, mul_add, ← hw.card_inter,
card_eq_sum_ones, ← mul_assoc, mul_sum, mul_one, mul_comm 2]
gcongr with i <;> exact minDegree_le_degree ..
_ ≤ #X * (#W - 3 + 2 * k) + #Xᶜ * ((#W - 1) + 2 * (k - 1)) := by grind
_ ≤ _ :=
by
by_cases hk :
k =
0 -- so `s ∩ t = ∅` and hence `Xᶜ = ∅`
· have Xu : X = univ := by
rw [← hw.card_inter, card_eq_zero] at hk
exact eq_univ_of_forall fun _ ↦ by simp [X, hk]
subst k
rw [add_zero] at Wc
simp [Xu, Wc, mul_comm]
have w3 : 3 ≤ #W :=
two_lt_card.2
⟨_, mem_insert_self .., _, by simp [W], _, by simp [W], hw.isPathGraph3Compl.ne_fst,
hw.isPathGraph3Compl.ne_snd, hw.isPathGraph3Compl.fst_ne_snd⟩
have hap : #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k := by omega
rw [hap, ← add_mul, card_add_card_compl, mul_comm, two_mul, ← add_assoc]
gcongr
cutsat
