Skip to content

Erdős problem 145

Let s1<s2<s_1 < s_2 < \cdots be the sequence of squarefree numbers. Is it true that, for any α0\alpha\geq 0, limx1xsnx(sn+1sn)α \lim_{x\to\infty} \frac{1}{x}\sum_{s_n\leq x}(s_{n+1}-s_n)^\alpha exists?

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

145.lean

Retained formal statement1 of 4

Let s1<s2<s_1 < s_2 < \cdots be the sequence of squarefree numbers. Is it true that, for any α0\alpha\geq 0, limx1xsnx(sn+1sn)α \lim_{x\to\infty} \frac{1}{x}\sum_{s_n\leq x}(s_{n+1}-s_n)^\alpha exists?

FormalConjectures/ErdosProblems/145.leanErdos145.erdos_1455 linesExact file
True  ∀ α ≥ 0,    ∃ β,      Filter.Tendsto (fun x => 1 / x * ∑ nErdos145.A x, (↑(Erdos145.s (n + 1)) - ↑(Erdos145.s n)) ^ α) Filter.atTop        (nhds β)
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page