Documentation

Mathlib.Combinatorics.Additive.Energy

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
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
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₂) :
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₂) :
theorem Finset.additiveEnergy_mono_left {α : Type u_1} [inst : DecidableEq α] [inst : Add α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} (hs : s₁ s₂) :
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₂) :
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 α} :
theorem Finset.additiveEnergy_pos {α : Type u_1} [inst : DecidableEq α] [inst : Add α] {s : Finset α} {t : Finset α} (hs : Finset.Nonempty s) (ht : Finset.Nonempty t) :
theorem Finset.multiplicativeEnergy_pos {α : Type u_1} [inst : DecidableEq α] [inst : Mul α] {s : Finset α} {t : Finset α} (hs : Finset.Nonempty s) (ht : Finset.Nonempty t) :
@[simp]
theorem Finset.additiveEnergy_empty_left {α : Type u_1} [inst : DecidableEq α] [inst : Add α] (t : Finset α) :
@[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 α) :
@[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 α} :
@[simp]
theorem Finset.additive_energy_eq_zero_iff {α : Type u_1} [inst : DecidableEq α] [inst : Add α] {s : Finset α} {t : Finset α} :
@[simp]
theorem Finset.multiplicativeEnergy_eq_zero_iff {α : Type u_1} [inst : DecidableEq α] [inst : Mul α] {s : Finset α} {t : Finset α} :
@[simp]
theorem Finset.additiveEnergy_univ_left {α : Type u_1} [inst : DecidableEq α] [inst : AddCommGroup α] [inst : Fintype α] (t : Finset α) :
@[simp]
theorem Finset.multiplicativeEnergy_univ_left {α : Type u_1} [inst : DecidableEq α] [inst : CommGroup α] [inst : Fintype α] (t : Finset α) :
@[simp]
theorem Finset.additiveEnergy_univ_right {α : Type u_1} [inst : DecidableEq α] [inst : AddCommGroup α] [inst : Fintype α] (s : Finset α) :
@[simp]
theorem Finset.multiplicativeEnergy_univ_right {α : Type u_1} [inst : DecidableEq α] [inst : CommGroup α] [inst : Fintype α] (s : Finset α) :