Elementary dense-graph cases

Uniform triangle counts yield a fractional decomposition by constant weights. The minimum-degree assumption also ensures every edge belongs to a triangle.

theorem LeanPool.DrossFractionalTriangleDecomposition.fractional_of_constant_triThrough {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (T : ℕ) (hT : 0 < T) (hconst : ∀ e ∈ G.edgeFinset, triThrough G e = T) : FractionalTriangleDecomp G

If all edges lie in exactly the same positive number of triangles, the constant reciprocal weight is a fractional triangle decomposition.

theorem LeanPool.DrossFractionalTriangleDecomposition.exists_triangle_of_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (h : 9 * Fintype.card V ≤ 10 * G.minDegree) (hm : G.edgeFinset.Nonempty) : 0 < (G.cliqueFinset 3).card

Under the nine-tenths minimum-degree hypothesis, every nonempty graph contains a triangle.