Additive energy

This file defines the additive energy of two finsets of a group. This is a central quantity in additive combinatorics.

Main declarations

• Finset.addEnergy: The additive energy of two finsets in an additive group.
• Finset.mulEnergy: The multiplicative energy of two finsets in a group.

Notation

The following notations are defined in the Combinatorics.Additive scope:

• E[s, t] for Finset.addEnergy s t.
• Eₘ[s, t] for Finset.mulEnergy s t.
• E[s] for E[s, s].
• Eₘ[s] for Eₘ[s, s].

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 mulEnergy s t) as a standalone definition.

def Finset.mulEnergy {α : Type u_1} [DecidableEq α] [Mul α] (s t : Finset α) : ℕ

The multiplicative energy Eₘ[s, t] 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 notation Eₘ[s, t] is available in scope Combinatorics.Additive.

Equations

• s.mulEnergy t = {x ∈ (s ×ˢ s) ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2}.card

def Finset.addEnergy {α : Type u_1} [DecidableEq α] [Add α] (s t : Finset α) : ℕ

The additive energy E[s, t] 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 notation E[s, t] is available in scope Combinatorics.Additive.

Equations

• s.addEnergy t = {x ∈ (s ×ˢ s) ×ˢ t ×ˢ t | x.1.1 + x.2.1 = x.1.2 + x.2.2}.card

def Combinatorics.Additive.«termEₘ[_,_]» : Lean.ParserDescr

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

• One or more equations did not get rendered due to their size.

def Combinatorics.Additive.«termE[_,_]» : Lean.ParserDescr

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

• One or more equations did not get rendered due to their size.

def Combinatorics.Additive.«termEₘ[_]» : Lean.ParserDescr

The multiplicative energy of a finset s in a group is the number of quadruples (a₁, a₂, b₁, b₂) ∈ s × s × s × s such that a₁ * b₁ = a₂ * b₂.

Equations

• One or more equations did not get rendered due to their size.

def Combinatorics.Additive.«termE[_]» : Lean.ParserDescr

The additive energy of a finset s in a group is the number of quadruples (a₁, a₂, b₁, b₂) ∈ s × s × s × s such that a₁ + b₁ = a₂ + b₂.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

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

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

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

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

theorem Finset.le_mulEnergy_self {α : Type u_1} [DecidableEq α] [Mul α] {s : Finset α} : s.card ^ 2 ≤ s.mulEnergy s

theorem Finset.le_addEnergy_self {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} : s.card ^ 2 ≤ s.addEnergy s

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

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

theorem Finset.mulEnergy_self_pos {α : Type u_1} [DecidableEq α] [Mul α] {s : Finset α} (hs : s.Nonempty) : 0 < s.mulEnergy s

theorem Finset.addEnergy_self_pos {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} (hs : s.Nonempty) : 0 < s.addEnergy s

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Finset.mulEnergy_self_pos_iff {α : Type u_1} [DecidableEq α] [Mul α] {s : Finset α} : 0 < s.mulEnergy s ↔ s.Nonempty

theorem Finset.addEnergy_self_pos_iff {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} : 0 < s.addEnergy s ↔ s.Nonempty

theorem Finset.mulEnergy_self_eq_zero_iff {α : Type u_1} [DecidableEq α] [Mul α] {s : Finset α} : s.mulEnergy s = 0 ↔ s = ∅

theorem Finset.addEnergy_self_eq_zero_iff {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} : s.addEnergy s = 0 ↔ s = ∅

theorem Finset.mulEnergy_eq_card_filter {α : Type u_1} [DecidableEq α] [Mul α] (s t : Finset α) : s.mulEnergy t = {x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}.card

theorem Finset.addEnergy_eq_card_filter {α : Type u_1} [DecidableEq α] [Add α] (s t : Finset α) : s.addEnergy t = {x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 + x.1.2 = x.2.1 + x.2.2}.card

theorem Finset.mulEnergy_eq_sum_sq' {α : Type u_1} [DecidableEq α] [Mul α] (s t : Finset α) : s.mulEnergy t = ∑ a ∈ s * t, {xy ∈ s ×ˢ t | xy.1 * xy.2 = a}.card ^ 2

theorem Finset.addEnergy_eq_sum_sq' {α : Type u_1} [DecidableEq α] [Add α] (s t : Finset α) : s.addEnergy t = ∑ a ∈ s + t, {xy ∈ s ×ˢ t | xy.1 + xy.2 = a}.card ^ 2

theorem Finset.mulEnergy_eq_sum_sq {α : Type u_1} [DecidableEq α] [Mul α] [Fintype α] (s t : Finset α) : s.mulEnergy t = ∑ a : α, {xy ∈ s ×ˢ t | xy.1 * xy.2 = a}.card ^ 2

theorem Finset.addEnergy_eq_sum_sq {α : Type u_1} [DecidableEq α] [Add α] [Fintype α] (s t : Finset α) : s.addEnergy t = ∑ a : α, {xy ∈ s ×ˢ t | xy.1 + xy.2 = a}.card ^ 2

theorem Finset.card_sq_le_card_mul_mulEnergy {α : Type u_1} [DecidableEq α] [Mul α] (s t u : Finset α) : {xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u}.card ^ 2 ≤ u.card * s.mulEnergy t

theorem Finset.card_sq_le_card_mul_addEnergy {α : Type u_1} [DecidableEq α] [Add α] (s t u : Finset α) : {xy ∈ s ×ˢ t | xy.1 + xy.2 ∈ u}.card ^ 2 ≤ u.card * s.addEnergy t

theorem Finset.le_card_mul_mul_mulEnergy {α : Type u_1} [DecidableEq α] [Mul α] (s t : Finset α) : s.card ^ 2 * t.card ^ 2 ≤ (s * t).card * s.mulEnergy t

theorem Finset.le_card_add_mul_addEnergy {α : Type u_1} [DecidableEq α] [Add α] (s t : Finset α) : s.card ^ 2 * t.card ^ 2 ≤ (s + t).card * s.addEnergy t

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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