Erdős Problem 904

References:

• erdosproblems.com/904
• [BoEr75] Bollobás, B. and Erdős, P., Unsolved Problems. Proc. Fifth British Combinatorial Conf. (1975), 678-680.
• [Er75] Erdős, P., Some recent progress on extremal problems in graph theory. Congr. Numer. (1975), 3-14.
• [Ed78] Edwards, C. S., Complete subgraphs with largest sum of vertex degrees. (1978), 293-306.
• [Fa92] Faudree, Ralph J., Complete subgraphs with large degree sums. J. Graph Theory (1992), 327-334.
• [BoNi05] Bollobás, Béla and Nikiforov, Vladimir, The sum of degrees in cliques. Electron. J. Combin. (2005), Note 21, 10.

@[reducible, inline]

abbrev Erdos904.n (V : Type u_1) [Fintype V] : ℕ

An abbreviation for the fixed number of vertices $n$ in the graph.

Equations

• Erdos904.n V = Fintype.card V

@[reducible, inline]

abbrev Erdos904.turanNumber (n r : ℕ) : ℕ

The number of edges of the Turán graph $T(n, r)$, i.e. the Turán number.

Equations

• Erdos904.turanNumber n r = (SimpleGraph.turanGraph n r).edgeFinset.card

theorem Erdos904.erdos_904 : True ↔ ∀ (V : Type u_1) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj], ∀ r ∈ Set.Icc 1 (n V), turanNumber (n V) r ≤ G.edgeFinset.card → ∃ (s : Finset V), G.IsNClique r s ∧ 2 * r * G.edgeFinset.card ≤ n V * ∑ v ∈ s, G.degree v

Let $r\geq 2$ and let $t_r(n)$ be the Turán number (the maximal number of edges in a graph on $n$ vertices with no $K_{r+1}$).

If $G$ is a graph with $n$ vertices and $m\geq t_r(n)$ edges there exists a clique on $r$ vertices, say $x_1,\ldots,x_r$, such that[d(x_1)+\cdots+d(x_r)\geq \frac{2rm}{n}.]

A conjecture of Bollobás and Erdős. This was conjectured in [Er75] only in the special case $r=3$. Edwards [Ed78] proved the conjecture for $2\leq r\leq 8$ (under the additional assumption that $n\geq r^2$). Faudree [Fa92] proved the conjecture for all $r\geq 2$ provided $n>\frac{r-1}{4}r^2$. The full conjecture was proved by Bollobás and Nikiforov [BoNi05].