Erdős problem 25

Let $n_1 < n_2 < \dots$ be an arbitrary sequence of integers, each with an associated residue class $a_i \pmod{n_i}$ . Let $A$ be the set of integers $n$ such that for every $i$ either $n < n_i$ or $n \not\equiv a_i \pmod{n_i}$ . Must the logarithmic density of $A$ exist?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

25.lean

Retained formal statement1 of 1

Let $n_1 < n_2 < \dots$ be an arbitrary sequence of integers, each with an associated residue class $a_i \pmod{n_i}$ . Let $A$ be the set of integers $n$ such that for every $i$ either $n < n_i$ or $n \not\equiv a_i \pmod{n_i}$ . Must the logarithmic density of $A$ exist?

FormalConjectures/ErdosProblems/25.leanErdos25.erdos_254 linesExact file

1True ↔2  ∀ (seq_n : ℕ → ℕ) (seq_a : ℕ → ℤ),3    (∀ (i : ℕ), 0 < seq_n i) →4      StrictMono seq_n → ∃ d, {x | ∀ (i : ℕ), ↑x < ↑(seq_n i) ∨ ¬↑x ≡ seq_a i [ZMOD ↑(seq_n i)]}.HasLogDensity d

OpenStatement only, no proof