mathlib3 documentation

analysis.schwartz_space

Schwartz space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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. The abstract theory of topological vector spaces developed in 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 #

Main statements #

Implementation details #

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

Notation #

Tags #

Schwartz space, tempered distributions

@[protected, instance]
Equations
@[protected, instance]

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations
theorem schwartz_map.decay {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] (f : schwartz_map E F) (k n : ) :
(C : ) (hC : 0 < C), (x : E), x ^ k * iterated_fderiv n f x C

All derivatives of a Schwartz function are rapidly decaying.

Every Schwartz function is smooth.

@[protected, continuity]

Every Schwartz function is continuous.

@[protected]

Every Schwartz function is differentiable.

@[protected]

Every Schwartz function is differentiable at any point.

@[ext]
theorem schwartz_map.ext {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {f g : schwartz_map E F} (h : (x : E), f x = g x) :
f = g

Auxiliary lemma, used in proving the more general result is_O_cocompact_zpow.

theorem schwartz_map.bounds_nonempty {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] (k n : ) (f : schwartz_map E F) :
(c : ), c {c : | 0 c (x : E), x ^ k * iterated_fderiv n f x c}
theorem schwartz_map.decay_smul_aux {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (k n : ) (f : schwartz_map E F) (c : 𝕜) (x : E) :
@[protected]
noncomputable def schwartz_map.seminorm_aux {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] (k n : ) (f : schwartz_map E F) :

Helper definition for the seminorms of the Schwartz space.

Equations
theorem schwartz_map.seminorm_aux_le_bound {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] (k n : ) (f : schwartz_map E F) {M : } (hMp : 0 M) (hM : (x : E), x ^ k * iterated_fderiv n f x M) :

If one controls the norm of every A x, then one controls the norm of A.

Algebraic properties #

@[protected, instance]
Equations
@[simp]
theorem schwartz_map.smul_apply {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] {f : schwartz_map E F} {c : 𝕜} {x : E} :
(c f) x = c f x
@[protected, instance]
def schwartz_map.is_scalar_tower {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] [normed_field 𝕜'] [normed_space 𝕜' F] [smul_comm_class 𝕜' F] [has_smul 𝕜 𝕜'] [is_scalar_tower 𝕜 𝕜' F] :
is_scalar_tower 𝕜 𝕜' (schwartz_map E F)
@[protected, instance]
def schwartz_map.smul_comm_class {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] [normed_field 𝕜'] [normed_space 𝕜' F] [smul_comm_class 𝕜' F] [smul_comm_class 𝕜 𝕜' F] :
smul_comm_class 𝕜 𝕜' (schwartz_map E F)
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem schwartz_map.zero_apply {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {x : E} :
0 x = 0
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem schwartz_map.add_apply {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {f g : schwartz_map E F} {x : E} :
(f + g) x = f x + g x
@[protected, instance]
Equations
@[simp]
theorem schwartz_map.sub_apply {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {f g : schwartz_map E F} {x : E} :
(f - g) x = f x - g x
@[protected, instance]
Equations

Coercion as an additive homomorphism.

Equations
@[protected, instance]
def schwartz_map.module {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] :
module 𝕜 (schwartz_map E F)
Equations

Seminorms on Schwartz space #

@[protected]
noncomputable def schwartz_map.seminorm (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (k n : ) :

The seminorms of the Schwartz space given by the best constants in the definition of 𝓢(E, F).

Equations
theorem schwartz_map.seminorm_le_bound (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (k n : ) (f : schwartz_map E F) {M : } (hMp : 0 M) (hM : (x : E), x ^ k * iterated_fderiv n f x M) :

If one controls the seminorm for every x, then one controls the seminorm.

theorem schwartz_map.seminorm_le_bound' (𝕜 : Type u_1) {F : Type u_5} [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (k n : ) (f : schwartz_map F) {M : } (hMp : 0 M) (hM : (x : ), |x| ^ k * iterated_deriv n f x M) :

If one controls the seminorm for every x, then one controls the seminorm.

Variant for functions 𝓢(ℝ, F).

theorem schwartz_map.le_seminorm (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (k n : ) (f : schwartz_map E F) (x : E) :

The seminorm controls the Schwartz estimate for any fixed x.

theorem schwartz_map.le_seminorm' (𝕜 : Type u_1) {F : Type u_5} [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (k n : ) (f : schwartz_map F) (x : ) :

The seminorm controls the Schwartz estimate for any fixed x.

Variant for functions 𝓢(ℝ, F).

theorem schwartz_map.norm_pow_mul_le_seminorm (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (f : schwartz_map E F) (k : ) (x₀ : E) :
x₀ ^ k * f x₀ (schwartz_map.seminorm 𝕜 k 0) f
theorem schwartz_map.norm_le_seminorm (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (f : schwartz_map E F) (x₀ : E) :
noncomputable def schwartz_seminorm_family (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] :

The family of Schwartz seminorms.

Equations
theorem schwartz_map.one_add_le_sup_seminorm_apply {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] {m : × } {k n : } (hk : k m.fst) (hn : n m.snd) (f : schwartz_map E F) (x : E) :

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 #

@[protected, instance]

Functions of temperate growth #

A function is called of temperate growth if it is smooth and all iterated derivatives are polynomially bounded.

Equations
theorem function.has_temperate_growth.norm_iterated_fderiv_le_uniform_aux {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {f : E F} (hf_temperate : function.has_temperate_growth f) (n : ) :
(k : ) (C : ) (hC : 0 C), (N : ), N n (x : E), iterated_fderiv N f x C * (1 + x) ^ k

Construction of continuous linear maps between Schwartz spaces #

def schwartz_map.mk_lm {𝕜 : Type u_1} {𝕜' : Type u_2} {D : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_field 𝕜'] [normed_add_comm_group D] [normed_space D] [normed_space 𝕜 E] [smul_comm_class 𝕜 E] [normed_add_comm_group G] [normed_space G] [normed_space 𝕜' G] [smul_comm_class 𝕜' G] {σ : 𝕜 →+* 𝕜'} (A : (D E) F G) (hadd : (f g : schwartz_map D E) (x : F), A (f + g) x = A f x + A g x) (hsmul : (a : 𝕜) (f : schwartz_map D E) (x : F), A (a f) x = σ a A f x) (hsmooth : (f : schwartz_map D E), cont_diff (A f)) (hbound : (n : × ), (s : finset ( × )) (C : ) (hC : 0 C), (f : schwartz_map D E) (x : F), x ^ n.fst * iterated_fderiv n.snd (A f) x C * (s.sup (schwartz_seminorm_family 𝕜 D E)) f) :

Create a semilinear map between Schwartz spaces.

Note: This is a helper definition for mk_clm.

Equations
def schwartz_map.mk_clm {𝕜 : Type u_1} {𝕜' : Type u_2} {D : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_field 𝕜'] [normed_add_comm_group D] [normed_space D] [normed_space 𝕜 E] [smul_comm_class 𝕜 E] [normed_add_comm_group G] [normed_space G] [normed_space 𝕜' G] [smul_comm_class 𝕜' G] {σ : 𝕜 →+* 𝕜'} [ring_hom_isometric σ] (A : (D E) F G) (hadd : (f g : schwartz_map D E) (x : F), A (f + g) x = A f x + A g x) (hsmul : (a : 𝕜) (f : schwartz_map D E) (x : F), A (a f) x = σ a A f x) (hsmooth : (f : schwartz_map D E), cont_diff (A f)) (hbound : (n : × ), (s : finset ( × )) (C : ) (hC : 0 C), (f : schwartz_map D E) (x : F), x ^ n.fst * iterated_fderiv n.snd (A f) x C * (s.sup (schwartz_seminorm_family 𝕜 D E)) f) :

Create a continuous semilinear map between Schwartz spaces.

For an example of using this definition, see fderiv_clm.

Equations
@[protected]
noncomputable def schwartz_map.eval_clm {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (m : E) :

The map applying a vector to Hom-valued Schwartz function as a continuous linear map.

Equations

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.

Equations
def schwartz_map.comp_clm (𝕜 : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [is_R_or_C 𝕜] [normed_add_comm_group D] [normed_space D] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] {g : D E} (hg : function.has_temperate_growth g) (hg_upper : (k : ) (C : ), (x : D), x C * (1 + g x) ^ k) :

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.

Equations

Derivatives of Schwartz functions #

noncomputable def schwartz_map.fderiv_clm (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [is_R_or_C 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] :

The Fréchet derivative on Schwartz space as a continuous 𝕜-linear map.

Equations
@[simp]
theorem schwartz_map.fderiv_clm_apply (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [is_R_or_C 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (f : schwartz_map E F) (x : E) :
noncomputable def schwartz_map.deriv_clm (𝕜 : Type u_1) {F : Type u_5} [normed_add_comm_group F] [normed_space F] [is_R_or_C 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] :

The 1-dimensional derivative on Schwartz space as a continuous 𝕜-linear map.

Equations
@[simp]
theorem schwartz_map.deriv_clm_apply (𝕜 : Type u_1) {F : Type u_5} [normed_add_comm_group F] [normed_space F] [is_R_or_C 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (f : schwartz_map F) (x : ) :
noncomputable def schwartz_map.pderiv_clm (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [is_R_or_C 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (m : E) :

The partial derivative (or directional derivative) in the direction m : E as a continuous linear map on Schwartz space.

Equations
@[simp]
theorem schwartz_map.pderiv_clm_apply (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [is_R_or_C 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (m : E) (f : schwartz_map E F) (x : E) :
noncomputable def schwartz_map.iterated_pderiv (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [is_R_or_C 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] {n : } :

The iterated partial derivative (or directional derivative) as a continuous linear map on Schwartz space.

Equations
@[simp]
theorem schwartz_map.iterated_pderiv_zero (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [is_R_or_C 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (m : fin 0 E) (f : schwartz_map E F) :
@[simp]

Inclusion into the space of bounded continuous functions #

Schwartz functions as continuous functions

Equations

The inclusion map from Schwartz functions to bounded continuous functions as a linear map.

Equations

The inclusion map from Schwartz functions to bounded continuous functions as a continuous linear map.

Equations
noncomputable def schwartz_map.delta (𝕜 : Type u_1) {E : Type u_4} (F : Type u_5) [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [is_R_or_C 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (x : E) :

The Dirac delta distribution

Equations
@[simp]
theorem schwartz_map.delta_apply (𝕜 : Type u_1) {E : Type u_4} (F : Type u_5) [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] [is_R_or_C 𝕜] [normed_space 𝕜 F] [smul_comm_class 𝕜 F] (x₀ : E) (f : schwartz_map E F) :
(schwartz_map.delta 𝕜 F x₀) f = f x₀