Additive combinatorics

DefinitionSets without arithmetic progressions#

A set is 3AP-free if it does not contain any non-trivial arithmetic progression of length three.

This is also sometimes called a non-averaging set or Salem-Spencer set.

ThreeAPFree.{u_2} {α : Type u_2} [AddMonoid α] (s : Set α) : Prop
Sources
MathlibThreeAPFree
Uses 1 · Used by 2
Statement usesNatural number
Used byBehrend's construction · Roth's theorem

TheoremRoth's theorem#

Roth's theorem for ℕ.

The maximum density of a 3AP-free set in {1, ..., n} goes to zero as n tends to infinity.

roth_3ap_theorem_nat {n : ℕ} (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound (ε / 3) ≤ n)
  (A : Finset ℕ) (hAn : A ⊆ Finset.range n) (hAε : ε * ↑n ≤ ↑A.card) : ¬ThreeAPFree ↑A
Sources
Mathlibroth_3ap_theorem_nat
Uses 7
Statement usesLogarithm · Sets without arithmetic progressions
Proof usesAffine space · Freiman homomorphisms · Permutation group of a type · Regularity lemma · Triangle counting lemma

TheoremCorners theorem#

The corners theorem for ℕ.

The maximum density of a corner-free set in {1, ..., n} × {1, ..., n} goes to zero as n tends to infinity.

corners_theorem_nat {n : ℕ} {ε : ℝ} (hε : 0 < ε) (hn : cornersTheoremBound (ε / 9) ≤ n)
  (A : Finset (ℕ × ℕ)) (hAn : A ⊆ Finset.range n ×ˢ Finset.range n) (hAε : ε * ↑n ^ 2 ≤ ↑A.card) :
  ¬IsCornerFree ↑A
Sources
Mathlibcorners_theorem_nat
Uses 5
Statement usesLogarithm
Proof usesAffine space · Freiman homomorphisms · Regularity lemma · Triangle counting lemma

TheoremBehrend's construction#

Mathlib states this as Behrend.roth_lower_bound.

Behrend.roth_lower_bound {N : ℕ} : ↑N * Real.exp (-4 * √(Real.log ↑N)) ≤ ↑(rothNumberNat N)
Sources
MathlibBehrend.roth_lower_bound
Uses 11
Statement usesLogarithm · Sets without arithmetic progressions
Proof usesCharacteristic p · Characteristic zero · Closure · Euclidean domain · Freiman homomorphisms · Inner product space, over \(R\) or \(C\) · Norms \(\lVert\cdot\rVert_p\) on \(\R^n\) and \(\C^n\) · Ordered ring · The Binomial Theorem

DefinitionDoubling constant#

The doubling constant σ[A, B] of two finsets A and B in a group is |A + B| / |A|.

The notation σ[A, B] is available in scope Combinatorics.Additive.

Finset.addConst.{u_1} {G : Type u_1} [AddGroup G] [DecidableEq G] (A B : Finset G) : ℚ≥0
Sources
MathlibFinset.addConst
Uses 2
Statement usesFinite set · Rational number

TheoremRuzsa covering lemma#

Ruzsa's covering lemma for sets. See also Finset.ruzsa_covering_add.

Set.ruzsa_covering_add.{u_1} {G : Type u_1} [AddGroup G] {K : ℝ} {A B : Set G} (hA : A.Finite)
  (hB : B.Finite) (hB₀ : B.Nonempty) (hK : ↑(Nat.card ↑(A + B)) ≤ K * ↑(Nat.card ↑B)) :
  ∃ F ⊆ A, ↑(Nat.card ↑F) ≤ K ∧ A ⊆ F + (B - B) ∧ F.Finite
Sources
MathlibSet.ruzsa_covering_add
Uses 5
Statement usesCardinal · Real number · Ring morphism
Proof usesFinite set · Order

TheoremRuzsa triangle inequality#

Ruzsa's triangle inequality. Subtraction version.

Finset.ruzsa_triangle_inequality_sub_sub_sub.{u_1} {G : Type u_1} [DecidableEq G] [AddGroup G]
  (A B C : Finset G) : (A - C).card * B.card ≤ (A - B).card * (C - B).card
Sources
MathlibFinset.ruzsa_triangle_inequality_sub_sub_sub
Uses 2
Statement usesFinite set · Integer

TheoremPlünnecke-Petridis inequality#

Mathlib states this as Finset.pluennecke_petridis_inequality_add.

Finset.pluennecke_petridis_inequality_add.{u_1} {G : Type u_1} [DecidableEq G] [AddGroup G]
  {A B : Finset G} (C : Finset G) (hA : ∀ A' ⊆ A, (A + B).card * A'.card ≤ (A' + B).card * A.card) :
  (C + A + B).card * A.card ≤ (A + B).card * (C + A).card
Sources
MathlibFinset.pluennecke_petridis_inequality_add
Uses 2
Statement usesFinite set · Integer

TheoremSmall tripling implies small powers#

If A is symmetric (A⁻¹ = A) and has small tripling, then A has small powers, in the sense that |A ^ m| is at most |A| times a constant exponential in m.

See also Finset.small_alternating_pow_of_small_tripling for a version with a weaker constant but which encompasses non-symmetric sets.

Finset.small_pow_of_small_tripling.{u_1} {G : Type u_1} [DecidableEq G] [Group G] {A : Finset G}
  {K : ℝ} {m : ℕ} (hm : 3 ≤ m) (hA : ↑(A ^ 3).card ≤ K * ↑A.card) (hAsymm : A⁻¹ = A) :
  ↑(A ^ m).card ≤ K ^ (m - 2) * ↑A.card
Sources
MathlibFinset.small_pow_of_small_tripling
Uses 5
Statement usesFinite set · Real number
Proof usesCharacteristic zero · Order · Ordered ring

DefinitionDyson transform#

The Dyson e-transform. Turns (s, t) into (s ∪ e +ᵥ t, t ∩ -e +ᵥ s). This reduces the sum of the two sets.

Finset.addDysonETransform.{u_1} {α : Type u_1} [DecidableEq α] [AddCommGroup α] (e : α)
  (x : Finset α × Finset α) : Finset α × Finset α
Sources
MathlibFinset.addDysonETransform
Uses 2
Statement usesFinite set · Integer

TheoremCauchy-Davenport theorem#

The Cauchy-Davenport Theorem. If s, t are nonempty sets in ℤ/pℤ, then the size of s + t is lower-bounded by |s| + |t| - 1, unless this quantity is greater than p.

ZMod.cauchy_davenport {p : ℕ} (hp : Nat.Prime p) {s t : Finset (ZMod p)} (hs : s.Nonempty)
  (ht : t.Nonempty) : min p (s.card + t.card - 1) ≤ (s + t).card
Sources
MathlibZMod.cauchy_davenport
Uses 8
Statement usesFinite set · Integer · Irreducible element
Proof usesCardinal · Characteristic zero · Ordered ring · Periodic points · Ring morphism

TheoremErdős–Ginzburg–Ziv theorem#

The Erdős–Ginzburg–Ziv theorem for ℤ/nℤ.

Any sequence of at least 2 * n - 1 elements of ZMod n contains a subsequence of n elements whose sum is zero.

ZMod.erdos_ginzburg_ziv.{u_1} {ι : Type u_1} {n : ℕ} {s : Finset ι} (a : ι → ZMod n)
  (hs : 2 * n - 1 ≤ s.card) : ∃ t ⊆ s, t.card = n ∧ ∑ i ∈ t, a i = 0
Sources
MathlibZMod.erdos_ginzburg_ziv
Uses 9
Statement usesFinite set · Integer · Ring
Proof usesAssociative algebra over a commutative ring · Characteristic zero · Chevalley–Warning theorem (1000+ theorems) · Fermat's little theorem · Linear map · Ring structure \(\Z\)

DefinitionAdditive energy#

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.

Finset.addEnergy.{u_1} {α : Type u_1} [DecidableEq α] [Add α] (s t : Finset α) : ℕ
Sources
MathlibFinset.addEnergy
Uses 2
Statement usesFinite set · Natural number

StructureFreiman homomorphisms#

An additive n-Freiman homomorphism from a set A to a set B is a map which preserves sums of n elements.

IsAddFreimanHom.{u_2, u_3} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (n : ℕ)
  (A : Set α) (B : Set β) (f : α → β) : Prop
Sources
MathlibIsAddFreimanHom
Uses 2 · Used by 3
Statement usesMultiset · Natural number
Used byBehrend's construction · Corners theorem · Roth's theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.