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

Teorema de Hajnal–Szemerédi

• hajnalSzemeredi_exact: si |V| = s (r + 1) y Δ(G) ≤ r, hay una (r+1)-coloración propia cuyas clases tienen todas exactamente s vértices (forma del problema de Erdős #914).
• hajnalSzemeredi: si Δ(G) ≤ r, hay una (r+1)-coloración propia equitativa (los tamaños de dos clases cualesquiera difieren en a lo más uno).

La forma general se reduce a la exacta agregando un K_p disjunto (p < r + 1) para que el número de vértices sea divisible por r + 1; cada clase contiene a lo más un vértice agregado.

theorem HajnalSzemeredi.degLe_univ {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℕ} (h : ∀ (v : V), G.degree v ≤ r) : DegLe G Finset.univ r

Pasar del grado de Mathlib a DegLe sobre univ.

theorem HajnalSzemeredi.hajnalSzemeredi_exact {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (r s : ℕ) (hcard : Fintype.card V = s * (r + 1)) (h : ∀ (v : V), G.degree v ≤ r) : ∃ (C : G.Coloring (Fin (r + 1))), ∀ (i : Fin (r + 1)), {v : V | C v = i}.card = s

Forma exacta.

def HajnalSzemeredi.padAdj {V : Type u_1} (G : SimpleGraph V) (p : ℕ) : V ⊕ Fin p → V ⊕ Fin p → Prop

Adyacencia del grafo con un K_p disjunto agregado.

Equations

• HajnalSzemeredi.padAdj G p (Sum.inl u) (Sum.inl v) = G.Adj u v
• HajnalSzemeredi.padAdj G p (Sum.inr i) (Sum.inr j) = (i ≠ j)
• HajnalSzemeredi.padAdj G p x✝¹ x✝ = False

def HajnalSzemeredi.pad {V : Type u_1} (G : SimpleGraph V) (p : ℕ) : SimpleGraph (V ⊕ Fin p)

G ⊔ K_p (unión disjunta).

Equations

• HajnalSzemeredi.pad G p = { Adj := HajnalSzemeredi.padAdj G p, symm := ⋯, loopless := ⋯ }

theorem HajnalSzemeredi.card_classes_split {V : Type u_1} [Fintype V] {W : Type u_2} [DecidableEq W] {p : ℕ} (f : V ⊕ Fin p → W) (i : W) : {w : V ⊕ Fin p | f w = i}.card = {v : V | f (Sum.inl v) = i}.card + {j : Fin p | f (Sum.inr j) = i}.card

theorem HajnalSzemeredi.hajnalSzemeredi {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (r : ℕ) (h : ∀ (v : V), G.degree v ≤ r) : ∃ (C : G.Coloring (Fin (r + 1))), ∀ (i j : Fin (r + 1)), {v : V | C v = i}.card ≤ {v : V | C v = j}.card + 1

Teorema de Hajnal–Szemerédi.