Triangle weights reconstructed from Dross's flow

Each rooted K₄ transfer adjusts the common initial triangle weight. Subsequent lemmas show that the weights are nonnegative and cover every graph edge.

noncomputable def LeanPool.DrossFractionalTriangleDecomposition.triWeight {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (F : Contrib.MaxFlowMinCut.Flow (drossNet G wΔ)) (t : Finset V) : ℝ

The weight of a triangle after all rooted-K₄ transfers in the auxiliary flow.

Equations

• One or more equations did not get rendered due to their size.