feat(analysis/schwartz): Definition of the Schwartz space (#15850)

This PR adds the definition of the Schwartz space and by abstract results also of tempered distributions. We prove basic algebraic and topological properties of the Schwartz space. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
leanprover-community · Sep 8, 2022 · 4c0aa6e · 4c0aa6e
1 parent 9b6eef6
commit 4c0aa6e
Show file tree

Hide file tree

Showing 3 changed files with 387 additions and 1 deletion.
diff --git a/docs/overview.yaml b/docs/overview.yaml
@@ -343,6 +343,9 @@ Analysis:
     Phragmen-Lindelöf principle: 'phragmen_lindelof.horizontal_strip'
     fundamental theorem of algebra: 'complex.is_alg_closed'
 
+  Distribution theory:
+    Schwartz space: 'schwartz_map'
+
 Probability Theory:
   Definitions in probability theory:
     probability measure: 'measure_theory.is_probability_measure'

diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
@@ -592,7 +592,7 @@ Distribution calculus:
     convergence of sequences of distributions: ''
     support of a distribution: ''
   Spaces $\mathcal{S}(\R^d)$:
-    Schwartz space of rapidly decreasing functions: ''
+    Schwartz space of rapidly decreasing functions: 'schwartz_map'
     stability by derivation: ''
     stability by multiplication by a slowly growing smooth function: ''
     gaussian functions: ''