Erdős Problem 946

References:

• erdosproblems.com/946
• [ErMi52] Erdős, P. and Mirsky, L., The distribution of values of the divisor function {$d(n)$}. Proc. London Math. Soc. (3) (1952), 257--271.
• [Sp81] Spiro, C. A., The frequency with which an integral-valued, prime-independent, multiplicative or additive function of n divides a polynomial function of n.
• [He84] Heath-Brown, D. R., The divisor function at consecutive integers. Mathematika 31 (1984), no. 2, 141--149.
• [Hi85] Hildebrand, A., The divisor function at consecutive integers. Pacific J. Math. (1987), 307--319
• [EPS87] Erdős, P., Pomerance, C., and Sarkőzy, A., On locally repeated values of arithmetic functions. III. Proc. Amer. Math. Soc. (1987), 1--7.

theorem Erdos946.erdos_946 : {n : ℕ | (ArithmeticFunction.sigma 0) n = (ArithmeticFunction.sigma 0) (n + 1)}.Infinite

There are infinitely many $n$ such that $τ(n) = τ(n+1)$. Proved in [He84]. Here τ is the divisor counting function, which is σ 0 in mathlib.

theorem Erdos946.erdos_946.variants.spiro_5040 : {n : ℕ | (ArithmeticFunction.sigma 0) n = (ArithmeticFunction.sigma 0) (n + 5040)}.Infinite

There are infinitely many $n$ such that $τ(n) = τ(n + 5040)$. Proved in [Sp81].

noncomputable def Erdos946.erdos946Count (x : ℝ) : ℝ

Number of $n \le x$ with $τ(n) = τ(n+1)$.

Equations

• Erdos946.erdos946Count x = ↑(Finset.filter (fun (n : ℕ) => (ArithmeticFunction.sigma 0) n = (ArithmeticFunction.sigma 0) (n + 1)) (Finset.range (⌊x⌋₊ + 1))).card

theorem Erdos946.erdos_946.variants.heathbrown_lower_bound : (fun (x : ℝ) => x / Real.log x ^ 7) =O[Filter.atTop] erdos946Count

The number of $n \le x$ with $τ(n) = τ(n+1)$ is at least $x / (\log x)^7$ for all sufficiently large $x$. Proved in [He84].

theorem Erdos946.erdos_946.variants.hildebrand_lower_bound : (fun (x : ℝ) => x / Real.log (Real.log x) ^ 3) =O[Filter.atTop] erdos946Count

Improved lower bound in [Hi85]: $Ω(x / (\log \log x)^3)$.

theorem Erdos946.erdos_946.variants.upper_bound : erdos946Count =O[Filter.atTop] fun (x : ℝ) => x / √(Real.log (Real.log x))

Upper bound in [EPS87]: $O(x / \sqrt{\log \log x})$.