REVIEW 3 cited by
A blueprint for the formalization of Carleson's theorem on convergence of Fourier series
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
This paper is the blueprint underlying the Lean formalization of the proof of Carleson's classical result asserting almost everywhere convergence of Fourier series of continuous functions. We break up the proof into two steps, a reduction of the classical result to a new theorem that appears in a sibling communication and a proof of this new theorem, which is also detailed as blueprint in this paper. An early version of this blueprint was used to initiate the Lean formalization. During the formalization, many contributors elaborated the blueprint with minor corrections, modifications and extensions. The final version is presented here as a guide through the accompanying Lean code.
Forward citations
Cited by 3 Pith papers
-
The Bilinear Hilbert-Carleson operator along curves. The purely non-zero curvature case
The Bilinear Hilbert-Carleson operator along the moment curve (t, t^2, t^3) satisfies the expected L^{p1} x L^{p2} to L^r bounds for 1 < p1, p2 < infinity and 1/2 < r < infinity.
-
A Formalization of the Mean-Field Derivation of the Vlasov Equation
A mathematician directing an AI completed an axiom-clean Lean 4 formalization of Dobrushin's mean-field derivation of the Vlasov equation, including well-posedness, stability, a conditional mean-field limit, and a sho...
-
Quantitative Polynomial Wiener-Wintner Theorems
Polynomial-phase ergodic and singular-integral averages on homogeneous Lie groups satisfy uniform r-variation bounds for every r>2.
Discussion (0). Continue with ORCID to comment.