Documentation

Mathlib.Combinatorics.Additive.Energy

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.

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
    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
      theorem Finset.additiveEnergy_mono {α : Type u_1} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} (hs : s₁ s₂) (ht : t₁ t₂) :
      theorem Finset.multiplicativeEnergy_mono {α : Type u_1} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} (hs : s₁ s₂) (ht : t₁ t₂) :
      theorem Finset.additiveEnergy_mono_left {α : Type u_1} [DecidableEq α] [Add α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} (hs : s₁ s₂) :
      theorem Finset.multiplicativeEnergy_mono_left {α : Type u_1} [DecidableEq α] [Mul α] {s₁ : Finset α} {s₂ : Finset α} {t : Finset α} (hs : s₁ s₂) :
      theorem Finset.additiveEnergy_mono_right {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} (ht : t₁ t₂) :
      theorem Finset.multiplicativeEnergy_mono_right {α : Type u_1} [DecidableEq α] [Mul α] {s : Finset α} {t₁ : Finset α} {t₂ : Finset α} (ht : t₁ t₂) :
      theorem Finset.additiveEnergy_pos {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} (hs : Finset.Nonempty s) (ht : Finset.Nonempty t) :
      @[simp]
      @[simp]
      theorem Finset.additive_energy_eq_zero_iff {α : Type u_1} [DecidableEq α] [Add α] {s : Finset α} {t : Finset α} :
      @[simp]
      @[simp]
      @[simp]