# mathlib3documentation

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) (whose card is multiplicative_energy s t) as a standalone definition.

def finset.additive_energy {α : Type u_1} [decidable_eq α] [has_add α] (s 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 such that a₁ + b₁ = a₂ + b₂.

Equations
def finset.multiplicative_energy {α : Type u_1} [decidable_eq α] [has_mul α] (s 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 such that a₁ * b₁ = a₂ * b₂.

Equations
theorem finset.multiplicative_energy_mono {α : Type u_1} [decidable_eq α] [has_mul α] {s₁ s₂ t₁ t₂ : finset α} (hs : s₁ s₂) (ht : t₁ t₂) :
theorem finset.additive_energy_mono {α : Type u_1} [decidable_eq α] [has_add α] {s₁ s₂ t₁ t₂ : finset α} (hs : s₁ s₂) (ht : t₁ t₂) :
theorem finset.additive_energy_mono_left {α : Type u_1} [decidable_eq α] [has_add α] {s₁ s₂ t : finset α} (hs : s₁ s₂) :
theorem finset.multiplicative_energy_mono_left {α : Type u_1} [decidable_eq α] [has_mul α] {s₁ s₂ t : finset α} (hs : s₁ s₂) :
theorem finset.multiplicative_energy_mono_right {α : Type u_1} [decidable_eq α] [has_mul α] {s t₁ t₂ : finset α} (ht : t₁ t₂) :
theorem finset.additive_energy_mono_right {α : Type u_1} [decidable_eq α] [has_add α] {s t₁ t₂ : finset α} (ht : t₁ t₂) :
theorem finset.le_multiplicative_energy {α : Type u_1} [decidable_eq α] [has_mul α] {s t : finset α} :
s.card * t.card
theorem finset.le_additive_energy {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} :
s.card * t.card
theorem finset.additive_energy_pos {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} (hs : s.nonempty) (ht : t.nonempty) :
0 <
theorem finset.multiplicative_energy_pos {α : Type u_1} [decidable_eq α] [has_mul α] {s t : finset α} (hs : s.nonempty) (ht : t.nonempty) :
@[simp]
theorem finset.additive_energy_empty_left {α : Type u_1} [decidable_eq α] [has_add α] (t : finset α) :
@[simp]
theorem finset.multiplicative_energy_empty_left {α : Type u_1} [decidable_eq α] [has_mul α] (t : finset α) :
@[simp]
theorem finset.additive_energy_empty_right {α : Type u_1} [decidable_eq α] [has_add α] (s : finset α) :
@[simp]
theorem finset.multiplicative_energy_empty_right {α : Type u_1} [decidable_eq α] [has_mul α] (s : finset α) :
@[simp]
theorem finset.additive_energy_pos_iff {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} :
0 <
@[simp]
theorem finset.multiplicative_energy_pos_iff {α : Type u_1} [decidable_eq α] [has_mul α] {s t : finset α} :
@[simp]
theorem finset.multiplicative_energy_eq_zero_iff {α : Type u_1} [decidable_eq α] [has_mul α] {s t : finset α} :
s = t =
@[simp]
theorem finset.additive_energy_eq_zero_iff {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} :
= 0 s = t =
theorem finset.additive_energy_comm {α : Type u_1} [decidable_eq α] (s t : finset α) :
=
theorem finset.multiplicative_energy_comm {α : Type u_1} [decidable_eq α] [comm_monoid α] (s t : finset α) :
@[simp]
theorem finset.multiplicative_energy_univ_left {α : Type u_1} [decidable_eq α] [comm_group α] [fintype α] (t : finset α) :
@[simp]
theorem finset.additive_energy_univ_left {α : Type u_1} [decidable_eq α] [fintype α] (t : finset α) :
= * t.card ^ 2
@[simp]
theorem finset.multiplicative_energy_univ_right {α : Type u_1} [decidable_eq α] [comm_group α] [fintype α] (s : finset α) :
@[simp]
theorem finset.additive_energy_univ_right {α : Type u_1} [decidable_eq α] [fintype α] (s : finset α) :
= * s.card ^ 2