Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Fourier Series

Email Gateway (Aug 22 2022 at 20:32):

From: Tobias Nipkow <nipkow@in.tum.de>
Fourier Series
Lawrence C Paulson

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

https://www.isa-afp.org/entries/Fourier.html

Enjoy!
smime.p7s

Last updated: Apr 26 2024 at 01:06 UTC