# Documentation

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 : ] [inst : Add α] (s : ) (t : ) :

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
def Finset.multiplicativeEnergy {α : Type u_1} [inst : ] [inst : Mul α] (s : ) (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
theorem Finset.additiveEnergy_mono {α : Type u_1} [inst : ] [inst : Add α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
theorem Finset.multiplicativeEnergy_mono {α : Type u_1} [inst : ] [inst : Mul α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
theorem Finset.additiveEnergy_mono_left {α : Type u_1} [inst : ] [inst : Add α] {s₁ : } {s₂ : } {t : } (hs : s₁ s₂) :
theorem Finset.multiplicativeEnergy_mono_left {α : Type u_1} [inst : ] [inst : Mul α] {s₁ : } {s₂ : } {t : } (hs : s₁ s₂) :
theorem Finset.additiveEnergy_mono_right {α : Type u_1} [inst : ] [inst : Add α] {s : } {t₁ : } {t₂ : } (ht : t₁ t₂) :
theorem Finset.multiplicativeEnergy_mono_right {α : Type u_1} [inst : ] [inst : Mul α] {s : } {t₁ : } {t₂ : } (ht : t₁ t₂) :
theorem Finset.le_additiveEnergy {α : Type u_1} [inst : ] [inst : Add α] {s : } {t : } :
theorem Finset.le_multiplicativeEnergy {α : Type u_1} [inst : ] [inst : Mul α] {s : } {t : } :
theorem Finset.additiveEnergy_pos {α : Type u_1} [inst : ] [inst : Add α] {s : } {t : } (hs : ) (ht : ) :
theorem Finset.multiplicativeEnergy_pos {α : Type u_1} [inst : ] [inst : Mul α] {s : } {t : } (hs : ) (ht : ) :
@[simp]
theorem Finset.additiveEnergy_empty_left {α : Type u_1} [inst : ] [inst : Add α] (t : ) :
@[simp]
theorem Finset.multiplicativeEnergy_empty_left {α : Type u_1} [inst : ] [inst : Mul α] (t : ) :
@[simp]
theorem Finset.additiveEnergy_empty_right {α : Type u_1} [inst : ] [inst : Add α] (s : ) :
@[simp]
theorem Finset.multiplicativeEnergy_empty_right {α : Type u_1} [inst : ] [inst : Mul α] (s : ) :
@[simp]
theorem Finset.additiveEnergy_pos_iff {α : Type u_1} [inst : ] [inst : Add α] {s : } {t : } :
@[simp]
theorem Finset.multiplicativeEnergy_pos_iff {α : Type u_1} [inst : ] [inst : Mul α] {s : } {t : } :
@[simp]
theorem Finset.additive_energy_eq_zero_iff {α : Type u_1} [inst : ] [inst : Add α] {s : } {t : } :
s = t =
@[simp]
theorem Finset.multiplicativeEnergy_eq_zero_iff {α : Type u_1} [inst : ] [inst : Mul α] {s : } {t : } :
s = t =
theorem Finset.additiveEnergy_comm {α : Type u_1} [inst : ] [inst : ] (s : ) (t : ) :
theorem Finset.multiplicativeEnergy_comm {α : Type u_1} [inst : ] [inst : ] (s : ) (t : ) :
@[simp]
theorem Finset.additiveEnergy_univ_left {α : Type u_1} [inst : ] [inst : ] [inst : ] (t : ) :
Finset.additiveEnergy Finset.univ t = * ^ 2
@[simp]
theorem Finset.multiplicativeEnergy_univ_left {α : Type u_1} [inst : ] [inst : ] [inst : ] (t : ) :
@[simp]
theorem Finset.additiveEnergy_univ_right {α : Type u_1} [inst : ] [inst : ] [inst : ] (s : ) :
Finset.additiveEnergy s Finset.univ = * ^ 2
@[simp]
theorem Finset.multiplicativeEnergy_univ_right {α : Type u_1} [inst : ] [inst : ] [inst : ] (s : ) :