The complete-graph case

Maximum possible minimum degree makes the graph complete. Each edge then has exactly n - 2 common neighbours, so constant triangle weights suffice.

theorem LeanPool.DrossFractionalTriangleDecomposition.degree_le_card_sub_one {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (u : V) : G.degree u ≤ Fintype.card V - 1

Every vertex degree is at most one less than the order of the graph.

theorem LeanPool.DrossFractionalTriangleDecomposition.adj_of_minDegree_eq_card_sub_one {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hmin : G.minDegree = Fintype.card V - 1) {u v : V} (huv : u ≠ v) : G.Adj u v

Maximum minimum degree forces all distinct vertices to be adjacent.

theorem LeanPool.DrossFractionalTriangleDecomposition.triThrough_of_minDegree_eq_card_sub_one {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableEq V] [DecidableRel G.Adj] (hmin : G.minDegree = Fintype.card V - 1) {e : Sym2 V} (he : e ∈ G.edgeFinset) : triThrough G e = Fintype.card V - 2

In the complete case, an edge belongs to precisely n - 2 triangles.

theorem LeanPool.DrossFractionalTriangleDecomposition.complete_fractional {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableEq V] [DecidableRel G.Adj] (hmin : G.minDegree = Fintype.card V - 1) (hcard : 3 ≤ Fintype.card V) : FractionalTriangleDecomp G

A graph with the maximum possible minimum degree has a fractional triangle decomposition once it has at least three vertices.