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.addEnergy {α : Type u_1} [DecidableEq α] [Add α] (s : Finset α) (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 = (Finset.filter (fun (x : (α × α) × α × α) => x.1.1 + x.2.1 = x.1.2 + x.2.2) ((s ×ˢ s) ×ˢ t ×ˢ t)).card

def Finset.mulEnergy {α : Type u_1} [DecidableEq α] [Mul α] (s : Finset α) (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 = (Finset.filter (fun (x : (α × α) × α × α) => x.1.1 * x.2.1 = x.1.2 * x.2.2) ((s ×ˢ s) ×ˢ t ×ˢ t)).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ₘ[_,_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

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[_,_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

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ₘ[_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

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.

def Combinatorics.Additive.«termE[_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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.

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

theorem Finset.mulEnergy_eq_card_filter {α : Type u_1} [DecidableEq α] [Mul α] (s : Finset α) (t : Finset α) : 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} [DecidableEq α] [Add α] (s : Finset α) (t : Finset α) : s.addEnergy t = ∑ a ∈ s + t, (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

• Finset.addEnergy_eq_sum_sq'.match_1 motive x h_1 = Prod.casesOn x fun (fst snd : α) => h_1 fst snd

theorem Finset.mulEnergy_eq_sum_sq' {α : Type u_1} [DecidableEq α] [Mul α] (s : Finset α) (t : Finset α) : s.mulEnergy t = ∑ a ∈ s * t, (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} [DecidableEq α] [Add α] [Fintype α] (s : Finset α) (t : Finset α) : s.addEnergy t = ∑ 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} [DecidableEq α] [Mul α] [Fintype α] (s : Finset α) (t : Finset α) : s.mulEnergy t = ∑ 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} [DecidableEq α] [Add α] (s : Finset α) (t : Finset α) (u : Finset α) : (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} [DecidableEq α] [Mul α] (s : Finset α) (t : Finset α) (u : Finset α) : (Finset.filter (fun (x : α × α) => match x with | (a, b) => a * b ∈ u) (s ×ˢ t)).card ^ 2 ≤ u.card * s.mulEnergy t

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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