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

source

def Finset.additiveEnergy {α : Type u_1} [DecidableEq α] [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 such that a₁ + b₁ = a₂ + b₂.

Instances For

source

def Finset.multiplicativeEnergy {α : Type u_1} [DecidableEq α] [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 such that a₁ * b₁ = a₂ * b₂.

Instances For

source

theorem Finset.additiveEnergy_mono {α : Type u_1} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :

Finset.additiveEnergy s₁ t₁ ≤ Finset.additiveEnergy s₂ t₂

source

theorem Finset.multiplicativeEnergy_mono {α : Type u_1} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :

Finset.multiplicativeEnergy s₁ t₁ ≤ Finset.multiplicativeEnergy s₂ t₂

source

theorem Finset.additiveEnergy_mono_left {α : Type u_1} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} (hs : s₁ ⊆ s₂) :

Finset.additiveEnergy s₁ t ≤ Finset.additiveEnergy s₂ t

source

theorem Finset.multiplicativeEnergy_mono_left {α : Type u_1} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} (hs : s₁ ⊆ s₂) :

Finset.multiplicativeEnergy s₁ t ≤ Finset.multiplicativeEnergy s₂ t

source

theorem Finset.additiveEnergy_mono_right {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} (ht : t₁ ⊆ t₂) :

Finset.additiveEnergy s t₁ ≤ Finset.additiveEnergy s t₂

source

theorem Finset.multiplicativeEnergy_mono_right {α : Type u_1} [DecidableEq α] [Mul α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} (ht : t₁ ⊆ t₂) :

Finset.multiplicativeEnergy s t₁ ≤ Finset.multiplicativeEnergy s t₂

source

theorem Finset.le_additiveEnergy {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} :

Finset.card s * Finset.card t ≤ Finset.additiveEnergy s t

source

theorem Finset.le_multiplicativeEnergy {α : Type u_1} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} :

Finset.card s * Finset.card t ≤ Finset.multiplicativeEnergy s t

source

theorem Finset.additiveEnergy_pos {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} (hs : Finset.Nonempty s) (ht : Finset.Nonempty t) :

0 < Finset.additiveEnergy s t

source

theorem Finset.multiplicativeEnergy_pos {α : Type u_1} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} (hs : Finset.Nonempty s) (ht : Finset.Nonempty t) :

0 < Finset.multiplicativeEnergy s t

source

@[simp]

theorem Finset.additiveEnergy_empty_left {α : Type u_1} [DecidableEq α] [Add α] (t : Finset α) :

Finset.additiveEnergy ∅ t = 0

source

@[simp]

theorem Finset.multiplicativeEnergy_empty_left {α : Type u_1} [DecidableEq α] [Mul α] (t : Finset α) :

Finset.multiplicativeEnergy ∅ t = 0

source

@[simp]

theorem Finset.additiveEnergy_empty_right {α : Type u_1} [DecidableEq α] [Add α] (s : Finset α) :

Finset.additiveEnergy s ∅ = 0

source

@[simp]

theorem Finset.multiplicativeEnergy_empty_right {α : Type u_1} [DecidableEq α] [Mul α] (s : Finset α) :

Finset.multiplicativeEnergy s ∅ = 0

source

@[simp]

theorem Finset.additiveEnergy_pos_iff {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} :

0 < Finset.additiveEnergy s t ↔ Finset.Nonempty s ∧ Finset.Nonempty t

source

@[simp]

theorem Finset.multiplicativeEnergy_pos_iff {α : Type u_1} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} :

0 < Finset.multiplicativeEnergy s t ↔ Finset.Nonempty s ∧ Finset.Nonempty t

source

@[simp]

theorem Finset.additive_energy_eq_zero_iff {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} :

Finset.additiveEnergy s t = 0 ↔ s = ∅ ∨ t = ∅

source

@[simp]

theorem Finset.multiplicativeEnergy_eq_zero_iff {α : Type u_1} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} :

Finset.multiplicativeEnergy s t = 0 ↔ s = ∅ ∨ t = ∅

source

theorem Finset.additiveEnergy_comm {α : Type u_1} [DecidableEq α] [AddCommMonoid α] (s : Finset α) (t : Finset α) :

Finset.additiveEnergy s t = Finset.additiveEnergy t s

source

theorem Finset.multiplicativeEnergy_comm {α : Type u_1} [DecidableEq α] [CommMonoid α] (s : Finset α) (t : Finset α) :

Finset.multiplicativeEnergy s t = Finset.multiplicativeEnergy t s

source

@[simp]

theorem Finset.additiveEnergy_univ_left {α : Type u_1} [DecidableEq α] [AddCommGroup α] [Fintype α] (t : Finset α) :

Finset.additiveEnergy Finset.univ t = Fintype.card α * Finset.card t ^ 2

source

@[simp]

theorem Finset.multiplicativeEnergy_univ_left {α : Type u_1} [DecidableEq α] [CommGroup α] [Fintype α] (t : Finset α) :

Finset.multiplicativeEnergy Finset.univ t = Fintype.card α * Finset.card t ^ 2

source

@[simp]

theorem Finset.additiveEnergy_univ_right {α : Type u_1} [DecidableEq α] [AddCommGroup α] [Fintype α] (s : Finset α) :

Finset.additiveEnergy s Finset.univ = Fintype.card α * Finset.card s ^ 2

source

@[simp]

theorem Finset.multiplicativeEnergy_univ_right {α : Type u_1} [DecidableEq α] [CommGroup α] [Fintype α] (s : Finset α) :

Finset.multiplicativeEnergy s Finset.univ = Fintype.card α * Finset.card s ^ 2