Distribution theory is foundational for partial differential equations, yet the theory of tempered distributions has never been formalized in any proof assistant.

The authors formalize tempered distributions in the Lean proof assistant using Mathlib. They develop the theory of Schwartz functions as a Frechet space with a family of seminorms, formalize the locally convex topology, and define tempered distributions as continuous linear functionals on Schwartz space. Key formalization choices diverge from classical presentations to accommodate Lean's type theory, including using seminorm families rather than abstract locally convex definitions.

As applications, they prove that the Fourier transform extends to a linear isometry on L^2 (Plancherel's theorem) and define Sobolev spaces via the Fourier transform on tempered distributions. This constitutes the first formalization of tempered distribution theory in any proof assistant.