English
For finite type α, E_m[s,t] equals the sum over all a in univ of the square of the number of representations of a as a product a1 b1 with a1 ∈ s, b1 ∈ t.
Русский
Для конечного типа α энергия E_m[s,t] равна сумме по всем a из универсума квадрата числа представлений a как произведения a1 b1 с a1 ∈ s, b1 ∈ t.
LaTeX
$$$ E_m[s,t] = \\sum_{a \\in \\mathrm{univ}} \\Big(\\#\\{xy ∈ s × t \\mid xy.1 \\cdot xy.2 = a\\}\\Big)^2 $$$
Lean4
@[to_additive]
theorem mulEnergy_eq_sum_sq [Fintype α] (s t : Finset α) : Eₘ[s, t] = ∑ a, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = a}) ^ 2 :=
by
rw [mulEnergy_eq_sum_sq']
exact Fintype.sum_subset <| by aesop (add simp [filter_eq_empty_iff, mul_mem_mul])