English
The multiplicative energy Eₘ[s,t] of two finite sets s and t in a group counts quadruples (a1, a2, b1, b2) in s × s × t × t such that a1 b1 = a2 b2.
Русский
Умножительная энергия Eₘ[s,t] двух конечных множеств s и t в группе равна числу четверок (a1, a2, b1, b2) из s × s × t × t, удовлетворяющих a1 b1 = a2 b2.
LaTeX
$$$ E_m[s,t] = \\#\\{(a_1,a_2,b_1,b_2) \\in s \\times s \\times t \\times t \\mid a_1 b_1 = a_2 b_2\\} $$$
Lean4
/-- The multiplicative energy `Eₘ[s, t]` of two finsets `s` and `t` in a group is the number of
quadruples `(a₁, a₂, b₁, b₂) ∈ s × s × t × t` such that `a₁ * b₁ = a₂ * b₂`.
The notation `Eₘ[s, t]` is available in scope `Combinatorics.Additive`. -/
@[to_additive /-- The additive energy `E[s, t]` of two finsets `s` and `t` in a group is the number of quadruples
`(a₁, a₂, b₁, b₂) ∈ s × s × t × t` such that `a₁ + b₁ = a₂ + b₂`.
The notation `E[s, t]` is available in scope `Combinatorics.Additive`. -/
]
def mulEnergy (s t : Finset α) : ℕ :=
#({x ∈ ((s ×ˢ s) ×ˢ t ×ˢ t) | x.1.1 * x.2.1 = x.1.2 * x.2.2})
