Fourier Series Formalization in ACL2(r)

Cuong K. Chau
(The University of Texas at Austin)
Matt Kaufmann
(The University of Texas at Austin)
Warren A. Hunt Jr.
(The University of Texas at Austin)

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-standard analysis. More specifically, we extend a framework for formally evaluating definite integrals of real-valued, continuous functions using the Second Fundamental Theorem of Calculus. Our extended framework is also applied to functions containing free arguments. Using this framework, we are able to prove the orthogonality relationships between trigonometric functions, which are the essential properties in Fourier series analysis. The sum rule for definite integrals of indexed sums is also formalized by applying the extended framework along with the First Fundamental Theorem of Calculus and the sum rule for differentiation. The Fourier coefficient formulas of periodic functions are then formalized from the orthogonality relations and the sum rule for integration. Consequently, the uniqueness of Fourier sums is a straightforward corollary.

We also present our formalization of the sum rule for definite integrals of infinite series in ACL2(r). Part of this task is to prove the Dini Uniform Convergence Theorem and the continuity of a limit function under certain conditions. A key technique in our proofs of these theorems is to apply the overspill principle from non-standard analysis.

In Matt Kaufmann and David L. Rager: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2015), Austin, Texas, USA, 1-2 October 2015, Electronic Proceedings in Theoretical Computer Science 192, pp. 35–51.
Published: 18th September 2015.

ArXived at: bibtex PDF

Comments and questions to:
For website issues: