∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) (G : SimpleGraph α)
  [inst_1 : DecidableRel G.Adj], P.energy G = (∑ uv ∈ P.parts.offDiag, G.edgeDensity uv.1 uv.2 ^ 2) / ↑P.parts.card ^ 2