  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.
