Skip to content

Erdős problem 394

Start work

For the least tk(n)t_k(n) with n∣tk(n)(tk(n)+1)⋯(tk(n)+k−1)n \mid t_k(n)(t_k(n)+1)\cdots(t_k(n)+k-1), do the conjectured logarithmic-saving and adjacent-length estimates hold on average? Both answered affirmatively, with c=1/2048c = 1/2048 admissible in the t2t_2 bound.

Sources

The source's own material, retained exactly.

10 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

394.lean

Retained formal statement5 of 9

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

FormalConjectures/ErdosProblems/394.leanErdos394.erdos_394.variants.hall_bound2 linesExact file
(fun x => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(Erdos394.t 2 n)) =O[Filter.atTop] fun x =>  ↑x ^ 2 * (Real.log (Real.log (Real.log ↑x)) / Real.log (Real.log ↑x))
SolvedStatement only, no proof