# Documentation

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.addEnergy {α : Type u_1} [] [Add α] (s : ) (t : ) :

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
Instances For
def Finset.mulEnergy {α : Type u_1} [] [Mul α] (s : ) (t : ) :

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
Instances For

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.
Instances For

Pretty printer defined by notation3 command.

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

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.
Instances For

Pretty printer defined by notation3 command.

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

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.
Instances For

Pretty printer defined by notation3 command.

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

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.
Instances For

Pretty printer defined by notation3 command.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Finset.addEnergy_mono {α : Type u_1} [] [Add α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
theorem Finset.mulEnergy_mono {α : Type u_1} [] [Mul α] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.mulEnergy t₁ s₂.mulEnergy t₂
theorem Finset.addEnergy_mono_left {α : Type u_1} [] [Add α] {s₁ : } {s₂ : } {t : } (hs : s₁ s₂) :
theorem Finset.mulEnergy_mono_left {α : Type u_1} [] [Mul α] {s₁ : } {s₂ : } {t : } (hs : s₁ s₂) :
s₁.mulEnergy t s₂.mulEnergy t
theorem Finset.addEnergy_mono_right {α : Type u_1} [] [Add α] {s : } {t₁ : } {t₂ : } (ht : t₁ t₂) :
theorem Finset.mulEnergy_mono_right {α : Type u_1} [] [Mul α] {s : } {t₁ : } {t₂ : } (ht : t₁ t₂) :
s.mulEnergy t₁ s.mulEnergy t₂
theorem Finset.le_addEnergy {α : Type u_1} [] [Add α] {s : } {t : } :
theorem Finset.le_mulEnergy {α : Type u_1} [] [Mul α] {s : } {t : } :
s.card * t.card s.mulEnergy t
theorem Finset.addEnergy_pos {α : Type u_1} [] [Add α] {s : } {t : } (hs : s.Nonempty) (ht : t.Nonempty) :
theorem Finset.mulEnergy_pos {α : Type u_1} [] [Mul α] {s : } {t : } (hs : s.Nonempty) (ht : t.Nonempty) :
0 < s.mulEnergy t
@[simp]
theorem Finset.addEnergy_empty_left {α : Type u_1} [] [Add α] (t : ) :
@[simp]
theorem Finset.mulEnergy_empty_left {α : Type u_1} [] [Mul α] (t : ) :
.mulEnergy t = 0
@[simp]
theorem Finset.addEnergy_empty_right {α : Type u_1} [] [Add α] (s : ) :
@[simp]
theorem Finset.mulEnergy_empty_right {α : Type u_1} [] [Mul α] (s : ) :
s.mulEnergy = 0
@[simp]
theorem Finset.addEnergy_pos_iff {α : Type u_1} [] [Add α] {s : } {t : } :
0 < s.addEnergy t s.Nonempty t.Nonempty
@[simp]
theorem Finset.mulEnergy_pos_iff {α : Type u_1} [] [Mul α] {s : } {t : } :
0 < s.mulEnergy t s.Nonempty t.Nonempty
@[simp]
theorem Finset.addEnergy_eq_zero_iff {α : Type u_1} [] [Add α] {s : } {t : } :
s.addEnergy t = 0 s = t =
@[simp]
theorem Finset.mulEnergy_eq_zero_iff {α : Type u_1} [] [Mul α] {s : } {t : } :
s.mulEnergy t = 0 s = t =
theorem Finset.addEnergy_eq_card_filter {α : Type u_1} [] [Add α] (s : ) (t : ) :
s.addEnergy t = (Finset.filter (fun (x : (α × α) × α × α) => Finset.addEnergy_eq_card_filter.match_1 (fun (x : (α × α) × α × α) => Prop) x fun (a b c d : α) => a + b = c + d) ((s ×ˢ t) ×ˢ s ×ˢ t)).card
abbrev Finset.addEnergy_eq_card_filter.match_1 {α : Type u_1} (motive : (α × α) × α × αSort u_2) :
(x : (α × α) × α × α) → ((a b c d : α) → motive ((a, b), c, d))motive x
Equations
• One or more equations did not get rendered due to their size.
Instances For
abbrev Finset.addEnergy_eq_card_filter.match_2 {α : Type u_1} [] [Add α] (s : ) (t : ) (motive : (x : (α × α) × α × α) → x Finset.filter (fun (x : (α × α) × α × α) => x.1.1 + x.2.1 = x.1.2 + x.2.2) ((s ×ˢ s) ×ˢ t ×ˢ t)Sort u_2) :
(x : (α × α) × α × α) → (x_1 : x Finset.filter (fun (x : (α × α) × α × α) => x.1.1 + x.2.1 = x.1.2 + x.2.2) ((s ×ˢ s) ×ˢ t ×ˢ t)) → ((a b c d : α) → (x : ((a, b), c, d) Finset.filter (fun (x : (α × α) × α × α) => x.1.1 + x.2.1 = x.1.2 + x.2.2) ((s ×ˢ s) ×ˢ t ×ˢ t)) → motive ((a, b), c, d) x)motive x x_1
Equations
• One or more equations did not get rendered due to their size.
Instances For
abbrev Finset.addEnergy_eq_card_filter.match_3 {α : Type u_1} [] [Add α] (s : ) (t : ) (motive : (x : (α × α) × α × α) → x Finset.filter (fun (x : (α × α) × α × α) => Finset.addEnergy_eq_card_filter.match_1 (fun (x : (α × α) × α × α) => Prop) x fun (a b c d : α) => a + b = c + d) ((s ×ˢ t) ×ˢ s ×ˢ t)Prop) :
∀ (x : (α × α) × α × α) (h : x Finset.filter (fun (x : (α × α) × α × α) => Finset.addEnergy_eq_card_filter.match_1 (fun (x : (α × α) × α × α) => Prop) x fun (a b c d : α) => a + b = c + d) ((s ×ˢ t) ×ˢ s ×ˢ t)), (∀ (a b c d : α) (h : ((a, b), c, d) Finset.filter (fun (x : (α × α) × α × α) => Finset.addEnergy_eq_card_filter.match_1 (fun (x : (α × α) × α × α) => Prop) x fun (a b c d : α) => a + b = c + d) ((s ×ˢ t) ×ˢ s ×ˢ t)), motive ((a, b), c, d) h)motive x h
Equations
• =
Instances For
theorem Finset.mulEnergy_eq_card_filter {α : Type u_1} [] [Mul α] (s : ) (t : ) :
s.mulEnergy t = (Finset.filter (fun (x : (α × α) × α × α) => match x with | ((a, b), c, d) => a * b = c * d) ((s ×ˢ t) ×ˢ s ×ˢ t)).card
theorem Finset.addEnergy_eq_sum_sq' {α : Type u_1} [] [Add α] (s : ) (t : ) :
s.addEnergy t = (s + t).sum fun (a : α) => (Finset.filter (fun (x : α × α) => Finset.addEnergy_eq_sum_sq'.match_1 (fun (x : α × α) => Prop) x fun (x y : α) => x + y = a) (s ×ˢ t)).card ^ 2
abbrev Finset.addEnergy_eq_sum_sq'.match_1 {α : Type u_1} (motive : α × αSort u_2) :
(x : α × α) → ((x y : α) → motive (x, y))motive x
Equations
Instances For
theorem Finset.mulEnergy_eq_sum_sq' {α : Type u_1} [] [Mul α] (s : ) (t : ) :
s.mulEnergy t = (s * t).sum fun (a : α) => (Finset.filter (fun (x : α × α) => match x with | (x, y) => x * y = a) (s ×ˢ t)).card ^ 2
theorem Finset.addEnergy_eq_sum_sq {α : Type u_1} [] [Add α] [] (s : ) (t : ) :
s.addEnergy t = Finset.univ.sum fun (a : α) => (Finset.filter (fun (x : α × α) => Finset.addEnergy_eq_sum_sq'.match_1 (fun (x : α × α) => Prop) x fun (x y : α) => x + y = a) (s ×ˢ t)).card ^ 2
theorem Finset.mulEnergy_eq_sum_sq {α : Type u_1} [] [Mul α] [] (s : ) (t : ) :
s.mulEnergy t = Finset.univ.sum fun (a : α) => (Finset.filter (fun (x : α × α) => match x with | (x, y) => x * y = a) (s ×ˢ t)).card ^ 2
theorem Finset.card_sq_le_card_mul_addEnergy {α : Type u_1} [] [Add α] (s : ) (t : ) (u : ) :
(Finset.filter (fun (x : α × α) => Finset.addEnergy_eq_sum_sq'.match_1 (fun (x : α × α) => Prop) x fun (a b : α) => a + b u) (s ×ˢ t)).card ^ 2 u.card * s.addEnergy t
theorem Finset.card_sq_le_card_mul_mulEnergy {α : Type u_1} [] [Mul α] (s : ) (t : ) (u : ) :
(Finset.filter (fun (x : α × α) => match x with | (a, b) => a * b u) (s ×ˢ t)).card ^ 2 u.card * s.mulEnergy t
s.card ^ 2 * t.card ^ 2 (s + t).card * s.addEnergy t
theorem Finset.le_card_add_mul_mulEnergy {α : Type u_1} [] [Mul α] (s : ) (t : ) :
s.card ^ 2 * t.card ^ 2 (s * t).card * s.mulEnergy t
theorem Finset.addEnergy_comm {α : Type u_1} [] [] (s : ) (t : ) :
theorem Finset.mulEnergy_comm {α : Type u_1} [] [] (s : ) (t : ) :
s.mulEnergy t = t.mulEnergy s
@[simp]
theorem Finset.addEnergy_univ_left {α : Type u_1} [] [] [] (t : ) :
Finset.univ.addEnergy t = * t.card ^ 2
@[simp]
theorem Finset.mulEnergy_univ_left {α : Type u_1} [] [] [] (t : ) :
Finset.univ.mulEnergy t = * t.card ^ 2
@[simp]
theorem Finset.addEnergy_univ_right {α : Type u_1} [] [] [] (s : ) :
s.addEnergy Finset.univ = * s.card ^ 2
@[simp]
theorem Finset.mulEnergy_univ_right {α : Type u_1} [] [] [] (s : ) :
s.mulEnergy Finset.univ = * s.card ^ 2