# mathlib3documentation

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 #

• `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)`
• `schwartz_map.deriv_clm`: The one-dimensional derivative as a continuous linear map `𝓢(ℝ, F) →L[𝕜] 𝓢(ℝ, F)`

## Main statements #

• `schwartz_map.uniform_add_group` and `schwartz_map.locally_convex`: The Schwartz space is a locally convex topological vector space.
• `schwartz_map.one_add_le_sup_seminorm_apply`: For a Schwartz function `f` there is a uniform bound on `(1 + ‖x‖) ^ k * ‖iterated_fderiv ℝ n f x‖`.

## 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

structure schwartz_map (E : Type u_4) (F : Type u_5) [ E] [ F] :
Type (max u_4 u_5)

A function is a Schwartz function if it is smooth and all derivatives decay faster than any power of `‖x‖`.

Instances for `schwartz_map`
@[protected, instance]
def schwartz_map.pi.has_coe {E : Type u_4} {F : Type u_5} [ E] [ F] :
has_coe F) (E F)
Equations
@[protected, instance]
def schwartz_map.fun_like {E : Type u_4} {F : Type u_5} [ E] [ F] :
fun_like F) E (λ (_x : E), F)
Equations
@[protected, instance]
def schwartz_map.has_coe_to_fun {E : Type u_4} {F : Type u_5} [ E] [ F] :
(λ (_x : F), E F)

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} [ E] [ F] (f : F) (k n : ) :
(C : ) (hC : 0 < C), (x : E), x ^ k * x C

All derivatives of a Schwartz function are rapidly decaying.

theorem schwartz_map.smooth {E : Type u_4} {F : Type u_5} [ E] [ F] (f : F) (n : ℕ∞) :
f

Every Schwartz function is smooth.

@[protected, continuity]
theorem schwartz_map.continuous {E : Type u_4} {F : Type u_5} [ E] [ F] (f : F) :

Every Schwartz function is continuous.

@[protected]
theorem schwartz_map.differentiable {E : Type u_4} {F : Type u_5} [ E] [ F] (f : F) :

Every Schwartz function is differentiable.

@[protected]
theorem schwartz_map.differentiable_at {E : Type u_4} {F : Type u_5} [ E] [ F] (f : F) {x : E} :

Every Schwartz function is differentiable at any point.

@[ext]
theorem schwartz_map.ext {E : Type u_4} {F : Type u_5} [ E] [ F] {f g : F} (h : (x : E), f x = g x) :
f = g
theorem schwartz_map.is_O_cocompact_zpow_neg_nat {E : Type u_4} {F : Type u_5} [ E] [ F] (f : F) (k : ) :
f =O[] λ (x : E), x ^ -k

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

theorem schwartz_map.is_O_cocompact_rpow {E : Type u_4} {F : Type u_5} [ E] [ F] (f : F) [proper_space E] (s : ) :
f =O[] λ (x : E), x ^ s
theorem schwartz_map.is_O_cocompact_zpow {E : Type u_4} {F : Type u_5} [ E] [ F] (f : F) [proper_space E] (k : ) :
f =O[] λ (x : E), x ^ k
theorem schwartz_map.bounds_nonempty {E : Type u_4} {F : Type u_5} [ E] [ F] (k n : ) (f : F) :
(c : ), c {c : | 0 c (x : E), x ^ k * x c}
theorem schwartz_map.bounds_bdd_below {E : Type u_4} {F : Type u_5} [ E] [ F] (k n : ) (f : F) :
bdd_below {c : | 0 c (x : E), x ^ k * x c}
theorem schwartz_map.decay_add_le_aux {E : Type u_4} {F : Type u_5} [ E] [ F] (k n : ) (f g : F) (x : E) :
theorem schwartz_map.decay_neg_aux {E : Type u_4} {F : Type u_5} [ E] [ F] (k n : ) (f : F) (x : E) :
x ^ k * (-f) x = x ^ k * x
theorem schwartz_map.decay_smul_aux {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [ E] [ F] [normed_field 𝕜] [ F] [ F] (k n : ) (f : F) (c : 𝕜) (x : E) :
x ^ k * (c f) x = c * x ^ k * x
@[protected]
noncomputable def schwartz_map.seminorm_aux {E : Type u_4} {F : Type u_5} [ E] [ F] (k n : ) (f : F) :

Helper definition for the seminorms of the Schwartz space.

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

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

### Algebraic properties #

@[protected, instance]
def schwartz_map.has_smul {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [ E] [ F] [normed_field 𝕜] [ F] [ F] :
F)
Equations
@[simp]
theorem schwartz_map.smul_apply {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [ E] [ F] [normed_field 𝕜] [ F] [ F] {f : 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} [ E] [ F] [normed_field 𝕜] [ F] [ F] [normed_field 𝕜'] [ F] [ F] [ 𝕜'] [ 𝕜' F] :
𝕜' F)
@[protected, instance]
def schwartz_map.smul_comm_class {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_4} {F : Type u_5} [ E] [ F] [normed_field 𝕜] [ F] [ F] [normed_field 𝕜'] [ F] [ F] [ 𝕜' F] :
𝕜' F)
theorem schwartz_map.seminorm_aux_smul_le {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [ E] [ F] [normed_field 𝕜] [ F] [ F] (k n : ) (c : 𝕜) (f : F) :
(c f) c *
@[protected, instance]
def schwartz_map.has_nsmul {E : Type u_4} {F : Type u_5} [ E] [ F] :
F)
Equations
@[protected, instance]
def schwartz_map.has_zsmul {E : Type u_4} {F : Type u_5} [ E] [ F] :
F)
Equations
@[protected, instance]
def schwartz_map.has_zero {E : Type u_4} {F : Type u_5} [ E] [ F] :
Equations
@[protected, instance]
def schwartz_map.inhabited {E : Type u_4} {F : Type u_5} [ E] [ F] :
Equations
theorem schwartz_map.coe_zero {E : Type u_4} {F : Type u_5} [ E] [ F] :
0 = 0
@[simp]
theorem schwartz_map.coe_fn_zero {E : Type u_4} {F : Type u_5} [ E] [ F] :
0 = 0
@[simp]
theorem schwartz_map.zero_apply {E : Type u_4} {F : Type u_5} [ E] [ F] {x : E} :
0 x = 0
theorem schwartz_map.seminorm_aux_zero {E : Type u_4} {F : Type u_5} [ E] [ F] (k n : ) :
= 0
@[protected, instance]
def schwartz_map.has_neg {E : Type u_4} {F : Type u_5} [ E] [ F] :
Equations
@[protected, instance]
def schwartz_map.has_add {E : Type u_4} {F : Type u_5} [ E] [ F] :
Equations
@[simp]
theorem schwartz_map.add_apply {E : Type u_4} {F : Type u_5} [ E] [ F] {f g : F} {x : E} :
(f + g) x = f x + g x
theorem schwartz_map.seminorm_aux_add_le {E : Type u_4} {F : Type u_5} [ E] [ F] (k n : ) (f g : F) :
(f + g)
@[protected, instance]
def schwartz_map.has_sub {E : Type u_4} {F : Type u_5} [ E] [ F] :
Equations
@[simp]
theorem schwartz_map.sub_apply {E : Type u_4} {F : Type u_5} [ E] [ F] {f g : F} {x : E} :
(f - g) x = f x - g x
@[protected, instance]
def schwartz_map.add_comm_group {E : Type u_4} {F : Type u_5} [ E] [ F] :
Equations
• schwartz_map.add_comm_group = 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
def schwartz_map.coe_hom (E : Type u_4) (F : Type u_5) [ E] [ F] :
F →+ E F

Coercion as an additive homomorphism.

Equations
theorem schwartz_map.coe_coe_hom {E : Type u_4} {F : Type u_5} [ E] [ F] :
theorem schwartz_map.coe_hom_injective {E : Type u_4} {F : Type u_5} [ E] [ F] :
@[protected, instance]
def schwartz_map.module {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [ E] [ F] [normed_field 𝕜] [ F] [ F] :
F)
Equations

### Seminorms on Schwartz space #

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

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} [ E] [ F] [normed_field 𝕜] [ F] [ F] (k n : ) (f : F) {M : } (hMp : 0 M) (hM : (x : E), x ^ k * x M) :
n) f 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} [ F] [normed_field 𝕜] [ F] [ F] (k n : ) (f : F) {M : } (hMp : 0 M) (hM : (x : ), |x| ^ k * x M) :
n) f 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} [ E] [ F] [normed_field 𝕜] [ F] [ F] (k n : ) (f : F) (x : E) :
x ^ k * x n) f

The seminorm controls the Schwartz estimate for any fixed `x`.

theorem schwartz_map.le_seminorm' (𝕜 : Type u_1) {F : Type u_5} [ F] [normed_field 𝕜] [ F] [ F] (k n : ) (f : F) (x : ) :
|x| ^ k * x n) f

The seminorm controls the Schwartz estimate for any fixed `x`.

Variant for functions `𝓢(ℝ, F)`.

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

The family of Schwartz seminorms.

Equations
@[simp]
theorem schwartz_map.schwartz_seminorm_family_apply (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [ E] [ F] [normed_field 𝕜] [ F] [ F] (n k : ) :
(n, k) =
@[simp]
theorem schwartz_map.schwartz_seminorm_family_apply_zero (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [ E] [ F] [normed_field 𝕜] [ F] [ F] :
0 =
theorem schwartz_map.one_add_le_sup_seminorm_apply {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [ E] [ F] [normed_field 𝕜] [ F] [ F] {m : × } {k n : } (hk : k m.fst) (hn : n m.snd) (f : F) (x : E) :
(1 + x) ^ k * x 2 ^ m.fst * ((finset.Iic m).sup (λ (m : × ), m.snd)) f

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]
noncomputable def schwartz_map.topological_space (E : Type u_4) (F : Type u_5) [ E] [ F] :
Equations
theorem schwartz_with_seminorms (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [ E] [ F] [normed_field 𝕜] [ F] [ F] :
@[protected, instance]
def schwartz_map.has_continuous_smul {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [ E] [ F] [normed_field 𝕜] [ F] [ F] :
F)
@[protected, instance]
def schwartz_map.topological_add_group {E : Type u_4} {F : Type u_5} [ E] [ F] :
@[protected, instance]
noncomputable def schwartz_map.uniform_space {E : Type u_4} {F : Type u_5} [ E] [ F] :
Equations
@[protected, instance]
def schwartz_map.uniform_add_group {E : Type u_4} {F : Type u_5} [ E] [ F] :
@[protected, instance]
def schwartz_map.locally_convex_space {E : Type u_4} {F : Type u_5} [ E] [ F] :
@[protected, instance]

### Functions of temperate growth #

def function.has_temperate_growth {E : Type u_4} {F : Type u_5} [ E] [ F] (f : E F) :
Prop

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} [ E] [ F] {f : E F} (hf_temperate : function.has_temperate_growth f) (n : ) :
(k : ) (C : ) (hC : 0 C), (N : ), N n (x : E), 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} [ E] [ F] [normed_field 𝕜] [normed_field 𝕜'] [ D] [ E] [ E] [ G] [ G] [ G] {σ : 𝕜 →+* 𝕜'} (A : (D E) F G) (hadd : (f g : E) (x : F), A (f + g) x = A f x + A g x) (hsmul : (a : 𝕜) (f : E) (x : F), A (a f) x = σ a A f x) (hsmooth : (f : E), (A f)) (hbound : (n : × ), (s : finset ( × )) (C : ) (hC : 0 C), (f : E) (x : F), x ^ n.fst * (A f) x C * (s.sup 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} [ E] [ F] [normed_field 𝕜] [normed_field 𝕜'] [ D] [ E] [ E] [ G] [ G] [ G] {σ : 𝕜 →+* 𝕜'} (A : (D E) F G) (hadd : (f g : E) (x : F), A (f + g) x = A f x + A g x) (hsmul : (a : 𝕜) (f : E) (x : F), A (a f) x = σ a A f x) (hsmooth : (f : E), (A f)) (hbound : (n : × ), (s : finset ( × )) (C : ) (hC : 0 C), (f : E) (x : F), x ^ n.fst * (A f) x C * (s.sup E)) f) :
E →SL[σ] G

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} [ E] [ F] [normed_field 𝕜] [ F] [ F] (m : E) :
(E →L[] F) →L[𝕜] F

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

Equations
noncomputable def schwartz_map.bilin_left_clm {D : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [ E] [ F] [ D] [ G] (B : E →L[] F →L[] G) {g : D F}  :

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} [ E] [ F] [is_R_or_C 𝕜] [ D] [ F] [ F] {g : D E} (hg_upper : (k : ) (C : ), (x : D), x C * (1 + g x) ^ k) :
F →L[𝕜] F

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} [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] :
F →L[𝕜] (E →L[] F)

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

Equations
• = schwartz_map.fderiv_clm._proof_12 _ schwartz_map.fderiv_clm._proof_14 _
@[simp]
theorem schwartz_map.fderiv_clm_apply (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] (f : F) (x : E) :
f) x = f x
noncomputable def schwartz_map.deriv_clm (𝕜 : Type u_1) {F : Type u_5} [ F] [is_R_or_C 𝕜] [ F] [ 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} [ F] [is_R_or_C 𝕜] [ F] [ F] (f : F) (x : ) :
f) x = x
noncomputable def schwartz_map.pderiv_clm (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] (m : E) :
F →L[𝕜] F

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} [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] (m : E) (f : F) (x : E) :
( f) x = f x) m
noncomputable def schwartz_map.iterated_pderiv (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] {n : } :
(fin n E) F →L[𝕜] F)

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} [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] (m : fin 0 E) (f : F) :
= f
@[simp]
theorem schwartz_map.iterated_pderiv_one (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] (m : fin 1 E) (f : F) :
= (m 0)) f
theorem schwartz_map.iterated_pderiv_succ_left (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] {n : } (m : fin (n + 1) E) (f : F) :
= (m 0)) ( f)
theorem schwartz_map.iterated_pderiv_succ_right (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] {n : } (m : fin (n + 1) E) (f : F) :
= ( (m (fin.last n))) f)

### Inclusion into the space of bounded continuous functions #

noncomputable def schwartz_map.to_bounded_continuous_function {E : Type u_4} {F : Type u_5} [ E] [ F] (f : F) :

Schwartz functions as bounded continuous functions

Equations
@[simp]
theorem schwartz_map.to_bounded_continuous_function_apply {E : Type u_4} {F : Type u_5} [ E] [ F] (f : F) (x : E) :
= f x
noncomputable def schwartz_map.to_continuous_map {E : Type u_4} {F : Type u_5} [ E] [ F] (f : F) :
C(E, F)

Schwartz functions as continuous functions

Equations
noncomputable def schwartz_map.to_bounded_continuous_function_lm (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] :

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

Equations
@[simp]
theorem schwartz_map.to_bounded_continuous_function_lm_apply (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] (f : F) (x : E) :
x = f x
noncomputable def schwartz_map.to_bounded_continuous_function_clm (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] :

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

Equations
@[simp]
theorem schwartz_map.to_bounded_continuous_function_clm_apply (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] (f : F) (x : E) :
x = f x
noncomputable def schwartz_map.delta (𝕜 : Type u_1) {E : Type u_4} (F : Type u_5) [ E] [ F] [is_R_or_C 𝕜] [ F] [ F] (x : E) :
F →L[𝕜] F

The Dirac delta distribution

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