Erdős problem 997

Is it true that, for every $\alpha$ , the sequence $\{ \alpha p_n\}$ is not well-distributed, if $p_n$ is the sequence of primes?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

997.lean

Retained formal statement3 of 3

Erdős proved that, if $n_k$ is a lacunary sequence, then the sequence $\{ \alpha n_k\}$ is not well-distributed for almost all $\alpha$ .

FormalConjectures/ErdosProblems/997.leanErdos997.erdos_997.variants.lacunary1 lineExact file

1∀ (n : ℕ → ℕ), IsLacunary n → ∀ᵐ (α : ℝ), ¬Erdos997.IsWellDistributed fun k => Int.fract (α * ↑(n k))

SolvedStatement only, no proof