Erdős Problem 281

References:

• erdosproblems.com/281
• [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
• [DaEr36] Davenport, H. and Erdős, P., On sequences of positive integers. Acta Arithmetica (1936), 147-151.
• [HaRo66] Halberstam, H. and Roth, K. F., Sequences. Vol. I. (1966), xx+291.

def Erdos281.ResidueChoice (n : ℕ → ℕ) : Type

Choices of congruence classes $a_i \pmod{n_i}$.

Equations

• Erdos281.ResidueChoice n = ((i : ℕ) → ZMod (n i))

def Erdos281.avoidAll (n : ℕ → ℕ) (a : ResidueChoice n) : Set ℤ

The integers avoiding all congruences $a_i \pmod{n_i}$.

Equations

• Erdos281.avoidAll n a = {m : ℤ | ∀ (i : ℕ), ↑m ≠ a i}

def Erdos281.avoidPrefix (n : ℕ → ℕ) (a : ResidueChoice n) (k : ℕ) : Set ℤ

The integers avoiding the first $k$ congruences $a_i \pmod{n_i}$.

Equations

• Erdos281.avoidPrefix n a k = {m : ℤ | ∀ i < k, ↑m ≠ a i}

theorem Erdos281.erdos_281 : True ↔ ∀ (n : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 0 < n i) → (∀ (a : ResidueChoice n), (avoidAll n a).HasIntDensity 0) → ∀ (ε : ℝ), 0 < ε → ∃ (k : ℕ), ∀ (a : ResidueChoice n), ∃ (d : ℝ), (avoidPrefix n a k).HasIntDensity d ∧ d < ε

Let $n_1<n_2<\cdots$ be an infinite sequence such that, for any choice of congruence classes $a_i\pmod{n_i}$, the set of integers not satisfying any of the congruences $a_i\pmod{n_i}$ has density $0$. Is it true that for every $\epsilon>0$ there exists some $k$ such that, for every choice of congruence classes $a_i$, the density of integers not satisfying any of the congruences $a_i\pmod{n_i}$ for $1\leq i\leq k$ is less than $\epsilon$?

The answer is yes; the linked Lean proof formalizes Somani's argument.