[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ 0 ≤ energy P G
[PROOFSTEP]
refine' div_nonneg (Finset.sum_nonneg fun _ _ => sq_nonneg _) <| sq_nonneg _
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(card (offDiag P.parts)) ≤ 1 * ↑(card P.parts) ^ 2
[PROOFSTEP]
rw [offDiag_card, one_mul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(card P.parts * card P.parts - card P.parts) ≤ ↑(card P.parts) ^ 2
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ card P.parts * card P.parts - card P.parts ≤ card P.parts ^ 2
[PROOFSTEP]
rw [sq]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ card P.parts * card P.parts - card P.parts ≤ card P.parts * card P.parts
[PROOFSTEP]
exact tsub_le_self
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
𝕜 : Type u_2
inst✝ : LinearOrderedField 𝕜
⊢ ↑(energy P G) = (∑ uv in offDiag P.parts, ↑(SimpleGraph.edgeDensity G uv.fst uv.snd) ^ 2) / ↑(card P.parts) ^ 2
[PROOFSTEP]
rw [energy]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
𝕜 : Type u_2
inst✝ : LinearOrderedField 𝕜
⊢ ↑((∑ uv in offDiag P.parts, SimpleGraph.edgeDensity G uv.fst uv.snd ^ 2) / ↑(card P.parts) ^ 2) =
    (∑ uv in offDiag P.parts, ↑(SimpleGraph.edgeDensity G uv.fst uv.snd) ^ 2) / ↑(card P.parts) ^ 2
[PROOFSTEP]
norm_cast
