Erdős Problem 1203

References:

• erdosproblems.com/1203

noncomputable def Erdos1203.F (n : ℕ) : ℝ

If $\omega(n)$ counts the number of distinct prime divisors of $n$ then let $F(n)=\max_k \omega(n+k)\frac{\log\log k}{\log k}.$

Equations

• Erdos1203.F n = ⨆ (k : ℕ), ↑(ArithmeticFunction.cardDistinctFactors (n + k)) * (Real.log (Real.log ↑k) / Real.log ↑k)

theorem Erdos1203.erdos_1203 : True ↔ Filter.Tendsto F Filter.atTop Filter.atTop

Prove that $F(n)\to \infty$ as $n\to \infty$.

theorem Erdos1203.erdos_1203.variants.lower_bound (ε : ℝ) : ε > 0 → ∀ᶠ (n : ℕ) in Filter.atTop, F n ≥ 1 - ε

It is easy to prove that $F(n)\geq 1-o(1)$.