Erdős Problem 419

References:

• erdosproblems.com/419
• [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
• [EGIP96] Erdős, Paul and Graham, S. W. and Ivić, Aleksandar and Pomerance, Carl, On the number of divisors of $n!$. (1996), 337--355.

noncomputable def Erdos419.factorialDivisorRatio (n : ℕ) : ℝ

The ratio $\sigma_0((n+1)!)/\sigma_0(n!)$, where $\sigma_0$ is the divisor-counting function.

Equations

• Erdos419.factorialDivisorRatio n = ↑((ArithmeticFunction.sigma 0) (n + 1).factorial) / ↑((ArithmeticFunction.sigma 0) n.factorial)

def Erdos419.limitPointSet : Set ℝ

The set $\{1\} \cup \{1+1/k : k \geq 1\}$.

Equations

• Erdos419.limitPointSet = {1} ∪ {x : ℝ | ∃ (k : ℕ), 1 ≤ k ∧ x = 1 + 1 / ↑k}

theorem Erdos419.erdos_419 : {x : ℝ | MapClusterPt x Filter.atTop factorialDivisorRatio} = limitPointSet

If $\tau(n)$ counts the number of divisors of $n$, then what is the set of limit points of [ \frac{\tau((n+1)!)}{\tau(n!)}? ]

The limit points are exactly $\{1\} \cup \{1+1/k : k \geq 1\}$.