Additive energy #
This file defines the additive energy of two finsets of a group. This is a central quantity in additive combinatorics.
TODO #
It's possibly interesting to have
(s ×ˢ s) ×ᶠ t ×ᶠ t).filter (λ x : (α × α) × α × α, x.1.1 * x.2.1 = x.1.2 * x.2.2)×ˢ s) ×ᶠ t ×ᶠ t).filter (λ x : (α × α) × α × α, x.1.1 * x.2.1 = x.1.2 * x.2.2)×ᶠ t ×ᶠ t).filter (λ x : (α × α) × α × α, x.1.1 * x.2.1 = x.1.2 * x.2.2)×ᶠ t).filter (λ x : (α × α) × α × α, x.1.1 * x.2.1 = x.1.2 * x.2.2)× α) × α × α, x.1.1 * x.2.1 = x.1.2 * x.2.2)× α × α, x.1.1 * x.2.1 = x.1.2 * x.2.2)× α, x.1.1 * x.2.1 = x.1.2 * x.2.2)
(whose card
is
multiplicativeEnergy s t
) as a standalone definition.
The additive energy of two finsets s
and t
in a group is the
number of quadruples (a₁, a₂, b₁, b₂) ∈ s × s × t × t∈ s × s × t × t× s × t × t× t × t× t
such that a₁ + b₁ = a₂ + b₂
.
Equations
- Finset.additiveEnergy s t = Finset.card (Finset.filter (fun x => x.fst.fst + x.snd.fst = x.fst.snd + x.snd.snd) ((s ×ᶠ s) ×ᶠ t ×ᶠ t))
The multiplicative energy of two finsets s
and t
in a group is the number of quadruples
(a₁, a₂, b₁, b₂) ∈ s × s × t × t∈ s × s × t × t× s × t × t× t × t× t
such that a₁ * b₁ = a₂ * b₂
.
Equations
- Finset.multiplicativeEnergy s t = Finset.card (Finset.filter (fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) ((s ×ᶠ s) ×ᶠ t ×ᶠ t))