Sum-difference exponent of a single set

DefinitionAdmissible exponents for sums and differences#✓fully proved

A real number \(\theta\) is an admissible exponent when every nonempty finite set \(A\) of integers satisfies \(|A+A|/|A| \le (|A-A|/|A|)^{\theta}\), where \(A+A\) and \(A-A\) are the sumset and the difference set of \(A\).

def IsAdmissibleExponent (θ : ℝ) : Prop :=
  ∀ A : Finset ℤ, A.Nonempty →
    ((A + A).card : ℝ) / (A.card : ℝ) ≤
      Real.rpow (((A - A).card : ℝ) / (A.card : ℝ)) θ

Used by 1

Used byThe single-set sum-difference exponent

DefinitionThe single-set sum-difference exponent#✓fully proved

The single-set sum-difference exponent \(C_{3d}\) is the infimum of the admissible exponents, that is, of the set of real numbers \(\theta\) such that \(|A+A|/|A| \le (|A-A|/|A|)^{\theta}\) for every nonempty finite set \(A\) of integers, where \(A+A\) and \(A-A\) are the sumset and the difference set of \(A\).

This is the source's equivalent formulation of \(C_{3d}\) as a least admissible exponent, over finite sets of integers.

noncomputable def singleSetSumDifferenceExponent : ℝ :=
  sInf {θ : ℝ | IsAdmissibleExponent θ}

Uses 1 · Used by 1

Statement usesAdmissible exponents for sums and differences

Used byThe proposition that the single-set sum-difference exponent equals 2

DefinitionThe proposition that the single-set sum-difference exponent equals 2#✓fully proved

This is the statement that the single-set sum-difference exponent \(C_{3d}\) is equal to \(2\).

def singleSetSumDifferenceExponent_eq_two : Prop :=
  singleSetSumDifferenceExponent = 2

Uses 1 · Used by 1

Statement usesThe single-set sum-difference exponent

Used byThe single-set sum-difference exponent equals 2

TheoremThe single-set sum-difference exponent equals 2#●ready to prove

The single-set sum-difference exponent \(C_{3d}\) is equal to \(2\).

Known constructions approach this value but do not attain it.

public theorem_wanted singleSetSumDifferenceExponent_eq_two_holds : singleSetSumDifferenceExponent_eq_two

Sources

• Haowei Lin and Shanda Li, Settling the optimal exponent relating sumsets and difference sets, arXiv:2607.27199v1 (2026), https://arxiv.org/abs/2607.27199v1.

Uses 1

Statement usesThe proposition that the single-set sum-difference exponent equals 2

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.