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: London Learning Lean is an in-person informal seminar where people in the Lean community give 10-minute presentations on things they're doing with the Lean theorem prover. It runs on the last Friday of the month, typically either at Imperial College or UCL. Please contact Kevin Buzzard on the Lean Zulip if you want to reserve a slot for a ten-minute presentation!