erdos_32.variants.ruzsa

Ruzsa proved that any additive complement $A$ to the primes must satisfy $\liminf_{N \to \infty} \frac{|A \cap \{1, \ldots, N\}|}{\log N} \geq e^\gamma$, where $\gamma$ is the Euler-Mascheroni constant.

theorem erdos_32.variants.ruzsa : ∀ A : Set ℕ,
    IsAdditiveComplementToPrimes A →
    (Real.exp Real.eulerMascheroniConstant : EReal) ≤
      liminf (fun N => (((Finset.Icc 1 N).filter (· ∈ A)).card / Real.log N : EReal)) atTop

Recent Submissions

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