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 : (M × M) × M × M ↦ x.1.1 * x.2.1 = x.1.2 * x.2.2) (whose density in G × G × G is mulEnergy' s t) as a standalone definition.

source

def Finset.mulEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s t : Finset M) :

ℚ≥0

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 / ↑(Fintype.card M) ^ 3

Instances For

source

def Finset.addEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] (s t : Finset M) :

ℚ≥0

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 / ↑(Fintype.card M) ^ 3

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

theorem Finset.mulEnergy'_mono {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s₁ s₂ t₁ t₂ : Finset M} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :

s₁.mulEnergy' t₁ ≤ s₂.mulEnergy' t₂

source

theorem Finset.addEnergy'_mono {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s₁ s₂ t₁ t₂ : Finset M} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :

s₁.addEnergy' t₁ ≤ s₂.addEnergy' t₂

source

theorem Finset.mulEnergy'_mono_left {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s₁ s₂ t : Finset M} (hs : s₁ ⊆ s₂) :

s₁.mulEnergy' t ≤ s₂.mulEnergy' t

source

theorem Finset.addEnergy'_mono_left {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s₁ s₂ t : Finset M} (hs : s₁ ⊆ s₂) :

s₁.addEnergy' t ≤ s₂.addEnergy' t

source

theorem Finset.mulEnergy'_mono_right {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s t₁ t₂ : Finset M} (ht : t₁ ⊆ t₂) :

s.mulEnergy' t₁ ≤ s.mulEnergy' t₂

source

theorem Finset.addEnergy'_mono_right {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s t₁ t₂ : Finset M} (ht : t₁ ⊆ t₂) :

s.addEnergy' t₁ ≤ s.addEnergy' t₂

source

theorem Finset.dens_mul_dens_le_mulEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s t : Finset M} :

s.dens * t.dens / ↑(Fintype.card M) ≤ s.mulEnergy' t

source

theorem Finset.dens_add_dens_le_addEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s t : Finset M} :

s.dens * t.dens / ↑(Fintype.card M) ≤ s.addEnergy' t

source

theorem Finset.dens_sq_le_mulEnergy'_self {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s : Finset M} :

s.dens ^ 2 / ↑(Fintype.card M) ≤ s.mulEnergy' s

source

theorem Finset.dens_sq_le_addEnergy'_self {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s : Finset M} :

s.dens ^ 2 / ↑(Fintype.card M) ≤ s.addEnergy' s

source

theorem Finset.mulEnergy'_pos {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s t : Finset M} (hs : s.Nonempty) (ht : t.Nonempty) :

0 < s.mulEnergy' t

source

theorem Finset.addEnergy'_pos {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s t : Finset M} (hs : s.Nonempty) (ht : t.Nonempty) :

0 < s.addEnergy' t

source

theorem Finset.mulEnergy'_self_pos {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s : Finset M} (hs : s.Nonempty) :

0 < s.mulEnergy' s

source

theorem Finset.addEnergy'_self_pos {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s : Finset M} (hs : s.Nonempty) :

0 < s.addEnergy' s

source

@[simp]

theorem Finset.mulEnergy'_empty_left {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (t : Finset M) :

∅.mulEnergy' t = 0

source

@[simp]

theorem Finset.addEnergy'_empty_left {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] (t : Finset M) :

∅.addEnergy' t = 0

source

@[simp]

theorem Finset.mulEnergy'_empty_right {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s : Finset M) :

s.mulEnergy' ∅ = 0

source

@[simp]

theorem Finset.addEnergy'_empty_right {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] (s : Finset M) :

s.addEnergy' ∅ = 0

source

@[simp]

theorem Finset.mulEnergy'_pos_iff {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s t : Finset M} :

0 < s.mulEnergy' t ↔ s.Nonempty ∧ t.Nonempty

source

@[simp]

theorem Finset.addEnergy'_pos_iff {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s t : Finset M} :

0 < s.addEnergy' t ↔ s.Nonempty ∧ t.Nonempty

source

@[simp]

theorem Finset.mulEnergy'_eq_zero_iff {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s t : Finset M} :

s.mulEnergy' t = 0 ↔ s = ∅ ∨ t = ∅

source

@[simp]

theorem Finset.addEnergy'_eq_zero_iff {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s t : Finset M} :

s.addEnergy' t = 0 ↔ s = ∅ ∨ t = ∅

source

theorem Finset.mulEnergy'_self_pos_iff {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s : Finset M} :

0 < s.mulEnergy' s ↔ s.Nonempty

source

theorem Finset.addEnergy'_self_pos_iff {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s : Finset M} :

0 < s.addEnergy' s ↔ s.Nonempty

source

theorem Finset.mulEnergy'_self_eq_zero_iff {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s : Finset M} :

s.mulEnergy' s = 0 ↔ s = ∅

source

theorem Finset.addEnergy'_self_eq_zero_iff {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s : Finset M} :

s.addEnergy' s = 0 ↔ s = ∅

source

theorem Finset.addEnergy'_eq_card_filter {M : Type u_2} [Fintype M] [DecidableEq M] [AddMonoid M] (s t : Finset M) :

s.addEnergy' t = ↑{x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 + x.1.2 = x.2.1 + x.2.2}.card / ↑(Fintype.card M) ^ 3

source

theorem Finset.mulEnergy'_eq_card_filter {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s t : Finset M) :

s.mulEnergy' t = ↑{x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}.card / ↑(Fintype.card M) ^ 3

source

theorem Finset.addEnergy'_eq_sum_sq' {M : Type u_2} [Fintype M] [DecidableEq M] [AddMonoid M] (s t : Finset M) :

s.addEnergy' t = ↑(∑ a ∈ s + t, {xy ∈ s ×ˢ t | xy.1 + xy.2 = a}.card ^ 2) / ↑(Fintype.card M) ^ 3

source

theorem Finset.mulEnergy'_eq_sum_sq' {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s t : Finset M) :

s.mulEnergy' t = ↑(∑ a ∈ s * t, {xy ∈ s ×ˢ t | xy.1 * xy.2 = a}.card ^ 2) / ↑(Fintype.card M) ^ 3

source

theorem Finset.addEnergy'_eq_sum_sq {M : Type u_2} [Fintype M] [DecidableEq M] [AddMonoid M] (s t : Finset M) :

s.addEnergy' t = ↑(∑ a : M, {xy ∈ s ×ˢ t | xy.1 + xy.2 = a}.card ^ 2) / ↑(Fintype.card M) ^ 3

source

theorem Finset.mulEnergy'_eq_sum_sq {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s t : Finset M) :

s.mulEnergy' t = ↑(∑ a : M, {xy ∈ s ×ˢ t | xy.1 * xy.2 = a}.card ^ 2) / ↑(Fintype.card M) ^ 3

source

theorem Finset.card_sq_le_card_mul_mulEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s t u : Finset M) :

{xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u}.dens ^ 2 ≤ u.dens * s.mulEnergy' t

source

theorem Finset.card_sq_le_card_mul_addEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] (s t u : Finset M) :

{xy ∈ s ×ˢ t | xy.1 + xy.2 ∈ u}.dens ^ 2 ≤ u.dens * s.addEnergy' t

source

theorem Finset.le_card_mul_mul_mulEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s t : Finset M) :

s.dens ^ 2 * t.dens ^ 2 ≤ (s * t).dens * s.mulEnergy' t

source

theorem Finset.le_card_add_mul_addEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] (s t : Finset M) :

s.dens ^ 2 * t.dens ^ 2 ≤ (s + t).dens * s.addEnergy' t

source

theorem Finset.mulEnergy'_comm {M : Type u_1} [Fintype M] [DecidableEq M] [CommMonoid M] (s t : Finset M) :

s.mulEnergy' t = t.mulEnergy' s

source

theorem Finset.addEnergy'_comm {M : Type u_1} [Fintype M] [DecidableEq M] [AddCommMonoid M] (s t : Finset M) :

s.addEnergy' t = t.addEnergy' s

source

@[simp]

theorem Finset.mulEnergy'_univ_left {M : Type u_1} [Fintype M] [DecidableEq M] [CommGroup M] (t : Finset M) :

univ.mulEnergy' t = t.dens ^ 2

source

@[simp]

theorem Finset.addEnergy'_univ_left {M : Type u_1} [Fintype M] [DecidableEq M] [AddCommGroup M] (t : Finset M) :

univ.addEnergy' t = t.dens ^ 2

source

@[simp]

theorem Finset.mulEnergy'_univ_right {M : Type u_1} [Fintype M] [DecidableEq M] [CommGroup M] (s : Finset M) :

s.mulEnergy' univ = s.dens ^ 2

source

@[simp]

theorem Finset.addEnergy'_univ_right {M : Type u_1} [Fintype M] [DecidableEq M] [AddCommGroup M] (s : Finset M) :

s.addEnergy' univ = s.dens ^ 2

Documentation

AddCombi.Mathlib.Combinatorics.Additive.Energy

Additive energy #

Main declarations #

Notation #

TODO #