Problem 512

Is it true that, if $A\subset \mathbb{Z}$ is a finite set of size $N$ , then

\int_0^1 \left\lvert \sum_{n\in A}e(n\theta)\right\rvert \mathrm{d}\theta \gg \log N,

where $e(x)=e^{2\pi ix }$ ?

Source: erdosproblems.com/512

Analysis

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

PROVED (LEAN), the site's label, which credits the independent proofs of Littlewood's conjecture by Konyagin and by McGehee, Pigno and Smith, both refereed; the Lean proof the formal-conjectures statement names is linked from the latter page.

Problem 512

Status

Proof claims

Discussion