mathlib documentation

analysis.schwartz_space

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 #

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_3} {F : Type u_4} [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.

@[ext]
theorem schwartz_map.ext {E : Type u_3} {F : Type u_4} [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_3} {F : Type u_4} [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_3} {F : Type u_4} [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_3} {F : Type u_4} [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_3} {F : Type u_4} [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_3} {F : Type u_4} [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_3} {F : Type u_4} [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_3} {F : Type u_4} [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_3} {F : Type u_4} [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_3} {F : Type u_4} [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_3} {F : Type u_4} [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_3} {F : Type u_4} [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_3} {F : Type u_4} [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_3} {F : Type u_4} [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.le_seminorm (𝕜 : Type u_1) {E : Type u_3} {F : Type u_4} [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.norm_pow_mul_le_seminorm (𝕜 : Type u_1) {E : Type u_3} {F : Type u_4} [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_3} {F : Type u_4} [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) :

The topology on the Schwartz space #

noncomputable def schwartz_seminorm_family (𝕜 : Type u_1) (E : Type u_3) (F : Type u_4) [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
@[protected, instance]

Derivatives of Schwartz functions #

@[protected]
noncomputable def schwartz_map.fderiv {E : Type u_3} {F : Type u_4} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] (f : schwartz_map E F) :

The derivative of a Schwartz function as a Schwartz function with values in the continuous linear maps E→L[ℝ] F.

Equations
@[simp, norm_cast]
@[simp]
noncomputable def schwartz_map.fderiv_lm (𝕜 : Type u_1) {E : Type u_3} {F : Type u_4} [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 derivative on Schwartz space as a linear map.

Equations
@[simp, norm_cast]
noncomputable def schwartz_map.fderiv_clm (𝕜 : Type u_1) {E : Type u_3} {F : Type u_4} [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 derivative on Schwartz space as a continuous linear map.

Equations
@[simp, norm_cast]

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_3} (F : Type u_4) [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_3} (F : Type u_4) [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₀