Formalization of Harmonic Analysis in Lean
W. Bosse (TU Delft - Electrical Engineering, Mathematics and Computer Science)
J. Reimann – Mentor (TU Delft - Analysis)
M.P.T. Caspers – Graduation committee member (TU Delft - Analysis)
Y. Murakami – Graduation committee member (TU Delft - Discrete Mathematics and Optimization)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
The formalization of mathematics has become increasingly popular in recent years. Formalization refers to the expression of mathematical definitions and proofs within a precisely defined system of rules, allowing software programs to verify their correctness. This thesis formalizes Schwartz functions using the interactive theorem prover Lean, which provides automation and feedback during the construction of definitions and arguments. Due to their smoothness and rapid decay at infinity, the space of Schwartz functions forms a natural setting for the Fourier transform. While Lean's library already contains an abstract formalization of Schwartz functions, this thesis presents a more concrete, coordinate-based approach that aligns more closely with standard mathematical textbooks. The knowledge gained throughout this thesis can support future formalizations of results in distribution theory, a domain that is still underdeveloped in Lean.