Erdős Problem 394

References:

• erdosproblems.com/394
• [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
• [ErHa78] Erdős, P. and Hall, R. R., On some unconventional problems on the divisors of integers. J. Austral. Math. Soc. Ser. A (1978), 479--485.

noncomputable def Erdos394.t (k n : ℕ) : ℕ

Let $t_k(n)$ denote the least $m$ such that $n\mid m(m+1)(m+2)\cdots (m+k-1).$

Equations

• Erdos394.t k n = sInf {m : ℕ | 0 < m ∧ n ∣ ∏ i ∈ Finset.range k, (m + i)}

theorem Erdos394.erdos_394_part_a : sorry ↔ ∃ c > 0, (fun (x : ℕ) => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(t 2 n)) =O[Filter.atTop] fun (x : ℕ) => ↑x ^ 2 / Real.log ↑x ^ c

Is it true that $\sum_{n\leq x}t_2(n)\ll \frac{x^2}{(\log x)^c}$ for some $c>0$?

theorem Erdos394.erdos_394_part_b : sorry ↔ ∀ k ≥ 2, (fun (x : ℝ) => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(t (k + 1) n)) =o[Filter.atTop] fun (x : ℝ) => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(t k n)

Is it true that, for $k\geq 2$, $\sum_{n\leq x}t_{k+1}(n) =o\left(\sum_{n\leq x}t_k(n)\right)?$

theorem Erdos394.erdos_394_hall_bound : (fun (x : ℕ) => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(t 2 n)) =O[Filter.atTop] fun (x : ℕ) => ↑x ^ 2 * (Real.log (Real.log (Real.log ↑x)) / Real.log (Real.log ↑x))

In [ErGr80] they mention a conjecture of Erdős that the sum is $o(x^2)$. This was proved by Erdős and Hall [ErHa78], who proved that in fact $\sum_{n\leq x}t_2(n)\ll \frac{\log\log\log x}{\log\log x}x^2.$

theorem Erdos394.erdos_394_hall_conjecture (c : ℝ) : c < Real.log 2 → (fun (x : ℝ) => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(t 2 n)) =o[Filter.atTop] fun (x : ℝ) => x ^ 2 / Real.log x ^ c

Erdős and Hall conjecture that the sum is $o(x^2/(\log x)^c)$ for any $c<\log 2$.

theorem Erdos394.erdos_394_lower_bound : (fun (x : ℕ) => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(t 2 n)) =O[Filter.atTop] fun (x : ℕ) => ↑x ^ 2 / Real.log ↑x

Since $t_2(p)=p-1$ for prime $p$ it is trivial that $\sum_{n\leq x}t_2(n)\gg \frac{x^2}{\log x}$.

theorem Erdos394.erdos_394_factorial_gap_conjecture : sorry ↔ {n : ℕ | ∀ (k : ℕ), 2 ≤ k → k < n → t k n.factorial < t (k - 1) n.factorial - 1}.Infinite

They ask about the behaviour of $t_{n-3}(n!)$ and also ask whether, for infinitely many $n$, $t_k(n!)< t_{k-1}(n!)-1$ for all $1\leq k < n$.

theorem Erdos394.erdos_394_factorial_gap_10 (k : ℕ) : 2 ≤ k → k < 10 → t k (Nat.factorial 10) < t (k - 1) (Nat.factorial 10) - 1

They proved (with Selfridge) that this holds for $n=10$.