Erdős Problem 912

References:

• erdosproblems.com/912
• [Er82c] Erdős, P., Miscellaneous problems in number theory. Congr. Numer. (1982), 25-45.

noncomputable def Erdos912.h (n : ℕ) : ℕ

If $n! = \prod_{i}p_i^{k_i}$ is the factorization into distinct primes, then we define $h(n)$ to be the number of distinct exponents $k_i$.

Equations

• Erdos912.h n = n.factorial.factorization.frange.card

theorem Erdos912.erdos_912.variants.selfridge : (fun (n : ℕ) => ↑(h n)) =Θ[Filter.atTop] fun (n : ℕ) => (↑n / Real.log ↑n) ^ (1 / 2)

Erdős and Selfridge prove in [Er82c] that $h(n) \asymp \left(\frac{n}{\log n}\right)^{1/2}$.

theorem Erdos912.erdos_912 : ∃ c > 0, Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(h n)) fun (n : ℕ) => c * (↑n / Real.log ↑n) ^ (1 / 2)

Prove that there exists some $c>0$ such that $$h(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}$$ as $n\to \infty$.

theorem Erdos912.erdos_912.variants.tao : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(h n)) fun (n : ℕ) => √(2 * Real.pi) * (↑n / Real.log ↑n) ^ (1 / 2)

A heuristic of Tao using the Cramér model for the primes suggests this is true with $c=\sqrt{2\pi}$.