Browse › Real and complex analysis › 075 The $L\log L$ Fourier-convergence conjecture
Almost-everywhere Fourier convergence in L log L
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove that the ordinary symmetric Fourier partial sums of every complex-valued function in $L\log L$ on the circle converge almost everywhere to the function along the full sequence. This establishes the classical $L\log L$ sufficiency conjecture.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI math release, Lean scope notes for family 075: The L log L Fourier-convergence conjecture (lean/docs/075.md, release of 2026-10-06). Release scope note: the formalization covers almost-everywhere convergence of the full symmetric partial sums for measurable complex $f$ on $\mathbb R/2\pi\mathbb Z$ with $\int|f|\log(2+|f|)<\infty$, and links the comparator statement. [family-level]
- OpenAI, FourierLLogL.lean (Comparator challenge) (openai/math, Lean 4 over Mathlib). Comparator statement
paperMainfor Theorem 1.1, with the proof left assorryand only Mathlib imported; the weak-$L^1$ maximal corollary is not stated.
Possibly relevant literature (found by the agent, not checked)
- Victor Lie, The pointwise convergence of Fourier Series (II). Strong $L^1$ case for the lacunary Carleson operator (arXiv:1902.03630, 2019). Proves that the lacunary Carleson operator is bounded from $L\log L$ to $L^1$, the lacunary-subsequence counterpart of the full-sequence $L\log L$ statement in Theorem 1.1; the paper cites only Lie's 2013 and 2017 papers.
- Francesco Di Plinio, Lacunary Fourier and Walsh-Fourier series near $L^1$ (arXiv:1304.3943, 2013; Collect. Math.). Gives lacunary a.e. convergence in $L\log\log L\log\log\log L$ and weak-$L^p$ bounds for the Walsh–Carleson operator, relevant to the near-$L^1$ convergence spaces surveyed in the paper's introduction.
- Michael Lacey, Carleson's Theorem: Proof, Complements, Variations (arXiv:math/0307008, 2003; revised 2005; Publ. Mat. 48 (2004), 251–307). This exposition of the Lacey–Thiele proof and its $L^p$ extensions provides background for the manuscript's claimed extension of almost-everywhere Fourier convergence to the $L\log L$ endpoint.
- Sergey Konyagin, Almost everywhere convergence and divergence of Fourier series (Proc. ICM 2006, EMS 2007, pp. 1393–1403). A survey of open problems on a.e. convergence and divergence of trigonometric Fourier series, giving context for the sufficiency question that Theorem 1.1 addresses.
- Lars Becker et al., Formalizing Carleson's Theorem in Lean (arXiv:2609.31334, 2026-09-25). An independent Lean formalization of Carleson's theorem, the $L^2$ result that the paper's introduction takes as its starting point, possibly relevant to a full formal proof of the comparator statement.
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 075
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:Almost-everywhere-Fourier-convergence-in-L-log-L-September-23-2026,
author = {{OpenAI}},
title = {{Almost-everywhere Fourier convergence in $L\log L$}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/Almost-everywhere-Fourier-convergence-in-L-log-L-September-23-2026/paper.pdf}{OAI:Almost-everywhere-Fourier-convergence-in-L-log-L-September-23-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/075.md. The Lean statements have not been checked by people against the paper's claims.
Family 075: The $L\log L$ Fourier-convergence conjecture
Proves that the ordinary symmetric Fourier partial sums of every complex-valued function in $L\log L(\mathbb T)$ converge almost everywhere along the full sequence. This resolves the classical sufficiency conjecture at the $L\log L$ scale.
This is the only paper in this family.