Fourier series

Abstract: Fourier series are not new to formalization; various results were proved by Harrison in HOL Light ten years ago, and there are developments in Isabelle and Metamath too. But the Hilbert space theory and measure theory in Lean's library mathlib allows for a very efficient presentation. I will give a tour of some of this theory, touching on topological groups, the Stone-Weierstrass theorem, the denseness of continuous functions in Lp, and a TFAE for Hilbert bases.

general mathematicsnumber theory

Audience: advanced learners

London Learning Lean

Series comments: This is a seminar on formalising research level, MSc, or advanced undergraduate level mathematics in the Lean theorem prover. It is suitable for people who have some mathematical background, e.g. MSc students in a mathematics department. Speakers will assume some familiarity with the Lean but you certainly don't have to be a Lean expert

Speakers are told to spend 50 percent of their time explaining the mathematics, and 50 percent on the Lean implementation.

Past seminars are available on the YouTube playlist here www.youtube.com/watch?v=UykGFDVfQNA&list=PLVZep5wTamMmqv34JnrNC2AgjfPoh_LN8

The seminar series is hybrid/online -- it will meet in person at Imperial College in room Huxley 410, and will also be live streamed on Zoom.