Additive energy #
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.
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₂.
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₂.
theorem
finset.multiplicative_energy_mono
{α : Type u_1}
[decidable_eq α]
[has_mul α]
{s₁ s₂ t₁ t₂ : finset α}
(hs : s₁ ⊆ s₂)
(ht : t₁ ⊆ t₂) :
s₁.multiplicative_energy t₁ ≤ s₂.multiplicative_energy t₂
theorem
finset.additive_energy_mono
{α : Type u_1}
[decidable_eq α]
[has_add α]
{s₁ s₂ t₁ t₂ : finset α}
(hs : s₁ ⊆ s₂)
(ht : t₁ ⊆ t₂) :
s₁.additive_energy t₁ ≤ s₂.additive_energy t₂
theorem
finset.additive_energy_mono_left
{α : Type u_1}
[decidable_eq α]
[has_add α]
{s₁ s₂ t : finset α}
(hs : s₁ ⊆ s₂) :
s₁.additive_energy t ≤ s₂.additive_energy t
theorem
finset.multiplicative_energy_mono_left
{α : Type u_1}
[decidable_eq α]
[has_mul α]
{s₁ s₂ t : finset α}
(hs : s₁ ⊆ s₂) :
s₁.multiplicative_energy t ≤ s₂.multiplicative_energy t
theorem
finset.multiplicative_energy_mono_right
{α : Type u_1}
[decidable_eq α]
[has_mul α]
{s t₁ t₂ : finset α}
(ht : t₁ ⊆ t₂) :
s.multiplicative_energy t₁ ≤ s.multiplicative_energy t₂
theorem
finset.additive_energy_mono_right
{α : Type u_1}
[decidable_eq α]
[has_add α]
{s t₁ t₂ : finset α}
(ht : t₁ ⊆ t₂) :
s.additive_energy t₁ ≤ s.additive_energy t₂
theorem
finset.le_multiplicative_energy
{α : Type u_1}
[decidable_eq α]
[has_mul α]
{s t : finset α} :
s.card * t.card ≤ s.multiplicative_energy t
theorem
finset.le_additive_energy
{α : Type u_1}
[decidable_eq α]
[has_add α]
{s t : finset α} :
s.card * t.card ≤ s.additive_energy t
theorem
finset.additive_energy_pos
{α : Type u_1}
[decidable_eq α]
[has_add α]
{s t : finset α}
(hs : s.nonempty)
(ht : t.nonempty) :
0 < s.additive_energy t
theorem
finset.multiplicative_energy_pos
{α : Type u_1}
[decidable_eq α]
[has_mul α]
{s t : finset α}
(hs : s.nonempty)
(ht : t.nonempty) :
0 < s.multiplicative_energy t
@[simp]
theorem
finset.additive_energy_empty_left
{α : Type u_1}
[decidable_eq α]
[has_add α]
(t : finset α) :
∅.additive_energy t = 0
@[simp]
theorem
finset.multiplicative_energy_empty_left
{α : Type u_1}
[decidable_eq α]
[has_mul α]
(t : finset α) :
∅.multiplicative_energy t = 0
@[simp]
theorem
finset.additive_energy_empty_right
{α : Type u_1}
[decidable_eq α]
[has_add α]
(s : finset α) :
s.additive_energy ∅ = 0
@[simp]
theorem
finset.multiplicative_energy_empty_right
{α : Type u_1}
[decidable_eq α]
[has_mul α]
(s : finset α) :
s.multiplicative_energy ∅ = 0
@[simp]
theorem
finset.additive_energy_pos_iff
{α : Type u_1}
[decidable_eq α]
[has_add α]
{s t : finset α} :
@[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 α} :
@[simp]
theorem
finset.additive_energy_eq_zero_iff
{α : Type u_1}
[decidable_eq α]
[has_add α]
{s t : finset α} :
theorem
finset.additive_energy_comm
{α : Type u_1}
[decidable_eq α]
[add_comm_monoid α]
(s t : finset α) :
s.additive_energy t = t.additive_energy s
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 α) :
finset.univ.multiplicative_energy t = fintype.card α * t.card ^ 2
@[simp]
theorem
finset.additive_energy_univ_left
{α : Type u_1}
[decidable_eq α]
[add_comm_group α]
[fintype α]
(t : finset α) :
finset.univ.additive_energy t = fintype.card α * t.card ^ 2
@[simp]
theorem
finset.multiplicative_energy_univ_right
{α : Type u_1}
[decidable_eq α]
[comm_group α]
[fintype α]
(s : finset α) :
s.multiplicative_energy finset.univ = fintype.card α * s.card ^ 2
@[simp]
theorem
finset.additive_energy_univ_right
{α : Type u_1}
[decidable_eq α]
[add_comm_group α]
[fintype α]
(s : finset α) :
s.additive_energy finset.univ = fintype.card α * s.card ^ 2