mulEnergy_eq_sum_sq — Mathlib

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])

Похожие утверждения