Erdős Problem 688

Reference:

• erdosproblems.com/688
• [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.

def Erdos688.Erdos688Prop (n : ℕ) (ε : ℝ) : Prop

Define $\epsilon_n$ to be maximal such that there exists some choice of congruence class $a_p$ for all primes $n^{\epsilon_n} < p \leq n$ such that every integer in $[1,n]$ satisfies at least one of the congruences $\equiv a_p \pmod p$.

Equations

• Erdos688.Erdos688Prop n ε = ∃ (a : ℕ → ℕ), ∀ (m : ℕ), 1 ≤ m → m ≤ n → ∃ (p : ℕ), Nat.Prime p ∧ ↑n ^ ε < ↑p ∧ p ≤ n ∧ a p ≡ m [MOD p]

noncomputable def Erdos688.epsilonFunction (n : ℕ) : ℝ

Equations

• Erdos688.epsilonFunction n = sSup {ε : ℝ | Erdos688.Erdos688Prop n ε}

theorem Erdos688.erdos_688.parts.i.lower_bound : sorry =O[Filter.atTop] epsilonFunction

Estimate $\epsilon_n$ - lower bound.

theorem Erdos688.erdos_688.parts.i.upper_bound : epsilonFunction =O[Filter.atTop] sorry

Estimate $\epsilon_n$ - upper bound.

theorem Erdos688.erdos_688.parts.ii : True ↔ epsilonFunction =o[Filter.atTop] fun (n : ℕ) => 1

In particular, is it true that $\epsilon_n = o(1)$?

theorem Erdos688.erdos_688.variants.lglglg_over_lglg_is_big_o : (fun (n : ℕ) => Real.log (Real.log (Real.log ↑n)) / Real.log (Real.log ↑n)) =O[Filter.atTop] epsilonFunction

Erdős claims in [Er80] (p. 106) that it is not difficult to prove $\epsilon_n \gg \frac{\log\log\log n}{\log\log n}$.