Erdős Problem 61 -- Erdős–Hajnal Conjecture

Reference: erdosproblems.com/61

def Erdos61.IsErdosHajnalLowerBound {α : Type u_1} [Fintype α] [DecidableEq α] (H : SimpleGraph α) (f : ℕ → ℝ) : Prop

Equations

• Erdos61.IsErdosHajnalLowerBound H f = ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), (¬∃ (g : α ↪ Fin n), H = SimpleGraph.comap (⇑g) G) → ↑G.indepNum ≥ f n ∨ ↑G.cliqueNum ≥ f n

theorem Erdos61.erdos_61 : True ↔ ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (H : SimpleGraph α), ∃ c > 0, IsErdosHajnalLowerBound H fun (n : ℕ) => ↑n ^ c

The Erdős–Hajnal Conjecture states that there is a constant $c(H) > 0$ for each $H$ such that we can take $f(n) = n^{c(H)}$ in the above formulation.

theorem Erdos61.erdos_61.variants.erha89 {α : Type u_1} [Fintype α] [DecidableEq α] (H : SimpleGraph α) : ∃ c > 0, IsErdosHajnalLowerBound H fun (n : ℕ) => Real.exp (c * √(Real.log ↑n))

Erdős and Hajnal [ErHa89] proved that we can take $f(n) = \exp(c_H \sqrt{\log n})$ for some constant $c_H > 0$ dependending on $H$.

[ErHa89] Erdős, P. and Hajnal, A., Ramsey-type theorems. Discrete Appl. Math. (1989), 37-52.

theorem Erdos61.erdos_61.variants.bnss23 {α : Type u_1} [Fintype α] [DecidableEq α] (H : SimpleGraph α) : ∃ c > 0, IsErdosHajnalLowerBound H fun (n : ℕ) => Real.exp (c * √(Real.log ↑n * Real.log (Real.log ↑n)))

Bucić, Nguyen, Scott, and Seymour [BNSS23] improved this to $f(n) = \exp(c_H \sqrt{\log n \log \log n})$ for some constant $c_H > 0$ dependending on $H$.

[BNSS23] Bucić, M. and Nguyen, T. and Scott, A. and Seymour, P., A loglog step towards Erdos-Hajnal