Erdős problem 25
Let be an arbitrary sequence of integers, each with an associated residue class . Let be the set of integers such that for every either or . Must the logarithmic density of exist?
Sources
FormalConjectures/ErdosProblems/
25.lean
Retained formal statement
Let be an arbitrary sequence of integers, each with an associated residue class . Let be the set of integers such that for every either or . Must the logarithmic density of exist?
True ↔ ∀ (seq_n : ℕ → ℕ) (seq_a : ℕ → ℤ), (∀ (i : ℕ), 0 < seq_n i) → StrictMono seq_n → ∃ d, {x | ∀ (i : ℕ), ↑x < ↑(seq_n i) ∨ ¬↑x ≡ seq_a i [ZMOD ↑(seq_n i)]}.HasLogDensity dOpenStatement only, no proof