Erdős problem 281
Let be an infinite sequence such that, for any choice of congruence classes , the set of integers not satisfying any of the congruences has density . Is it true that for every there exists some such that, for every choice of congruence classes , the density of integers not satisfying any of the congruences for is less than ?
Sources
FormalConjectures/ErdosProblems/
281.lean
Let be an infinite sequence such that, for any choice of congruence classes , the set of integers not satisfying any of the congruences has density . Is it true that for every there exists some such that, for every choice of congruence classes , the density of integers not satisfying any of the congruences for is less than ?
The answer is yes; the linked Lean proof formalizes Somani's argument.
True ↔ ∀ (n : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 0 < n i) → (∀ (a : Erdos281.ResidueChoice n), (Erdos281.avoidAll n a).HasIntDensity 0) → ∀ (ε : ℝ), 0 < ε → ∃ k, ∀ (a : Erdos281.ResidueChoice n), ∃ d, (Erdos281.avoidPrefix n a k).HasIntDensity d ∧ d < ε