Fourier series formalization in acl2(r)

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 this paper, we present our efforts in formalizing 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 via non-standard analysis [8, 12]. In particular, we describe our formalization of the Fourier coefficient formulas for periodic functions and the sum rule for definite integrals of infinite series. The formalization of Fourier series will enable interactive theorem provers to reason about systems modeled by Fourier series, with applications to a wide variety of problems in mathematics, physics, electrical engineering, signal processing, and image processing. We do not claim to be developing new mathematics. However, as far as we know the mechanized formalizations and proofs presented in this paper are new. The research contributions of this paper are twofold: a demonstration that a mechanized proof assistant, in particular ACL2(r), can be used to verify properties of Fourier series; and infrastructure to support that activity, which we expect to be reusable for future ACL2(r) verifications of continuous mathematics. Our formalizations presented in the paper assume that there exists a Fourier series, i.e., a (possibly infinite) sum of sines and cosines for any periodic function. Future work could include proving convergence of the Fourier series for any suitable periodic function. The proofs of Fourier coefficient formulas depend on the orthogonality relationships between trigonometric functions and the sum rule for integration of indexed sums. A key tool for proving these properties is the Second Fundamental Theorem of Calculus (FTC-2). Cowles and Gamboa [5] implemented a framework for formally evaluating definite integrals of real-valued continuous functions using FTC-2.