English
Under the same hypothesis as the previous item, colorability holds.
Русский
При тех же предпосылках сохраняется цветообразность.
LaTeX
$$$$ \\text{If } \\text{hypotheses of the previous item hold, then } G.Colorable(r). $$$$
Lean4
/-- **Andrasfái-Erdős-Sós** theorem
If `G` is a `Kᵣ₊₁`-free graph with `n` vertices and `(3 * r - 4) * n / (3 * r - 1) < G.minDegree`
then `G` is `r + 1`-colorable, e.g. if `G` is `K₃`-free and `2 * n / 5 < G.minDegree` then `G`
is `2`-colorable.
-/
theorem colorable_of_cliqueFree_lt_minDegree [Fintype α] [DecidableRel G.Adj] (hf : G.CliqueFree (r + 1))
(hd : (3 * r - 4) * ‖α‖ / (3 * r - 1) < G.minDegree) : G.Colorable r := by
match r with
| 0 | 1 => aesop
| r + 2 =>
-- There is an edge maximal `Kᵣ₊₃`-free supergraph `H` of `G`
obtain ⟨H, hle, hmcf⟩ := @Finite.exists_le_maximal _ _ _ (fun H ↦ H.CliqueFree (r + 3)) G hf
apply Colorable.mono_left hle
by_contra! hnotcol
have hn : ¬H.IsCompleteMultipartite := fun hc ↦
hnotcol <|
hc.colorable_of_cliqueFree
hmcf.1
-- Hence `H` contains `Wᵣ₊₁,ₖ` but not `Wᵣ₊₁,ₖ₊₁`, for some `k < r + 1`
obtain ⟨k, _, _, _, _, _, hw, hlt, hm⟩ :=
exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite hmcf hn
classical
-- But the minimum degree of `G`, and hence of `H`, is too large for it to be `Wᵣ₊₁,ₖ₊₁`-free,
-- a contradiction.
have hD := hw.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ hmcf.1 <| hm _ <| lt_add_one _
have : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5) :=
by
apply (Nat.le_div_iff_mul_le <| Nat.succ_pos _).2 <| (mul_le_mul_iff_right₀ (_ + 2).succ_pos).1 _
rw [← mul_assoc, mul_comm (2 * r + 2 + k + 3), mul_comm _ (_ * ‖α‖)]
apply (Nat.mul_le_mul_right _ (Nat.div_mul_le_self ..)).trans
nlinarith
exact (hd.trans_le <| minDegree_le_minDegree hle).not_ge <| hD.trans <| this
