mulEnergy_eq_sum_sq' — Mathlib

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)

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