English
E_m[s,t] equals the sum over a in s×t of the square of the number of representations of a as a product a1 b1 with a1,b1 ∈ s,t respectively.
Русский
E_m[s,t] равно сумме по a ∈ s×t квадратов числа представлений a как произведения a1 b1 с a1 ∈ s, b1 ∈ t.
LaTeX
$$$ E_m[s,t] = \\sum_{a \\in s \\times t} \\Big(\\#\\{xy ∈ s \\times t \\mid xy.1 \\cdot xy.2 = a\\}\\Big)^2 $$$
Lean4
@[to_additive]
theorem mulEnergy_eq_sum_sq' (s t : Finset α) : Eₘ[s, t] = ∑ a ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = a}) ^ 2 :=
by
simp_rw [mulEnergy_eq_card_filter, sq, ← card_product]
rw [← card_disjiUnion]
swap
· aesop (add simp [Set.PairwiseDisjoint, Set.Pairwise, disjoint_left])
· congr
aesop (add unsafe mul_mem_mul)