Sum-product estimates for sets of small doubling

DefinitionErdős Problem 818#✓fully proved

The statement that for every real \(K > 0\) there are reals \(C > 0\) and \(c > 0\) such that every finite set \(A\) of integers with \(|A| \ge 2\) and \(|A + A| \le K|A|\) satisfies \(c|A|^2 / (\log |A|)^C \le |A \cdot A|\). Here \(A + A = \{a + b : a, b \in A\}\), \(A \cdot A = \{ab : a, b \in A\}\) and \(\log\) is the natural logarithm.

def conjecture : Prop :=
  ∀ K : ℝ, 0 < K → ∃ C : ℝ, 0 < C ∧ ∃ c : ℝ, 0 < c ∧
    ∀ A : Finset ℤ, 2 ≤ A.card → ((A + A).card : ℝ) ≤ K * (A.card : ℝ) →
      c * (A.card : ℝ) ^ 2 / (Real.log (A.card : ℝ)) ^ C ≤ ((A * A).card : ℝ)

Used by 1

Used byErdős Problem 818 is true

TheoremErdős Problem 818 is true#●ready to prove

For every real \(K > 0\) there are reals \(C > 0\) and \(c > 0\) such that every finite set \(A\) of integers with \(|A| \ge 2\) and \(|A + A| \le K|A|\) satisfies \(c|A|^2 / (\log |A|)^C \le |A \cdot A|\). Here \(A + A = \{a + b : a, b \in A\}\), \(A \cdot A = \{ab : a, b \in A\}\) and \(\log\) is the natural logarithm.

József Solymosi proved a stronger bound, with a single logarithm in the denominator.

public theorem_wanted conjecture_holds : conjecture

def conjecture : Prop :=
  ∀ K : ℝ, 0 < K → ∃ C : ℝ, 0 < C ∧ ∃ c : ℝ, 0 < c ∧
    ∀ A : Finset ℤ, 2 ≤ A.card → ((A + A).card : ℝ) ≤ K * (A.card : ℝ) →
      c * (A.card : ℝ) ^ 2 / (Real.log (A.card : ℝ)) ^ C ≤ ((A * A).card : ℝ)

WantedExt/NumberTheory/ErdosProblem818Wanted.lean:35

Sources

József Solymosi, Bounding multiplicative energy by the sumset, Advances in Mathematics 222 (2009), 402–408, https://doi.org/10.1016/j.aim.2009.04.006.

Uses 1

Statement usesErdős Problem 818

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.