Fourier Series

Lawrence C. Paulson 🌐

September 6, 2019

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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

Cite

× 
@article{Fourier-AFP,
  author  = {Lawrence C. Paulson},
  title   = {Fourier Series},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2019},
  note    = {\url{https://isa-afp.org/entries/Fourier.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: