Erdős Problem 961

References:

• erdosproblems.com/961
• [Ju74] Jutila, Matti, On numbers with a large prime factor. {II}. J. Indian Math. Soc. (N.S.) (1974), 125--130.
• RaSh73 Ramachandra, K. and Shorey, T. N., On gaps between numbers with a large prime factor. Acta Arith. (1973), 99--111.

noncomputable def Erdos961.Erdos961Prop (k n : ℕ) : Prop

Equations

• Erdos961.Erdos961Prop k n = ∀ m ≥ k + 1, ∃ i ∈ Set.Ico m (m + n), i ∉ (k + 1).smoothNumbers

theorem Erdos961.erdos_961.sylvester_schur (k : ℕ) (hk : 0 < k) : Erdos961Prop k k

Sylvester and Schur [Er34] proved that every set of $k$ consecutive integers greater than $k$ contains an integer divisible by a prime greater than $k$, i.e. not $(k+1)$-smooth.

theorem Erdos961.erdos_961.sylvester_schur_1_1 : Erdos961Prop 1 1

theorem Erdos961.erdos_961.well_defined (k : ℕ) (hk : 0 < k) : ∃ (n : ℕ), Erdos961Prop k n

noncomputable def Erdos961.f (k : ℕ) : ℕ

For $k$, let $f(k)$ be the minimal $n$ such that every set of $n$ consecutive integers $>k$ contains an integer divisible by a prime $>k$, i.e. not $(k+1)$-smooth.

Equations

• Erdos961.f k = if hk : 0 < k then Nat.find ⋯ else 0

theorem Erdos961.erdos_961 : sorry ↔ ∃ C > 0, ∀ᶠ (k : ℕ) in Filter.atTop, ↑(f k) < Real.log ↑k ^ C

It is conjectured that $f(k) \ll (\log k)^O(1)$.

theorem Erdos961.erdos_961.erdos_upper_bound : ∀ᶠ (k : ℕ) in Filter.atTop, ↑(f k) < 3 * ↑k / Real.log ↑k

Erdos [Er55d] proved $f(k) < 3 \frac{k}{\log k}$ for sufficiently large $k$.

theorem Erdos961.erdos_961.jutila_ramachandra_shorey_upper_bound : (fun (k : ℕ) => ↑(f k)) =O[Filter.atTop] fun (k : ℕ) => Real.log (Real.log (Real.log ↑k)) / Real.log (Real.log ↑k) * (↑k / Real.log ↑k)

Jutila [Ju74], and Ramachandra--Shorey [RaSh73] proved a stronger upper bound $f(k) \ll \frac{\log \log \log k}{\log \log k} \frac{k}{\log k}$.