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.
def
Finset.additiveEnergy
{α : Type u_1}
[inst : DecidableEq α]
[inst : Add α]
(s : Finset α)
(t : Finset α)
:
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))
def
Finset.multiplicativeEnergy
{α : Type u_1}
[inst : DecidableEq α]
[inst : Mul α]
(s : Finset α)
(t : Finset α)
:
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))
theorem
Finset.additiveEnergy_mono
{α : Type u_1}
[inst : DecidableEq α]
[inst : Add α]
{s₁ : Finset α}
{s₂ : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
(hs : s₁ ⊆ s₂)
(ht : t₁ ⊆ t₂)
:
Finset.additiveEnergy s₁ t₁ ≤ Finset.additiveEnergy s₂ t₂
theorem
Finset.multiplicativeEnergy_mono
{α : Type u_1}
[inst : DecidableEq α]
[inst : Mul α]
{s₁ : Finset α}
{s₂ : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
(hs : s₁ ⊆ s₂)
(ht : t₁ ⊆ t₂)
:
Finset.multiplicativeEnergy s₁ t₁ ≤ Finset.multiplicativeEnergy s₂ t₂
theorem
Finset.additiveEnergy_mono_left
{α : Type u_1}
[inst : DecidableEq α]
[inst : Add α]
{s₁ : Finset α}
{s₂ : Finset α}
{t : Finset α}
(hs : s₁ ⊆ s₂)
:
Finset.additiveEnergy s₁ t ≤ Finset.additiveEnergy s₂ t
theorem
Finset.multiplicativeEnergy_mono_left
{α : Type u_1}
[inst : DecidableEq α]
[inst : Mul α]
{s₁ : Finset α}
{s₂ : Finset α}
{t : Finset α}
(hs : s₁ ⊆ s₂)
:
theorem
Finset.additiveEnergy_mono_right
{α : Type u_1}
[inst : DecidableEq α]
[inst : Add α]
{s : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
(ht : t₁ ⊆ t₂)
:
Finset.additiveEnergy s t₁ ≤ Finset.additiveEnergy s t₂
theorem
Finset.multiplicativeEnergy_mono_right
{α : Type u_1}
[inst : DecidableEq α]
[inst : Mul α]
{s : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
(ht : t₁ ⊆ t₂)
:
theorem
Finset.le_additiveEnergy
{α : Type u_1}
[inst : DecidableEq α]
[inst : Add α]
{s : Finset α}
{t : Finset α}
:
Finset.card s * Finset.card t ≤ Finset.additiveEnergy s t
theorem
Finset.le_multiplicativeEnergy
{α : Type u_1}
[inst : DecidableEq α]
[inst : Mul α]
{s : Finset α}
{t : Finset α}
:
theorem
Finset.additiveEnergy_pos
{α : Type u_1}
[inst : DecidableEq α]
[inst : Add α]
{s : Finset α}
{t : Finset α}
(hs : Finset.Nonempty s)
(ht : Finset.Nonempty t)
:
0 < Finset.additiveEnergy s t
theorem
Finset.multiplicativeEnergy_pos
{α : Type u_1}
[inst : DecidableEq α]
[inst : Mul α]
{s : Finset α}
{t : Finset α}
(hs : Finset.Nonempty s)
(ht : Finset.Nonempty t)
:
0 < Finset.multiplicativeEnergy s t
@[simp]
theorem
Finset.additiveEnergy_empty_left
{α : Type u_1}
[inst : DecidableEq α]
[inst : Add α]
(t : Finset α)
:
Finset.additiveEnergy ∅ t = 0
@[simp]
theorem
Finset.multiplicativeEnergy_empty_left
{α : Type u_1}
[inst : DecidableEq α]
[inst : Mul α]
(t : Finset α)
:
@[simp]
theorem
Finset.additiveEnergy_empty_right
{α : Type u_1}
[inst : DecidableEq α]
[inst : Add α]
(s : Finset α)
:
Finset.additiveEnergy s ∅ = 0
@[simp]
theorem
Finset.multiplicativeEnergy_empty_right
{α : Type u_1}
[inst : DecidableEq α]
[inst : Mul α]
(s : Finset α)
:
@[simp]
theorem
Finset.additiveEnergy_pos_iff
{α : Type u_1}
[inst : DecidableEq α]
[inst : Add α]
{s : Finset α}
{t : Finset α}
:
0 < Finset.additiveEnergy s t ↔ Finset.Nonempty s ∧ Finset.Nonempty t
@[simp]
theorem
Finset.multiplicativeEnergy_pos_iff
{α : Type u_1}
[inst : DecidableEq α]
[inst : Mul α]
{s : Finset α}
{t : Finset α}
:
0 < Finset.multiplicativeEnergy s t ↔ Finset.Nonempty s ∧ Finset.Nonempty t
theorem
Finset.additiveEnergy_comm
{α : Type u_1}
[inst : DecidableEq α]
[inst : AddCommMonoid α]
(s : Finset α)
(t : Finset α)
:
theorem
Finset.multiplicativeEnergy_comm
{α : Type u_1}
[inst : DecidableEq α]
[inst : CommMonoid α]
(s : Finset α)
(t : Finset α)
:
@[simp]
theorem
Finset.additiveEnergy_univ_left
{α : Type u_1}
[inst : DecidableEq α]
[inst : AddCommGroup α]
[inst : Fintype α]
(t : Finset α)
:
Finset.additiveEnergy Finset.univ t = Fintype.card α * Finset.card t ^ 2
@[simp]
theorem
Finset.multiplicativeEnergy_univ_left
{α : Type u_1}
[inst : DecidableEq α]
[inst : CommGroup α]
[inst : Fintype α]
(t : Finset α)
:
Finset.multiplicativeEnergy Finset.univ t = Fintype.card α * Finset.card t ^ 2
@[simp]
theorem
Finset.additiveEnergy_univ_right
{α : Type u_1}
[inst : DecidableEq α]
[inst : AddCommGroup α]
[inst : Fintype α]
(s : Finset α)
:
Finset.additiveEnergy s Finset.univ = Fintype.card α * Finset.card s ^ 2
@[simp]
theorem
Finset.multiplicativeEnergy_univ_right
{α : Type u_1}
[inst : DecidableEq α]
[inst : CommGroup α]
[inst : Fintype α]
(s : Finset α)
:
Finset.multiplicativeEnergy s Finset.univ = Fintype.card α * Finset.card s ^ 2