English
For finite s,t ⊆ α in a multiplicative group, the inequality |s|^2 · |t|^2 ≤ |s t| · E_m[s,t] holds, where s t is the product set and E_m[s,t] is the multiplicative energy.
Русский
Для конечных подмножеств s,t ⊆ α в мультипликативной группе выполняется неравенство |s|^2 · |t|^2 ≤ |s t| · E_m[s,t], где s t — множество произведений и E_m[s,t] — мультипликативная энергия.
LaTeX
$$$|s|^2 \\cdot |t|^2 \\le |s t| \\cdot E_m[s,t]$$$
Lean4
@[to_additive le_card_add_mul_addEnergy]
theorem le_card_mul_mul_mulEnergy (s t : Finset α) : #s ^ 2 * #t ^ 2 ≤ #(s * t) * Eₘ[s, t] :=
calc
_ = #({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ s * t}) ^ 2 := by rw [filter_eq_self.2, card_product, mul_pow];
aesop (add unsafe mul_mem_mul)
_ ≤ #(s * t) * Eₘ[s, t] := card_sq_le_card_mul_mulEnergy _ _ _
