Fourier Series Formalization in ACL2(r)

Cuong K. Chau, Matt Kaufmann, Warren A. Hunt

We formalize some basic properties of Fourier series in the logic of ACL2(r), which is a variant of ACL2 that supports reasoning about the real and complex numbers by way of non-st…