FormalConjectures/ErdosProblems/618.lean

GitHub source file

2 declarations, 1 contain sorry, 0 declared as axioms

1. def Erdos618.h2 Documented declaration: h2 line 42 source

   Source documentation

   For a graph G on Fin n, h2 G is the smallest number of edges that need to be added to G so that the resulting supergraph has diameter at most 2 (every two distinct vertices are adjacent or have a common neighbour) and is still triangle-free (CliqueFree 3). By the sInf convention on ℕ, h2 G = 0 if no such supergraph exists.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, SimpleGraph, Fin

   Proof uses: InfSet.sInf, Set.ofPred, Exists, And, LE.le, SimpleGraph.CliqueFree, OfNat.ofNat, Ne, Or, SimpleGraph.Adj, Eq, Finset.card, Sym2, SDiff.sdiff, Finset, SimpleGraph.edgeFinset, Classical.propDecidable

   9 instances, coercions and auxiliary constants left out.

   noncomputable def h2 {n : ℕ} (G : SimpleGraph (Fin n)) : ℕ :=
   …

2. theorem Erdos618.erdos_618 For a triangle-free graph $G$ let $h_2(G)$ be the smallest number of edges that need to be added to $G$ so that it has diameter $2$ and is still triangle-free sorry line 62 source

   Source documentation

   For a triangle-free graph $G$ let $h_2(G)$ be the smallest number of edges that need to be added to $G$ so that it has diameter $2$ and is still triangle-free. Is it true that if $G$ has maximum degree $o(n^{1/2})$ then $h(G)=o(n^2)$?

   A problem of Erdős, Gyárfás, and Ruszinkó [EGR98]. Simonovits showed that there exist graphs $G$ with maximum degree $\gg n^{1/2}$ and $h_2(G)\gg n^2$. Alon has observed this problem is essentially identical to [134], and his solution in this note also solves this problem in the affirmative.

   L4DEL explanation

   For a triangle-free graph $G$ let $h_2(G)$ be the smallest number of edges that need to be added to $G$ so that it has diameter $2$ and is still triangle-free. Is it true that if $G$ has maximum degree $o(n^{1/2})$ then $h(G)=o(n^2)$? A problem of Erdős, Gyárfás, and Ruszinkó [EGR98]. Simonovits showed that there exist graphs $G$ with maximum degree $\gg n^{1/2}$ and $h_2(G)\gg n^2$. Alon has observed this problem is essentially identical to [134], and his solution in this note also solves this problem in the affirmative.

   Sources and attribution: Pinned Lean source (1646ca16afd6)

   depends on sorry what this means

   Statement uses: Iff, True, Nat, SimpleGraph, Fin, SimpleGraph.CliqueFree, OfNat.ofNat, Asymptotics.IsLittleO, Real, Filter.atTop, SimpleGraph.maxDegree, Classical.propDecidable, SimpleGraph.Adj, HPow.hPow, HDiv.hDiv, Erdos618.h2

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

   38 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_618 : answer(True) ↔
       ∀ (G : ∀ n : ℕ, SimpleGraph (Fin n)),
         (∀ n, (G n).CliqueFree 3) →
         (fun n => ((G n).maxDegree : ℝ)) =o[atTop] (fun n => (n : ℝ) ^ ((1 : ℝ) / 2)) →
         (fun n => (h2 (G n) : ℝ)) =o[atTop] (fun n => (n : ℝ) ^ 2) := by
   …

   Mentions: Erdos618.h2