Erdős Problem 1201

Reference: erdosproblems.com/1201

noncomputable def Erdos1201.Erdos1201Set (ε : ℝ) (k : ℕ) : Set ℕ

The set of $n$ for which $P(n(n+1)\cdots(n+k)) > n^{1-\epsilon}$, where $P(m)$ is the greatest prime divisor of $m$.

Equations

• Erdos1201.Erdos1201Set ε k = {n : ℕ | ↑(sSup {p : ℕ | Nat.Prime p ∧ p ∣ ∏ i ∈ Finset.range (k + 1), (n + i)}) > ↑n ^ (1 - ε)}

theorem Erdos1201.erdos_1201 : sorry ↔ ∀ ε > 0, ∀ η > 0, ∃ (k : ℕ), Filter.liminf (fun (x : ℕ) => ↑↑(Nat.count (Erdos1201Set ε k) x) / ↑↑x) Filter.atTop ≥ 1 - η

Is it true that for every $\epsilon,\eta>0$ there exists a $k$ such that the density of $n$ for which $P(n(n+1)\cdots(n+k))>n^{1-\epsilon}$ is at least $1-\eta$ (where $P(m)$ is the greatest prime divisor of $m$)?

theorem Erdos1201.erdos_1201.variants.epsilon_half (η : EReal) : η > 0 → ∃ (k : ℕ), Filter.liminf (fun (x : ℕ) => ↑↑(Nat.count (Erdos1201Set (1 / 2) k) x) / ↑↑x) Filter.atTop ≥ 1 - η

Erdős wrote he could prove this for $\epsilon=1/2$.