Erdős Problem 244

Reference: erdosproblems.com/244

theorem Erdos244.erdos_244 : (∀ C > 1, 0 < {x : ℕ | ∃ (p : ℕ) (k : ℕ) (_ : Nat.Prime p), p + ⌊C ^ k⌋₊ = x}.lowerDensity) ↔ sorry

Let $C > 1$. Does the set of integers of the form $p + \lfloor C^k \rfloor$, for some prime $p$ and $k\geq 0$, have density $>0$?

theorem Erdos244.erdos_244.variants.Romanoff {C : ℕ} (hC : 1 < C) : 0 < {x : ℕ | ∃ (p : ℕ) (k : ℕ) (_ : Nat.Prime p), p + ⌊C ^ k⌋₊ = x}.lowerDensity

Romanoff [Ro34] proved that the answer is yes if $C$ is an integer.

[Ro34] Romanoff, N. P., Über einige Sätze der additiven Zahlentheorie. Math. Ann. (1934), 668-678.