Erdős Problem 851

Reference: erdosproblems.com/851

def Erdos851.TwoPowAddSet (r : ℕ) : Set ℕ

TwoPowAddSet r is the set of integers of the form 2^k+n, where k ≥ 0 and n has at most r prime divisors.

Equations

• Erdos851.TwoPowAddSet r = {x : ℕ | ∃ (k : ℕ) (n : ℕ) (_ : n.primeFactors.card ≤ r), 2 ^ k + n = x}

theorem Erdos851.erdos_851.variants.romanoff : 0 < (TwoPowAddSet 1).lowerDensity

The set of integers of the form 2^k+p (where p is prime) has positive lower density.

Formalisation note: here we also allow p = 1 since this simplifies the code and is equivalent to the original statement.

theorem Erdos851.erdos_851 (ε : ℝ) (hε : ε ∈ Set.Ioo 0 1) : ∃ (r : ℕ) (d : ℝ), (TwoPowAddSet r).HasDensity d ∧ 1 - ε ≤ d

Let $\epsilon > 0$. Is there some $r \ll_\epsilon 1$ such that the density of integers of the form $2^k+n$, where $k \geq 0$ and $n$ has at most $r$ prime divisors, is at least $1-\epsilon$?