erdos_32.varaints.log_squared

Erdős proved in [Erd54] that there exists an additive complement $A$ to the primes with $|A \cap \{1, \ldots, N\}| = O((\log N)^2)$.

theorem erdos_32.varaints.log_squared : ∃ A : Set ℕ,
    IsAdditiveComplementToPrimes A ∧
    (fun N => (((Finset.Icc 1 N).filter (· ∈ A)).card : ℝ)) =O[atTop]
      fun N => (Real.log N) ^ 2

Recent Submissions

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