Erdős Problem #995

The question

Erdős Problem 995:

For every lacunary sequence $(n_k)$ of integers and every $f\in L^2([0,1])$ with ${\int }_0^{1}f=0$, is it true that for almost all $\alpha$, $$\sum _{k<N}f(\{\alpha n_k\})=o\left(N\sqrt{\log \log N}\right)?$$

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«995». answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem erdos_995 :
    answer(sorry) ↔
      ∀ (n : ℕ → ℕ), IsLacunary n → ∀ (f : ℝ → ℝ),
        MemLp f 2 (volume.restrict (Icc (0 : ℝ) 1)) →
        ∫ x in (0 : ℝ)..1, f x = 0 →
        ∀ᵐ α ∂(volume.restrict (Icc (0 : ℝ) 1)),
          partialSum n f α =o[atTop] fun N => (N : ℝ) * Real.sqrt (Real.log (Real.log N))

What counts as progress

• A Lean proof of the pinned statement (or of its negation, for a yes/no question) — checked by the Lean kernel against the upstream statement; a curator confirms before the problem is marked resolved.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already — check erdosproblems.com/995. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• erdosproblems.com/995
• [Er49] Erdős, P., On the strong law of large numbers, Trans. Amer. Math. Soc. (1949), 329-334.

Let $n_1<n_2<\cdots$ be a lacunary sequence of integers and $f\in L^2([0,1])$ with ${\int }_0^{1}f=0$. Estimate the growth of $$S_N(\alpha )=\sum _{k\le N}f(\{\alpha n_k\})$$ for almost all $\alpha$, where $\{\cdot \}$ denotes the fractional part. In particular, is it true that $S_N(\alpha )=o\left(N\sqrt{\log \log N}\right)$ for almost all $\alpha$?

Erdős [Er49] constructed a lacunary sequence and a mean-zero $f\in L^2([0,1])$ for which, for every $\epsilon >0$, ${\mathrm{limsup}}_N{S}_N(\alpha )/(N(\log \log N{)}^{1/2-\epsilon })=\infty$ for almost all $\alpha$, and believed this lower bound to be close to the truth.

The mean-zero hypothesis ${\int }_0^{1}f=0$ is the natural normalisation: otherwise the sum has a linear main term coming from the average of $f$.

Source and licence

Imported from Formal Conjectures (Erdős problems), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.