Erdős problem 996

Let $n_1<n_2<\cdots$ be a lacunary sequence of integers and $f\in L^2([0,1])$ with $n$ th Fourier partial sum $f_n$ . Is there an absolute constant $C>0$ such that if $\| f-f_n\|_2 \ll (\log\log\log n)^{-C}$ then $\frac{1}{N}\sum_{k\leq N}f(\{\alpha n_k\})\to\int_0^1 f$ for almost every $\alpha$ ? A preprint answers this negatively via a dyadic spike-block counterexample.

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

996.lean

Retained formal statement1 of 2

Does there exists a positive constant C such that for all f ∈ L²[0,1] and all lacunary sequences n, if ‖f - fₖ‖₂ = O(1 / log log log k ^ C), then for almost every x, lim ∑ k ∈ Finset.range N, f (n k • x)) / N = ∫ t, f t ∂t?

FormalConjectures/ErdosProblems/996.leanErdos996.erdos_99611 linesExact file

1sorry ↔2  ∃ C,3    0 < C ∧4      ∀ (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (n : ℕ → ℕ),5        IsLacunary n →6          ((fun k =>7                (MeasureTheory.eLpNorm (Erdos996.fourierPartial f k) 2 AddCircle.haarAddCircle).toReal) =O[Filter.atTop]8              fun k => 1 / Real.log (Real.log (Real.log ↑k)) ^ C) →9            ∀ᵐ (x : AddCircle 1),10              Filter.Tendsto (fun N => (∑ k ∈ Finset.range N, ↑↑f (n k • x)) / ↑N) Filter.atTop11                (nhds (∫ (t : AddCircle 1), ↑↑f t ∂AddCircle.haarAddCircle))

OpenStatement only, no proof