Counting high-degree vertices without a high-degree triangle #
The high-degree vertices span a triangle-free graph. A common-neighbour
count at the ends of one edge gives the exact -4 correction needed later.
theorem
LeanPool.DrossFractionalTriangleDecomposition.nb_bound_tight
{V : Type u_1}
[Fintype V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(_h : 9 * Fintype.card V ≤ 10 * G.minDegree)
(_hn20 : 20 ≤ Fintype.card V)
(hdef2 : 2 ≤ Fintype.card V - G.minDegree)
(hNoHDT :
∀ (u v w : V),
G.Adj u v →
G.Adj u w →
G.Adj v w → G.minDegree + 2 ≤ G.degree u → G.minDegree + 2 ≤ G.degree v → G.minDegree + 2 ≤ G.degree w → False)
:
Without a triangle whose three vertices have degree at least
minDegree + 2, the number of such vertices is at most twice the
deficiency minus four, provided the deficiency is at least two.