Let $n_{1} < n_{2} < \dots$ be a lacunary sequence of integers, and let $f \in L^{2} ([0, 1])$ . Let $f_{n}$ be the $n$ th partial sum of the Fourier series of $f (x)$ . Is there an absolute constant $C > 0$ such that, if $∥ f - f_{n} ∥_{2} ≪ \frac{1}{( lo g lo g lo g n ) ^{C}}$ then $N \to \infty lim \frac{1}{N} k \leq N \sum f ({α n_{k}}) = \int_{0}^{1} f (x) d x$ for almost every $α$ ?

Worked, still open.

analysis · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

Erdős posed essentially this question in his 1964 paper and wrote that he *expected* one might be able to replace a (log log)-type hypothesis by a **(log log log)**-type hypothesis, but he “was not able to decide this.” ([Numdam][1])

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 42 · open (literature)

theorem erdos_996 : answer(sorry) ↔
    ∃ (C : ℝ), 0 < C ∧ ∀ (f : Lp ℂ 2 (haarAddCircle (T := 1))) (n : ℕ → ℕ),
    IsLacunary n →
    (fun k => (eLpNorm (fourierPartial f k) 2 (haarAddCircle (T := 1))).toReal) =O[atTop]
    (fun k => 1 / (log (log (log k))) ^ C)
    →
    ∀ᵐ x, Tendsto (fun N => (∑ k ∈ .range N, f (n k • x)) / N) atTop
    (𝓝 (∫ t, f t ∂haarAddCircle))

formal-conjectures/996.lean ↗

status

open

evidence

formal

status

Search Vela