Fourier Coefficient Formalization in ACL2(r)

Cuong Chau
ACL2 Seminar
Apr. 14, 2015

Abstract:

Fourier coefficient formalization is a natural follow-on to the
orthogonality relations of trigonometric functions in Fourier analysis. As
a part of this formalization, we first need to prove the sum rule for
definite integration for finitely indexed sums. This can be done using the
Second Fundamental Theorem of Calculus (FTC-2) proof procedure as described
in my previous talk and the sum rule for differentiation. Then, we are
finally able to formalize the Fourier coefficients of periodic functions
from the orthogonality relations and the sum rule for integration.
Consequently, the uniqueness of Fourier sums is a straightforward corollary.

In this talk, I also propose a technique for dealing with functional
instantiation of non-classical theorems when instantiated classical
functions contain free variables. The final part of the talk describes my
ongoing work to address challenges in formalizing the definite integral of
an infinite series in ACL2(r). Part of this task is to prove the Dini
Uniform Convergence Theorem, where pointwise convergence of a sequence of
functions implies its uniform convergence under some conditions.