Skip to content

Erdős problem 968

Start work

Does the set {n | u n < u (n+1)} have positive lower density?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

968.lean

Retained formal statement5 of 5

Erdős and Prachar proved ∑_{pₙ < x} |u (n+1) - u n| ≍ (log x)^2 (see [ErPr61]).

We encode ∑_{pₙ < x} as a sum over n < Nat.primeCounting' x (the number of primes < x).

FormalConjectures/ErdosProblems/968.leanErdos968.erdos_968.variants.sum_abs_diff_isTheta_log_sq2 linesExact file
(fun x => ∑ n ∈ Finset.Iio x.primeCounting', |Erdos968.u (n + 1) - Erdos968.u n|) =Θ[Filter.atTop] fun x =>  Real.log ↑x ^ 2
SolvedStatement only, no proof