Erdős Problem 945

References:

• erdosproblems.com/945
• [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.

def Erdos945 : Prop

Equations

• Erdos945 = ∃ (O : ℝ → ℝ), O =O[Filter.atTop] 1 ∧ ∀ᶠ (x : ℝ) in Filter.atTop, ↑(F✝ x) ≤ Real.log x ^ O x

theorem erdos_945 : Erdos945 ↔ sorry

Is it true that $F(x) \leq (\log x)^{O(1)}$?

def Erdos945Constant : Prop

Equations

• Erdos945Constant = ∃ C > 0, ∀ᶠ (x : ℝ) in Filter.atTop, ∃ (a : ℕ) (b : ℕ), a ≠ b ∧ ↑a ∈ Set.Icc x (x + Real.log x ^ C) ∧ ↑b ∈ Set.Icc x (x + Real.log x ^ C) ∧ τ✝ a = τ✝ b

theorem erdos_945.variants.constant : Erdos945Constant ↔ sorry

Is there a constant $C > 0$ such that, for all large $x$, every interval $[x, x+(\log x)C]$ contains two integers with the same number of divisors?

theorem erdos_945.equivalence : Erdos945 ↔ Erdos945Constant

The two ways of phrasing the conjecture are equivalent.

theorem erdos_945.variants.lower_bound : (fun (x : ℕ) => √(Real.log ↑x) / Real.log (Real.log ↑x)) =O[Filter.atTop] fun (n : ℕ) => ↑(F✝ ↑n)

Erdős and Mirsky [ErMi52] proved that $\frac{(\log x)^{1/2}}{\log\log x}\ll F(x)$.

theorem erdos_945.variants.upper_bound : (fun (n : ℕ) => Real.log ↑(F✝ ↑n)) =O[Filter.atTop] fun (x : ℕ) => √(Real.log ↑x) / Real.log (Real.log ↑x)

Erdős and Mirsky [ErMi52] proved that $\log F(x) << \frac{(\log x)^{1/2}}$.