Problem 512

../

claims/: The 2 claim pages of Problem 512, one per claimant's result; the problem's standing derives from them.

---

Statement. 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 }$?

Status. 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.

Source. erdosproblems.com/512, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #512, https://www.erdosproblems.com/512.

References.

• [Ko81] Konyagin, S. V., On the Littlewood problem. Izv. Akad. Nauk SSSR Ser. Mat. (1981), 243-265, 463.
• [MPS81] McGehee, O. Carruth and Pigno, Louis and Smith, Brent, Hardy's inequality and the $L\sp{1}$ norm of exponential sums. Ann. of Math. (2) (1981), 613-618.

Formalization. Statement in formal-conjectures, which names as its formal proof the file problems/512/Erdos512.lean of the Jayyhk/erdos-lean repository, a proof produced by Aristotle (Harmonic) from the paper of McGehee, Pigno and Smith, as the thread's one comment reports, and linked at its pinned commit from their claim page; it was not built here, and the "(LEAN)" suffix of the site's label is a catalog label.

Current assessment

The answer is yes. Littlewood's conjecture, that the $L^1$ norm of a sum of $N$ distinct exponentials is at least an absolute constant times $\log N$, was proved independently in 1981 by Konyagin [Ko81] and by McGehee, Pigno and Smith [MPS81]. Both are accepted claims, Konyagin 1981 and McGehee, Pigno and Smith 1981, on refereed publication and the site's credit. Konyagin's paper is filed as a library card; the papers of McGehee, Pigno and Smith are not held, and no proof has been independently reviewed. The Lean proof that the site's label refers to, produced by Aristotle (Harmonic) from the paper of McGehee, Pigno and Smith, is linked from their claim page and has not been built here.

Known Results

• Konyagin [Ko81]: for distinct integers $m_1,\ldots,m_M$, $\int_{-\pi}^{\pi}\lvert\sum_{j}e^{im_jx}\rvert\,\mathrm dx\ge C\log M$, proved in the stronger form of a lower bound on the $L^1$ distance from $F=\sum_ja_je^{in_jx}$ with every $\lvert a_j\rvert\ge1$ to a subspace of trigonometric polynomials, by dyadic averaging projections. This is the accepted claim Konyagin 1981.
• McGehee, Pigno and Smith [MPS81]: the same inequality through a Hardy-type inequality and a dual construction, announced in Bull. Amer. Math. Soc. (N.S.) 5 (1981), 71--72. This is the accepted claim McGehee, Pigno and Smith 1981; the Lean file problems/512/Erdos512.lean of the Jayyhk/erdos-lean repository formalizes this proof and is linked from that page.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

• konyagin_1981_littlewood_problem
• konyagin_1981_littlewood_problem / corollary_1
• konyagin_1981_littlewood_problem / corollary_2
• konyagin_1981_littlewood_problem / theorem