Problem 255

Let $z_1,z_2,\ldots \in [0,1]$ be an infinite sequence, and define the discrepancy

D_N(I) = \#\{ n\leq N : z_n\in I\} - N\lvert I\rvert.

Must there exist some interval $I\subseteq [0,1]$ such that

\limsup_{N\to \infty}\lvert D_N(I)\rvert =\infty?

Source: erdosproblems.com/255

Discrepancy

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

PROVED (LEAN): Schmidt's 1968 theorem, refereed in the Quarterly Journal of Mathematics, answers yes; see the claim page (schmidt, 1968), which also links the unbuilt public Lean file that the site's Lean qualifier most likely refers to.

Problem 255

Status

Proof claims

Discussion