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.

@[reducible, inline]

abbrev Erdos945.τ (n : ℕ) : ℕ

Equations

• Erdos945.τ n = n.divisors.card

noncomputable def Erdos945.F (x : ℝ) : ℕ

Let $F(x)$ be the maximal $k$ such that there exist $n+1, \dots, n+k \le x$ with $τ(n+1), \dots, τ(n+k)$ all distinct, where $τ(m)$ counts the divisors of $m$.

Equations

• Erdos945.F x = sSup {k : ℕ | ∃ (n : ℕ), ↑n + ↑k ≤ x ∧ Set.InjOn Erdos945.τ (Set.Ioc n (n + k))}

def Erdos945.Erdos945 : Prop

Equations

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

theorem Erdos945.erdos_945 : Erdos945 ↔ sorry

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

def Erdos945.Erdos945Constant : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos945.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 Erdos945.erdos_945.equivalence : Erdos945 ↔ Erdos945Constant

The two ways of phrasing the conjecture are equivalent.

theorem Erdos945.erdos_945.variants.lower_bound : (fun (x : ℕ) => √(Real.log ↑x) / Real.log (Real.log ↑x)) ≪ fun (n : ℕ) => ↑(F ↑n)

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

theorem Erdos945.erdos_945.variants.upper_bound : (fun (n : ℕ) => Real.log ↑(F ↑n)) ≪ fun (x : ℕ) => √(Real.log ↑x) / Real.log (Real.log ↑x)

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