Abstract
This development formalises the square integrable functions over the
reals and the basics of Fourier series. It culminates with a proof
that every well-behaved periodic function can be approximated by a
Fourier series. The material is ported from HOL Light:
https://github.com/jrh13/hol-light/blob/master/100/fourier.ml