The exact edge-count bound

Split the degree sum into vertices of degree at least minDegree + 2 and the remaining vertices. The sharpened high-degree count supplies the linear correction in Dross's exact cut inequality.

theorem LeanPool.DrossFractionalTriangleDecomposition.mbound_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) (hδeq : ↑(Fintype.card V) - ↑G.minDegree = δ * ↑(Fintype.card V)) (hδn2 : 2 ≤ δ * ↑(Fintype.card V)) (hnb : ↑{v : V | G.minDegree + 2 ≤ G.degree v}.card ≤ 2 * δ * ↑(Fintype.card V) - 4) : 2 * ↑G.edgeFinset.card ≤ (1 - δ + 2 * δ ^ 2) * ↑(Fintype.card V) ^ 2 + 4 + ↑(Fintype.card V) - 6 * δ * ↑(Fintype.card V)