mathlib3 documentation

combinatorics.additive.energy

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.

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₂) :
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₂) :
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_additive_energy {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} :
theorem finset.additive_energy_pos {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} (hs : s.nonempty) (ht : t.nonempty) :
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]
@[simp]
theorem finset.additive_energy_pos_iff {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} :
@[simp]
@[simp]
theorem finset.additive_energy_eq_zero_iff {α : Type u_1} [decidable_eq α] [has_add α] {s t : finset α} :