FormalConjectures/ErdosProblems/134.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

1. theorem Erdos134.erdos_134 Let $\epsilon,\delta>0$ and $n$ be sufficiently large in terms of $\epsilon$ and $\delta$ sorry line 40 source

   Source documentation

   Let $\epsilon,\delta>0$ and $n$ be sufficiently large in terms of $\epsilon$ and $\delta$. Let $G$ be a triangle-free graph on $n$ vertices with maximum degree $<n^{1/2-\epsilon}$. Can $G$ be made into a triangle-free graph with diameter $2$ by adding at most $\delta n^2$ edges?

   Asked by Erdős and Gyárfás, who proved that this is the case when $G$ has maximum degree $\ll \log n/\log\log n$. A construction of Simonovits shows that this conjecture is false if we just have maximum degree $\leq Cn^{1/2}$, for some large enough $C$. In this note Alon solves this problem in a strong form, in particular proving that a triangle-free graph on $n$ vertices with maximum degree $<n^{1/2-\epsilon}$ can be made into a triangle-free graph with diameter $2$ by adding at most $O(n^{2-\epsilon})$ edges.

   depends on sorry what this means

   Statement uses: Iff, True, Real, LT.lt, OfNat.ofNat, Exists, Nat, GE.ge, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, SimpleGraph.CliqueFree, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Real.rpow, HSub.hSub, HDiv.hDiv and 11 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   68 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_134 : answer(True) ↔
       ∀ (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ),
       ∃ N : ℕ, ∀ n ≥ N, ∀ (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
         G.CliqueFree 3 →
         (∀ v : Fin n, (G.degree v : ℝ) < Real.rpow (n : ℝ) ((1 : ℝ) / 2 - ε)) →
         ∃ (H : SimpleGraph (Fin n)) (_ : DecidableRel H.Adj),
           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 := by
   …