Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit ba34061e3cf12dfc8297610d5d7b3f0afac7ec54; import paths adapted.

Teorema 2.4 de Kierstead–Kostochka (forma divisible)

core: si |S| = s (r + 1), |P| = r + 1 y G[S] tiene grado máximo ≤ r, existe una coloración propia de S con paleta P cuyas clases tienen todas tamaño s.

Inducción primaria en el número de aristas de G[S]; inducción secundaria (main_lemma) en el número q de clases inaccesibles de una coloración casi equitativa.

theorem HajnalSzemeredi.bminus {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} {TU : Finset ℕ} (h : Ctx G S P c r s lo hi) (hch : CountHyp G S c (acc G S P c lo) (P \ acc G S P c lo) TU r s) {y₁ : V} (hy₁ : y₁ ∈ part S c (P \ acc G S P c lo)) : (part S c (P \ acc G S P c lo)).erase y₁ ⊆ S ∧ edgeCount G ((part S c (P \ acc G S P c lo)).erase y₁) < edgeCount G S ∧ ((part S c (P \ acc G S P c lo)).erase y₁).card = s * ((P \ acc G S P c lo).card - 1 + 1) ∧ DegLe G ((part S c (P \ acc G S P c lo)).erase y₁) ((P \ acc G S P c lo).card - 1)

Hechos sobre B⁻ = B \ {y₁} necesarios para aplicar la hipótesis de inducción primaria.

theorem HajnalSzemeredi.main_lemma {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {r s lo : ℕ} (IH : ∀ S' ⊆ S, edgeCount G S' < edgeCount G S → ∀ (P' : Finset ℕ) (r' : ℕ), P'.card = r' + 1 → S'.card = s * (r' + 1) → DegLe G S' r' → ∃ (c : V → ℕ), IsEq G S' P' c s) (hdeg : DegLe G S r) (hP : P.card = r + 1) (c : V → ℕ) (hi : ℕ) : IsNear G S P c s lo hi → ∃ (c' : V → ℕ), IsEq G S P c' s

Lema principal (inducción secundaria en el número de clases inaccesibles).

theorem HajnalSzemeredi.exists_equipartition {V : Type u_1} (P : Finset ℕ) (s : ℕ) (S : Finset V) : S.card = s * P.card → ∃ (c : V → ℕ), Into S c P ∧ ∀ i ∈ P, (cls S c i).card = s

Existencia de una partición de S en clases de tamaño s indexadas por P.

theorem HajnalSzemeredi.core {V : Type u_1} (n : ℕ) (G : SimpleGraph V) (S : Finset V) (P : Finset ℕ) (r s : ℕ) : edgeCount G S = n → P.card = r + 1 → S.card = s * (r + 1) → DegLe G S r → ∃ (c : V → ℕ), IsEq G S P c s

Teorema 2.4 (forma divisible).