Schwartz space #

This file defines the Schwartz space. Usually, the Schwartz space is defined as the set of smooth functions $f : ℝ^n → ℂ$ such that there exists $C_{αβ} > 0$ with $$|x^α ∂^β f(x)| < C_{αβ}$$ for all $x ∈ ℝ^n$ and for all multiindices $α, β$. In mathlib, we use a slightly different approach and define define the Schwartz space as all smooth functions f : E → F, where E and F are real normed vector spaces such that for all natural numbers k and n we have uniform bounds ‖x‖^k * ‖iterated_fderiv ℝ n f x‖ < C. This approach completely avoids using partial derivatives as well as polynomials. We construct the topology on the Schwartz space by a family of seminorms, which are the best constants in the above estimates, which is by abstract theory from seminorm_family.module_filter_basis and with_seminorms.to_locally_convex_space turns the Schwartz space into a locally convex topological vector space.

Main definitions #

• schwartz_map: The Schwartz space is the space of smooth functions such that all derivatives decay faster than any power of ‖x‖.
• schwartz_map.seminorm: The family of seminorms as described above
• schwartz_map.fderiv_clm: The differential as a continuous linear map 𝓢(E, F) →L[𝕜] 𝓢(E, E →L[ℝ] F)

Main statements #

• schwartz_map.uniform_add_group and schwartz_map.locally_convex: The Schwartz space is a locally convex topological vector space.

Implementation details #

The implementation of the seminorms is taken almost literally from continuous_linear_map.op_norm.

Notation #

• 𝓢(E, F): The Schwartz space schwartz_map E F localized in schwartz_space

Tags #

Schwartz space, tempered distributions

Algebraic properties #

Seminorms on Schwartz space #

The topology on the Schwartz space #

Derivatives of Schwartz functions #

Inclusion into the space of bounded continuous functions #