Mathlib Phrasebook

1.2. Quantities🔗

1.2.1. Doubling constant🔗

The easiest way to talk about a Finset having doubling at most K is simply

open scoped Finset variable {G : Type*} [AddCommGroup G] [DecidableEq G] {K : ℝ} {A : Finset G} (hA : #(A + A) ≤ K * #A)

and similarly for small difference. One can also write the doubling and difference constants Finset.addConst and Finset.subConst directly as follows:

open scoped Combinatorics.Additive σ[A] : ℚ≥0#check σ[A] δ[A] : ℚ≥0#check δ[A] 
σ[A] : ℚ≥0
δ[A] : ℚ≥0

The multiplicative doubling and difference constants Finset.mulConst and Finset.divConst are denote σₘ[A] and δₘ[A].

One can relate σ[A] ≤ K and #(A + A) ≤ K * #A through Finset.addConst_mul_card.

Mathlib contains the proof of the Ruzsa triangle and Plünnecke-Ruzsa inequalities. See Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_sub.

1.2.2. Energy🔗

The energy of a Finset is Finset.addEnergy:

variable {A : Finset G} open scoped Combinatorics.Additive E[A] : ℕ#check E[A]

Similarly to the doubling constant, the multiplicative energy Finset.mulEnergy is denoted Eₘ[A].

Mathlib knows that sets of small doubling have large energy (see Finset.le_card_add_mul_addEnergy), and AddCombi knows the partial converse, namely the Balog-Szemerédi-Gowers theorem (see BSG).

1.2.3. Covering🔗

To say that a set B is covered by K translates of another set A, one can use the predicate CovByVAdd (or its multiplicative version CovBySMul):

variable {A B : Set G} {K : ℝ} (hAB : CovByVAdd G K A B)

This is in turn used to define approximate subgroups:

variable (hA : IsApproximateAddSubgroup K A)