erdos_32.variants.liminf_gt_one

Must every additive complement $A$ to the primes satisfy $\liminf_{N \to \infty} \frac{|A \cap \{1, \ldots, N\}|}{\log N} > 1$?

theorem erdos_32.variants.liminf_gt_one : ∀ A : Set ℕ,
    IsAdditiveComplementToPrimes A →
    (1 : 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.