Erdős Problem 280

References:

• erdosproblems.com/280
• [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

def Erdos280.isCoveredBy (n a : ℕ → ℕ) (m k : ℕ) : Prop

The integer m is covered by one of the first k chosen congruence classes.

Equations

• Erdos280.isCoveredBy n a m k = ∃ i ∈ Finset.Icc 1 k, m % n i = a i

noncomputable def Erdos280.uncoveredCount (n a : ℕ → ℕ) (k : ℕ) : ℕ

The number of integers below n k not covered by the first k congruence classes.

Equations

• Erdos280.uncoveredCount n a k = {m ∈ Finset.range (n k) | ¬Erdos280.isCoveredBy n a m k}.card

theorem Erdos280.erdos_280 : False ↔ ∀ (n a : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 1 ≤ i → a i < n i) → (∃ (ε : ℝ), 0 < ε ∧ ∀ (k : ℕ), 1 ≤ k → ↑(n k) > (1 + ε) * ↑k * Real.log ↑k) → ¬Filter.Tendsto (fun (k : ℕ) => ↑(uncoveredCount n a k) / ↑k) Filter.atTop (nhds 0)

Let $n_1<n_2<\cdots $ be an infinite sequence of integers with associated $a_k\pmod{n_k}$, such that for some $\epsilon>0$ we have $n_k>(1+\epsilon)k\log k$ for all $k$. Then [ #{ m<n_k : m\not\equiv a_i\pmod{n_i} \textrm{ for }1\leq i\leq k}\neq o(k). ]

Cambie observed that this is false.