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 aboveschwartz_map.fderiv_clm
: The differential as a continuous linear map𝓢(E, F) →L[𝕜] 𝓢(E, E →L[ℝ] F)
Main statements #
schwartz_map.uniform_add_group
andschwartz_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 spaceschwartz_map E F
localized inschwartz_space
Tags #
Schwartz space, tempered distributions
- to_fun : E → F
- smooth' : cont_diff ℝ ⊤ self.to_fun
- decay' : ∀ (k n : ℕ), ∃ (C : ℝ), ∀ (x : E), ‖x‖ ^ k * ‖iterated_fderiv ℝ n self.to_fun x‖ ≤ C
A function is a Schwartz function if it is smooth and all derivatives decay faster than
any power of ‖x‖
.
Instances for schwartz_map
- schwartz_map.has_sizeof_inst
- schwartz_map.pi.has_coe
- schwartz_map.fun_like
- schwartz_map.has_coe_to_fun
- schwartz_map.has_smul
- schwartz_map.is_scalar_tower
- schwartz_map.smul_comm_class
- schwartz_map.has_nsmul
- schwartz_map.has_zsmul
- schwartz_map.has_zero
- schwartz_map.inhabited
- schwartz_map.has_neg
- schwartz_map.has_add
- schwartz_map.has_sub
- schwartz_map.add_comm_group
- schwartz_map.module
- schwartz_map.topological_space
- schwartz_map.has_continuous_smul
- schwartz_map.topological_add_group
- schwartz_map.uniform_space
- schwartz_map.uniform_add_group
- schwartz_map.locally_convex_space
- schwartz_map.topological_space.first_countable_topology
Equations
- schwartz_map.pi.has_coe = {coe := schwartz_map.to_fun _inst_4}
Equations
- schwartz_map.fun_like = {coe := λ (f : schwartz_map E F), f.to_fun, coe_injective' := _}
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
.
Equations
- schwartz_map.has_coe_to_fun = {coe := λ (p : schwartz_map E F), p.to_fun}
All derivatives of a Schwartz function are rapidly decaying.
Every Schwartz function is smooth.
Every Schwartz function is continuous.
Every Schwartz function is differentiable.
Auxiliary lemma, used in proving the more general result is_O_cocompact_zpow
.
Helper definition for the seminorms of the Schwartz space.
If one controls the norm of every A x
, then one controls the norm of A
.
Algebraic properties #
Equations
- schwartz_map.inhabited = {default := 0}
Equations
- schwartz_map.add_comm_group = function.injective.add_comm_group coe_fn schwartz_map.add_comm_group._proof_1 schwartz_map.add_comm_group._proof_2 schwartz_map.add_comm_group._proof_3 schwartz_map.add_comm_group._proof_4 schwartz_map.add_comm_group._proof_5 schwartz_map.add_comm_group._proof_6 schwartz_map.add_comm_group._proof_7
Coercion as an additive homomorphism.
Equations
- schwartz_map.coe_hom E F = {to_fun := λ (f : schwartz_map E F), ⇑f, map_zero' := _, map_add' := _}
Equations
- schwartz_map.module = function.injective.module 𝕜 (schwartz_map.coe_hom E F) schwartz_map.coe_hom_injective schwartz_map.module._proof_1
Seminorms on Schwartz space #
The seminorms of the Schwartz space given by the best constants in the definition of
𝓢(E, F)
.
Equations
- schwartz_map.seminorm 𝕜 k n = seminorm.of_smul_le (schwartz_map.seminorm_aux k n) _ _ _
If one controls the seminorm for every x
, then one controls the seminorm.
The seminorm controls the Schwartz estimate for any fixed x
.
The topology on the Schwartz space #
The family of Schwartz seminorms.
Equations
- schwartz_seminorm_family 𝕜 E F = λ (n : ℕ × ℕ), schwartz_map.seminorm 𝕜 n.fst n.snd
Equations
Derivatives of Schwartz functions #
The derivative of a Schwartz function as a Schwartz function with values in the
continuous linear maps E→L[ℝ] F
.
The derivative on Schwartz space as a linear map.
Equations
- schwartz_map.fderiv_lm 𝕜 = {to_fun := schwartz_map.fderiv _inst_4, map_add' := _, map_smul' := _}
The derivative on Schwartz space as a continuous linear map.
Equations
- schwartz_map.fderiv_clm 𝕜 = {to_linear_map := schwartz_map.fderiv_lm 𝕜 _inst_7, cont := _}
Inclusion into the space of bounded continuous functions #
Schwartz functions as bounded continuous functions
Equations
Schwartz functions as continuous functions
Equations
The inclusion map from Schwartz functions to bounded continuous functions as a linear map.
Equations
- schwartz_map.to_bounded_continuous_function_lm 𝕜 E F = {to_fun := λ (f : schwartz_map E F), f.to_bounded_continuous_function, map_add' := _, map_smul' := _}
The inclusion map from Schwartz functions to bounded continuous functions as a continuous linear map.
Equations
- schwartz_map.to_bounded_continuous_function_clm 𝕜 E F = {to_linear_map := {to_fun := (schwartz_map.to_bounded_continuous_function_lm 𝕜 E F).to_fun, map_add' := _, map_smul' := _}, cont := _}
The Dirac delta distribution