English
Let α be a type with a multiplicative operation. For finite subsets s, t, u of α, define the multiplicative energy E_m[s,t] = sum over c in u of (number of representations of c as x y with x in s and y in t) squared. Then the square of the number of pairs (x,y) in s × t with x y ∈ u is at most |u| times E_m[s,t].
Русский
Пусть α — множество с умножением. Для конечных подмножеств s, t, u ⊆ α определим мультипликативную энергию E_m[s,t] = ∑_{c∈u} (число представлений c в виде x y, где x∈s, y∈t)^2. Тогда квадрат числа пар (x,y) ∈ s × t с x y ∈ u не превосходит |u| умноженное на E_m[s,t].
LaTeX
$$$\\#\\{(x,y) \\in s \\times t \\mid x y \\in u\\}^2 \\le \\#u \\cdot E_m[s,t]$$$
Lean4
@[to_additive card_sq_le_card_mul_addEnergy]
theorem card_sq_le_card_mul_mulEnergy (s t u : Finset α) : #({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u}) ^ 2 ≤ #u * Eₘ[s, t] := by
calc
_ = (∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) ^ 2 := by rw [← sum_card_fiberwise_eq_card_filter]
_ ≤ #u * ∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2 := by simpa using sum_mul_sq_le_sq_mul_sq (R := ℕ) _ 1 _
_ ≤ #u * ∑ c ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2 :=
by
refine mul_le_mul_left' (sum_le_sum_of_ne_zero ?_) _
aesop (add simp [filter_eq_empty_iff]) (add unsafe mul_mem_mul)
_ = #u * Eₘ[s, t] := by rw [mulEnergy_eq_sum_sq']
