∑math20

Real and complex analysis · Result 075

The \(L\log L\) Fourier-convergence conjecture

1 paperLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Almost-everywhere Fourier convergence in L log L

Almost-everywhere Fourier convergence in L log L

OpenAI · September 23, 2026

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.

Read PDF Download Source

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}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The \(L\log L\) Fourier-convergence conjecture asks whether ordinary symmetric Fourier partial sums converge almost everywhere at this integrability scale. The formalization proves this for every measurable complex-valued function on \(\mathbb T=\mathbb R/(2\pi\mathbb Z)\) satisfying \(\int_{\mathbb T}|f|\log(2+|f|)<\infty\). Outside one measurable null set, \(\sum_{k=-N}^{N}\widehat f(k)e^{ikx}\to f(x)\) along the full sequence \(N\to\infty\).

Comparator links

ResultComparator statement
Almost-everywhere convergence of full symmetric Fourier partial sumsFourierLLogL.lean

Scope note on GitHub →