Formalizing Schwartz functions and tempered distributions
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917047814848512 |
|---|---|
| author | Doll, Moritz |
| author_facet | Doll, Moritz |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_24060 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formalizing Schwartz functions and tempered distributions Doll, Moritz Logic in Computer Science Analysis of PDEs 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. |
| title | Formalizing Schwartz functions and tempered distributions |
| topic | Logic in Computer Science Analysis of PDEs |
| url | https://arxiv.org/abs/2510.24060 |