Formalizing Schwartz functions and tempered distributions
Moritz Doll
TL;DR
The article advances the formalization of distribution theory in the Lean proof assistant by constructing tempered distributions as the topological dual of the Schwartz space $\mathscr{S}(\mathbb{R}^d)$ and by developing a robust framework for vector-valued, locally convex spaces. It defines $\mathscr{S}$ with a seminorm-based topology, provides a general method (mkCLM) for constructing continuous linear maps on $\mathscr{S}$, and extends the Fourier transform to tempered distributions via duality, all within Lean's type-theoretic setting. A key contribution is proving that the Fourier transform is an isometry on $L^2$ by first establishing Plancherel on $\mathscr{S}$ and density of $\mathscr{S}$ in $L^p$, and then formulating Sobolev spaces via Fourier multipliers with $\Lambda_s=\mathcal{F}^{-1}\langle\xi\rangle^s\mathcal{F}$ and $H^s(\mathbb{R}^d)=\{u\in \mathscr{S}'(\mathbb{R}^d): \Lambda_s u\in L^2\}$. This work provides a principled, PDE-friendly backbone for formalized analysis, while noting current limits in handling nontrivial PDE results and the preference for abstract Fourier-analytic methods over direct $L^p$-space computations.
Abstract
Distribution theory is a cornerstone of the theory of partial differential equations. We report on the progress of formalizing the theory of tempered distributions in the interactive proof assistant Lean, which is the first formalization in any proof assistant. We give an overview of the mathematical theory and highlight key aspects of the formalization that differ from the classical presentation. As an application, we prove that the Fourier transform extends to a linear isometry on $L^2$ and we define Sobolev spaces via the Fourier transform on tempered distributions.