Hajnal–Szemerédi theorem

TheoremEquitable coloring with more colors than the maximum degree#✓fully proved

Let \(G\) be a simple graph on a finite vertex set with maximum degree \(\Delta(G)\), and let \(k\) be a natural number with \(\Delta(G) < k\). Then \(G\) has a proper coloring with the \(k\) colors \(0, 1, \dots, k-1\) that is equitable: for any two colors \(i\) and \(j\), the number of vertices of color \(i\) is at most one more than the number of vertices of color \(j\).

public theorem exists_equitable_coloring_of_maxDegree_lt
    {V : Type*} [Fintype V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (k : ℕ) (hk : G.maxDegree < k) :
    ∃ C : G.Coloring (Fin k),
      ∀ i j : Fin k, (C.colorClass i).ncard ≤ (C.colorClass j).ncard + 1

Used by 1

Used byHajnal–Szemerédi theorem

TheoremHajnal–Szemerédi theorem#✓fully proved

Let \(G\) be a simple graph on a finite vertex set with maximum degree \(\Delta(G)\), and let \(k\) be a natural number with \(\Delta(G) < k\). Then \(G\) has a proper coloring with the \(k\) colors \(0, 1, \dots, k-1\) that is equitable: for any two colors \(i\) and \(j\), the number of vertices of color \(i\) is at most one more than the number of vertices of color \(j\).

public theorem hajnal_szemeredi_equitable_coloring
    {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (k : ℕ) (hk : G.maxDegree < k) :
    ∃ C : G.Coloring (Fin k),
      ∀ i j : Fin k, (C.colorClass i).ncard ≤ (C.colorClass j).ncard + 1

Sources

A. Hajnal and E. Szemerédi, "Proof of a conjecture of P. Erdős", Combinatorial Theory and Its Applications II, Colloq. Math. Soc. János Bolyai 4 (1970), 601-623.

Uses 1

Proof usesEquitable coloring with more colors than the maximum degree

DefinitionErdős Problem 914 on clique factors and equitable colourings#✓fully proved

The proposition asserts that for all integers \(r \ge 2\) and \(m \ge 1\) and every finite simple graph \(G\) with exactly \(rm\) vertices, (a) if every vertex of \(G\) has degree at least \(m(r - 1)\), then \(G\) contains \(m\) pairwise disjoint cliques of \(r\) vertices each, and (b) if every vertex of \(G\) has degree at most \(m - 1\), then \(G\) has a proper colouring with \(m\) colours in which every colour class has exactly \(r\) vertices.

def conjecture : Prop :=
  (∀ {r m : ℕ}, 2 ≤ r → 1 ≤ m → ∀ {V : Type*} [Fintype V] (G : SimpleGraph V)
    [DecidableRel G.Adj], Fintype.card V = r * m → m * (r - 1) ≤ G.minDegree →
    ∃ K : Fin m → Finset V, (∀ i, G.IsNClique r (K i)) ∧
      Pairwise fun i j => Disjoint (K i) (K j)) ∧
  (∀ {r m : ℕ}, 2 ≤ r → 1 ≤ m → ∀ {V : Type*} [Fintype V] (G : SimpleGraph V)
    [DecidableRel G.Adj], Fintype.card V = r * m → G.maxDegree ≤ m - 1 →
    ∃ C : G.Coloring (Fin m), ∀ i, (C.colorClass i).ncard = r)

Used by 1

Used byHajnal–Szemerédi theorem in clique-factor and equitable-colouring form

TheoremHajnal–Szemerédi theorem in clique-factor and equitable-colouring form#●ready to prove

For all integers \(r \ge 2\) and \(m \ge 1\) and every finite simple graph \(G\) with exactly \(rm\) vertices, (a) if every vertex of \(G\) has degree at least \(m(r - 1)\), then \(G\) contains \(m\) pairwise disjoint cliques of \(r\) vertices each, and (b) if every vertex of \(G\) has degree at most \(m - 1\), then \(G\) has a proper colouring with \(m\) colours in which every colour class has exactly \(r\) vertices.

This resolves Erdős Problem 914 affirmatively: part (a) was proved by Corrádi and Hajnal for \(r = 3\) and by Hajnal and Szemerédi for all \(r\), and part (b) is its equitable-colouring reformulation, obtained by applying (a) to the complement of \(G\).

public theorem_wanted conjecture_holds : conjecture

def conjecture : Prop :=
  (∀ {r m : ℕ}, 2 ≤ r → 1 ≤ m → ∀ {V : Type*} [Fintype V] (G : SimpleGraph V)
    [DecidableRel G.Adj], Fintype.card V = r * m → m * (r - 1) ≤ G.minDegree →
    ∃ K : Fin m → Finset V, (∀ i, G.IsNClique r (K i)) ∧
      Pairwise fun i j => Disjoint (K i) (K j)) ∧
  (∀ {r m : ℕ}, 2 ≤ r → 1 ≤ m → ∀ {V : Type*} [Fintype V] (G : SimpleGraph V)
    [DecidableRel G.Adj], Fintype.card V = r * m → G.maxDegree ≤ m - 1 →
    ∃ C : G.Coloring (Fin m), ∀ i, (C.colorClass i).ncard = r)

WantedExt/Combinatorics/ErdosProblem914Wanted.lean:35

Sources

A. Hajnal and E. Szemerédi, Proof of a conjecture of P. Erdős (1970), 601–623, https://mathscinet.ams.org/mathscinet-getitem?mr=297607; External Lean proof of Erdős Problem 914, plby/lean-proofs, https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/v4.29.1/ErdosProblems/Erdos914.lean.

Uses 1

Statement usesErdős Problem 914 on clique factors and equitable colourings

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.