Mechanized Proof of the Orthogonality Relations of the Trigonometric
Functions in ACL2(r) Using Non-Standard Analysis

Cuong Chau
ACL2 Seminar
Feb. 10, 2015

Abstract:

The orthogonality relations of the trigonometric functions sine and cosine
play an important role in Fourier series analysis. For example, they are
often used to determined the Fourier coefficients of periodic functions.
The hand proofs of these relations can easily be found on the Internet.
However, lack of mechanized proofs of these properties limits automatic
theorem provers for reasoning about Fourier series properties. In this talk,
I will show how the Second Fundamental Theorem of Calculus can be applied
to prove the orthogonality relations of sines and cosines in ACL2(r) using
non-standard analysis. Furthermore, the proof procedure can be applied to
compute the definite integral of any real-valued continuous function f
defined on an interval [a, b], even when f contains free variables. I will
discuss three main points in this procedure.

- Finding the antiderivative g of f and proving that f is the derivative of
  g, i.e., g' = f.
- Defining the Riemann integral of f.
- Issues with functional instantiation in the presence of free variables
  when non-classical functions are under consideration, and possible
  solutions.