English
Let P be a partition of a finite subset s of α in a simple graph G on α. The energy of P with respect to G is the average, over all ordered pairs of distinct parts of P, of the squared edge density between those parts.
Русский
Пусть P — разбиение конечного подмножества s множества α графа G на α. Энергия P по отношению к G равна среднему значению по всем упорядоченным парам различных частей P квадрата плотности ребер между этими частями.
LaTeX
$$$E(P,G) = \\dfrac{\\displaystyle \\sum_{uv \\in P.parts.offDiag} \\bigl(G.edgeDensity(u,v)\\bigr)^2}{\\left(\\lvert P.parts\\rvert\\right)^2}$$$
Lean4
/-- The energy of a partition, also known as index. Auxiliary quantity for Szemerédi's regularity
lemma. -/
def energy : ℚ :=
((∑ uv ∈ P.parts.offDiag, G.edgeDensity uv.1 uv.2 ^ 2) : ℚ) / (#P.parts : ℚ) ^ 2
