green_61

Suppose that $A + A$ contains the first $n$ squares. Is $|A| \geq n^{1 - o(1)}$? It is known that necessarily $|A| \geq n^{2/3 - o(1)}$, whilst in the other direction there do exist such $A$ with $|A| \ll_C n / \log^C n$ for any $C$.

theorem green_61 :
    answer(sorry) ↔
      ∃ f : ℕ → ℝ, Tendsto f atTop (𝓝 0) ∧
        ∀ n : ℕ, n ≥ 1 → ∀ (A : Finset ℕ),
          (Finset.Icc 1 n).image (· ^ 2) ⊆ A + A →
            (n : ℝ) ^ (1 - f n) ≤ A.card

Recent Submissions

No submissions yet. Be the first to attempt this problem.