Skip to content

Erdős problem 950

Start work

This function was considered by de Bruijn, Erdős, and Turán, who showed that ∑n<xf(n)∼∑n<xf(n)2∼x\sum_{n<x}f(n)\sim \sum_{n<x}f(n)^2\sim x. They gave no proofs, but a proof of the (harder) second claim is given by Gorodetsky here [mathoverflow/508491].

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

950.lean

Retained formal statement7 of 7

He notes that if π(x)<π(y)+O(x−ylog⁡x)\pi(x)< \pi(y)+O\left(\frac{x-y}{\log x}\right) for all y<x−(log⁡x)Cy<x-(\log x)^C for some constant C>0C>0 then f(n)≪log⁡log⁡log⁡nf(n)\ll \log\log\log n.

FormalConjectures/ErdosProblems/950.leanErdos950.erdos_950.variants.weaker_pi_implies_f5 linesExact file
(∃ C > 0,    ∃ K > 0,      ∀ᶠ (x : ℕ) in Filter.atTop,        ∀ (y : ℕ), ↑y < ↑x - Real.log ↑x ^ C → ↑x.primeCounting < ↑y.primeCounting + K * ((↑x - ↑y) / Real.log ↑x)) →  Erdos950.f =O[Filter.atTop] fun n => Real.log (Real.log (Real.log ↑n))
SolvedStatement only, no proof