Erdős problem 134
Let and be sufficiently large in terms of and . Let be a triangle-free graph on vertices with maximum degree . Can be made into a triangle-free graph with diameter by adding at most edges?
Sources
FormalConjectures/ErdosProblems/
134.lean
Let and be sufficiently large in terms of and . Let be a triangle-free graph on vertices with maximum degree . Can be made into a triangle-free graph with diameter by adding at most edges?
Asked by Erdős and Gyárfás, who proved that this is the case when has maximum degree . A construction of Simonovits shows that this conjecture is false if we just have maximum degree , for some large enough . In this note Alon solves this problem in a strong form, in particular proving that a triangle-free graph on vertices with maximum degree can be made into a triangle-free graph with diameter by adding at most edges.
True ↔ ∀ (ε δ : ℝ), 0 < ε → 0 < δ → ∃ N, ∀ n ≥ N, ∀ (G : SimpleGraph (Fin n)), G.CliqueFree 3 → (∀ (v : Fin n), ↑(G.degree v) < (↑n).rpow (1 / 2 - ε)) → ∃ H, G ≤ H ∧ H.CliqueFree 3 ∧ (∀ (x y : Fin n), x ≠ y → H.Adj x y ∨ ∃ z, H.Adj x z ∧ H.Adj z y) ∧ ↑(H.edgeFinset \ G.edgeFinset).card ≤ δ * ↑n ^ 2