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

Reference: erdosproblems.com/61

For a graph $H$, consider all graphs $G$ that do not contain $H$ as an induced subgraph. We would like to find a lower bound $f(n)$ such that every such $G$ on $n$ vertices has a clique or independent set of size $\ge f(n)$ for sufficiently large $n$.

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 : (∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (H : SimpleGraph α), ∃ c > 0, IsErdosHajnalLowerBound H fun (n : ℕ) => ↑n ^ c) ↔ sorry

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