F. van Doorn on Formalizing a proof of Carleson's theorem in HoTTEST, October 10, 11:30 Eastern time

[Chris Kapulkin]

Folks,

This week in HoTTEST, we are excited to have one of the heavy weights
of the formalization enterprise, Floris van Doorn. The title and
abstract of his talk can be found below.

The 60-minute talk will start at 11:30 Eastern and will be followed by
up to 30 minutes of discussion. (If you're into pretending that the
universal time is helpful for anything, then 11:30 Eastern translates
to 15:30 UTC.) The Zoom link is

https://zoom.us/j/994874377

More information about this and other talks, along with videos and
slides from previous talks can be found at

https://www.math.uwo.ca/faculty/kapulkin/seminars/hottest.html

I'm looking forward to seeing many of you in Floris's talk later this week!

Best,
Chris

*

Floris van Doorn
University of Bonn

Formalizing a proof of Carleson's theorem

A fundamental question in Fourier analysis is the Fourier inversion
theorem, which states that for nice functions, applying the Fourier
transform twice gives the original function back up to reversal. This
is true for continuously differentiable functions, but the situation
is a lot more subtle for e.g. continuous functions. In this case the
Fourier transform might not be integrable, and one has to consider
improper integrals. Moreover, this improper integral need not converge
at every point, but in 1966 Lennart Carleson proved that it does
converge at almost all points for functions on the real line. This
result follows from the boundedness of the Carleson operator.
Carleson's proof is famously hard to read, and there are no known easy
proofs of this theorem.

We have proven a generalization of the boundedness of the Carleson's
operator in the setting of doubling metric measure spaces, and we are
currently working on formalizing the entire proof in the proof
assistant Lean, based on a detailed blueprint we wrote first. This
advanced formalization is possible because of Lean's large
mathematical library Mathlib.

In this talk I will give an overview of the project including its
practical aspects, as well as highlighting some other exciting
projects around Mathlib. No background in Fourier analysis is assumed.

This is joint work with Lars Becker, Leo Diedering, Asgar Jamneshan,
Rajula Srivastava, Jeremy Tan, Christoph Thiele and others.