Fourier Series

Lawrence C. Paulson 🌐

September 6, 2019

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

License

BSD License

Topics

Session Fourier

Depends on