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 (fun x : (α × α) × α × α ↦ 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} [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₂.

Equations

• Finset.additiveEnergy s t = (Finset.filter (fun (x : (α × α) × α × α) => x.1.1 + x.2.1 = x.1.2 + x.2.2) ((s ×ˢ s) ×ˢ t ×ˢ t)).card

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₂.

Equations

• Finset.multiplicativeEnergy s t = (Finset.filter (fun (x : (α × α) × α × α) => x.1.1 * x.2.1 = x.1.2 * x.2.2) ((s ×ˢ s) ×ˢ t ×ˢ t)).card

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₂

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₂

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

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

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₂

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₂

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Finset.additiveEnergy_pos_iff {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : 0 < Finset.additiveEnergy s t ↔ s.Nonempty ∧ t.Nonempty

@[simp]

theorem Finset.multiplicativeEnergy_pos_iff {α : Type u_1} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : 0 < Finset.multiplicativeEnergy s t ↔ s.Nonempty ∧ t.Nonempty

@[simp]

theorem Finset.additive_energy_eq_zero_iff {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} : Finset.additiveEnergy s t = 0 ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Finset.multiplicativeEnergy_eq_zero_iff {α : Type u_1} [DecidableEq α] [Mul α] {s : Finset α} {t : Finset α} : Finset.multiplicativeEnergy s t = 0 ↔ s = ∅ ∨ t = ∅

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

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

@[simp]

theorem Finset.additiveEnergy_univ_left {α : Type u_1} [DecidableEq α] [AddCommGroup α] [Fintype α] (t : Finset α) : Finset.additiveEnergy Finset.univ t = Fintype.card α * t.card ^ 2

@[simp]

theorem Finset.multiplicativeEnergy_univ_left {α : Type u_1} [DecidableEq α] [CommGroup α] [Fintype α] (t : Finset α) : Finset.multiplicativeEnergy Finset.univ t = Fintype.card α * t.card ^ 2

@[simp]

theorem Finset.additiveEnergy_univ_right {α : Type u_1} [DecidableEq α] [AddCommGroup α] [Fintype α] (s : Finset α) : Finset.additiveEnergy s Finset.univ = Fintype.card α * s.card ^ 2

@[simp]

theorem Finset.multiplicativeEnergy_univ_right {α : Type u_1} [DecidableEq α] [CommGroup α] [Fintype α] (s : Finset α) : Finset.multiplicativeEnergy s Finset.univ = Fintype.card α * s.card ^ 2