Formalizing Schwartz functions and tempered distributions

TL;DR

This paper presents the first formalization of tempered distributions in the Lean proof assistant, including key theorems like the Fourier transform extension and Sobolev spaces, advancing formalized analysis.

Contribution

It introduces the first formalization of tempered distributions in a proof assistant, bridging distribution theory and formal verification.

Findings

Fourier transform extends to a linear isometry on L^2

Sobolev spaces are defined via Fourier transform on tempered distributions

First formalization of distribution theory in Lean

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.