Dross's theorem without a high-degree triangle #
The small and complete cases are elementary. Otherwise the exact high-degree and edge-count estimates imply the cut hypothesis, so the saturating flow gives the desired fractional triangle decomposition.
theorem
LeanPool.DrossFractionalTriangleDecomposition.dross_fractional_flow_noHDT_exact
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(h : 9 * Fintype.card V ≤ 10 * 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)
:
Exact Dross decomposition when no triangle has all three vertices of
degree at least minDegree + 2.