Erdős Problem 390

References:

• erdosproblems.com/390
• [EGS82] Erdős, P., R. K. Guy, and J. L. Selfridge. "Another Property of 239 and some related questions." Congr. Numer. 34 (1982): 243-257.

noncomputable def Erdos390.f (n : ℕ) : ℕ

Let f n be the smallest integer for which n! can be represented as the product of distinct integers greater than n, the largest of which is f n.

Equations

• Erdos390.f n = sInf {m : ℕ | ∃ (k : ℕ) (f : ℕ → ℕ), StrictMono f ∧ n < f 0 ∧ f (k - 1) = m ∧ ∏ i ∈ Finset.Iio k, f i = n.factorial}

theorem Erdos390.erdos_390_theta : (fun (n : ℕ) => ↑(f n) - 2 * ↑n) =Θ[Filter.atTop] fun (n : ℕ) => ↑n / Real.log ↑n

f n - 2 * n = θ (n / log n). This is proved in [EGS82].

theorem Erdos390.erdos_390_equivalent : sorry ↔ ∃ (c : ℝ), Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(f n) - 2 * ↑n) fun (n : ℕ) => c * ↑n / Real.log ↑n

Does there exists a constant c such that f n - 2 * n ~ c * (n / log n)?