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 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 * βiteratedFDeriv β 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. The abstract theory of topological vector spaces developed in
SeminormFamily.moduleFilterBasis
and WithSeminorms.toLocallyConvexSpace
turns the
Schwartz space into a locally convex topological vector space.
Main definitions #
SchwartzMap
: The Schwartz space is the space of smooth functions such that all derivatives decay faster than any power ofβxβ
.SchwartzMap.seminorm
: The family of seminorms as described aboveSchwartzMap.fderivCLM
: The differential as a continuous linear mapπ’(E, F) βL[π] π’(E, E βL[β] F)
SchwartzMap.derivCLM
: The one-dimensional derivative as a continuous linear mapπ’(β, F) βL[π] π’(β, F)
Main statements #
SchwartzMap.instUniformAddGroup
andSchwartzMap.instLocallyConvexSpace
: The Schwartz space is a locally convex topological vector space.SchwartzMap.one_add_le_sup_seminorm_apply
: For a Schwartz functionf
there is a uniform bound on(1 + βxβ) ^ k * βiteratedFDeriv β n f xβ
.
Implementation details #
The implementation of the seminorms is taken almost literally from ContinuousLinearMap.opNorm
.
Notation #
π’(E, F)
: The Schwartz spaceSchwartzMap E F
localized inSchwartzSpace
Tags #
Schwartz space, tempered distributions
- toFun : E β F
A function is a Schwartz function if it is smooth and all derivatives decay faster than
any power of βxβ
.
Instances For
Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun
.
All derivatives of a Schwartz function are rapidly decaying.
Every Schwartz function is smooth.
Every Schwartz function is continuous.
Every Schwartz function is differentiable.
Every Schwartz function is differentiable at any point.
Auxiliary lemma, used in proving the more general result isBigO_cocompact_rpow
.
Helper definition for the seminorms of the Schwartz space.
Instances For
If one controls the norm of every A x
, then one controls the norm of A
.
Algebraic properties #
Coercion as an additive homomorphism.
Instances For
Seminorms on Schwartz space #
The seminorms of the Schwartz space given by the best constants in the definition of
π’(E, F)
.
Instances For
If one controls the seminorm for every x
, then one controls the seminorm.
If one controls the seminorm for every x
, then one controls the seminorm.
Variant for functions π’(β, F)
.
The seminorm controls the Schwartz estimate for any fixed x
.
The seminorm controls the Schwartz estimate for any fixed x
.
Variant for functions π’(β, F)
.
The family of Schwartz seminorms.
Instances For
A more convenient version of le_sup_seminorm_apply
.
The set Finset.Iic m
is the set of all pairs (k', n')
with k' β€ m.1
and n' β€ m.2
.
Note that the constant is far from optimal.
The topology on the Schwartz space #
Functions of temperate growth #
A function is called of temperate growth if it is smooth and all iterated derivatives are polynomially bounded.
Instances For
Construction of continuous linear maps between Schwartz spaces #
Create a semilinear map between Schwartz spaces.
Note: This is a helper definition for mkCLM
.
Instances For
Create a continuous semilinear map between Schwartz spaces.
For an example of using this definition, see fderivCLM
.
Instances For
The map applying a vector to Hom-valued Schwartz function as a continuous linear map.
Instances For
The map f β¦ (x β¦ B (f x) (g x))
as a continuous π
-linear map on Schwartz space,
where B
is a continuous π
-linear map and g
is a function of temperate growth.
Instances For
Composition with a function on the right is a continuous linear map on Schwartz space provided that the function is temperate and growths polynomially near infinity.
Instances For
Derivatives of Schwartz functions #
The FrΓ©chet derivative on Schwartz space as a continuous π
-linear map.
Instances For
The 1-dimensional derivative on Schwartz space as a continuous π
-linear map.
Instances For
The partial derivative (or directional derivative) in the direction m : E
as a
continuous linear map on Schwartz space.
Instances For
The iterated partial derivative (or directional derivative) as a continuous linear map on Schwartz space.
Instances For
Inclusion into the space of bounded continuous functions #
Schwartz functions as bounded continuous functions
Instances For
Schwartz functions as continuous functions
Instances For
The inclusion map from Schwartz functions to bounded continuous functions as a linear map.
Instances For
The inclusion map from Schwartz functions to bounded continuous functions as a continuous linear map.
Instances For
The Dirac delta distribution