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 #

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) [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

Type (max u_4 u_5)

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

@[protected, instance]

def schwartz_map.pi.has_coe {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

has_coe (schwartz_map E F) (E → F)

Equations

schwartz_map.pi.has_coe = {coe := schwartz_map.to_fun _inst_4}

@[protected, instance]

def schwartz_map.fun_like {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

fun_like (schwartz_map E F) E (λ (_x : E), F)

Equations

schwartz_map.fun_like = {coe := λ (f : schwartz_map E F), f.to_fun, coe_injective' := _}

@[protected, instance]

def schwartz_map.has_coe_to_fun {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

has_coe_to_fun (schwartz_map E F) (λ (_x : schwartz_map E F), E → F)

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}

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.

theorem schwartz_map.smooth {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) (n : ℕ∞) :

cont_diff ℝ n ⇑f

Every Schwartz function is smooth.

@[protected, continuity]

theorem schwartz_map.continuous {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) :

continuous ⇑f

Every Schwartz function is continuous.

@[protected]

theorem schwartz_map.differentiable {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) :

differentiable ℝ ⇑f

Every Schwartz function is differentiable.

@[protected]

theorem schwartz_map.differentiable_at {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) {x : E} :

differentiable_at ℝ ⇑f x

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

theorem schwartz_map.is_O_cocompact_zpow_neg_nat {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 : ℕ) :

⇑f =O[filter.cocompact E] λ (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} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] (f : schwartz_map E F) [proper_space E] (s : ℝ) :

⇑f =O[filter.cocompact E] λ (x : E), ‖x‖ ^ s

theorem schwartz_map.is_O_cocompact_zpow {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) [proper_space E] (k : ℤ) :

⇑f =O[filter.cocompact E] λ (x : E), ‖x‖ ^ k

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.bounds_bdd_below {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) :

bdd_below {c : ℝ | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iterated_fderiv ℝ n ⇑f x‖ ≤ c}

theorem schwartz_map.decay_add_le_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 g : schwartz_map E F) (x : E) :

‖x‖ ^ k * ‖iterated_fderiv ℝ n (⇑f + ⇑g) x‖ ≤ ‖x‖ ^ k * ‖iterated_fderiv ℝ n ⇑f x‖ + ‖x‖ ^ k * ‖iterated_fderiv ℝ n ⇑g x‖

theorem schwartz_map.decay_neg_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) (x : E) :

‖x‖ ^ k * ‖iterated_fderiv ℝ n (-⇑f) x‖ = ‖x‖ ^ k * ‖iterated_fderiv ℝ n ⇑f x‖

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) :

‖x‖ ^ k * ‖iterated_fderiv ℝ n (c • ⇑f) x‖ = ‖c‖ * ‖x‖ ^ k * ‖iterated_fderiv ℝ n ⇑f x‖

@[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

schwartz_map.seminorm_aux k n f = has_Inf.Inf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iterated_fderiv ℝ n ⇑f x‖ ≤ c}

theorem schwartz_map.seminorm_aux_nonneg {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) :

0 ≤ schwartz_map.seminorm_aux k n f

theorem schwartz_map.le_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) (x : E) :

‖x‖ ^ k * ‖iterated_fderiv ℝ n ⇑f x‖ ≤ schwartz_map.seminorm_aux k n f

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) :

schwartz_map.seminorm_aux k n f ≤ 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} [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] :

has_smul 𝕜 (schwartz_map E F)

Equations

schwartz_map.has_smul = {smul := λ (c : 𝕜) (f : schwartz_map E F), {to_fun := c • ⇑f, smooth' := _, decay' := _}}

@[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)

theorem schwartz_map.seminorm_aux_smul_le {𝕜 : 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 : ℕ) (c : 𝕜) (f : schwartz_map E F) :

schwartz_map.seminorm_aux k n (c • f) ≤ ‖c‖ * schwartz_map.seminorm_aux k n f

@[protected, instance]

def schwartz_map.has_nsmul {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

has_smul ℕ (schwartz_map E F)

Equations

schwartz_map.has_nsmul = {smul := λ (c : ℕ) (f : schwartz_map E F), {to_fun := c • ⇑f, smooth' := _, decay' := _}}

@[protected, instance]

def schwartz_map.has_zsmul {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

has_smul ℤ (schwartz_map E F)

Equations

schwartz_map.has_zsmul = {smul := λ (c : ℤ) (f : schwartz_map E F), {to_fun := c • ⇑f, smooth' := _, decay' := _}}

@[protected, instance]

def schwartz_map.has_zero {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

has_zero (schwartz_map E F)

Equations

schwartz_map.has_zero = {zero := {to_fun := λ (_x : E), 0, smooth' := _, decay' := _}}

@[protected, instance]

def schwartz_map.inhabited {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

inhabited (schwartz_map E F)

Equations

schwartz_map.inhabited = {default := 0}

theorem schwartz_map.coe_zero {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

↑0 = 0

@[simp]

theorem schwartz_map.coe_fn_zero {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

⇑0 = 0

@[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

theorem schwartz_map.seminorm_aux_zero {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 : ℕ) :

schwartz_map.seminorm_aux k n 0 = 0

@[protected, instance]

def schwartz_map.has_neg {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

has_neg (schwartz_map E F)

Equations

schwartz_map.has_neg = {neg := λ (f : schwartz_map E F), {to_fun := -⇑f, smooth' := _, decay' := _}}

@[protected, instance]

def schwartz_map.has_add {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

has_add (schwartz_map E F)

Equations

schwartz_map.has_add = {add := λ (f g : schwartz_map E F), {to_fun := ⇑f + ⇑g, smooth' := _, decay' := _}}

@[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

theorem schwartz_map.seminorm_aux_add_le {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 g : schwartz_map E F) :

schwartz_map.seminorm_aux k n (f + g) ≤ schwartz_map.seminorm_aux k n f + schwartz_map.seminorm_aux k n g

@[protected, instance]

def schwartz_map.has_sub {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

has_sub (schwartz_map E F)

Equations

schwartz_map.has_sub = {sub := λ (f g : schwartz_map E F), {to_fun := ⇑f - ⇑g, smooth' := _, decay' := _}}

@[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]

def schwartz_map.add_comm_group {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

add_comm_group (schwartz_map E F)

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

def schwartz_map.coe_hom (E : Type u_4) (F : Type u_5) [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

schwartz_map E F →+ E → F

Coercion as an additive homomorphism.

Equations

schwartz_map.coe_hom E F = {to_fun := λ (f : schwartz_map E F), ⇑f, map_zero' := _, map_add' := _}

theorem schwartz_map.coe_coe_hom {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

⇑(schwartz_map.coe_hom E F) = coe_fn

theorem schwartz_map.coe_hom_injective {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

function.injective ⇑(schwartz_map.coe_hom E F)

@[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

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 #

@[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 : ℕ) :

seminorm 𝕜 (schwartz_map E F)

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) _ _ _

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) :

⇑(schwartz_map.seminorm 𝕜 k 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} [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) :

⇑(schwartz_map.seminorm 𝕜 k 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} [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) :

‖x‖ ^ k * ‖iterated_fderiv ℝ n ⇑f x‖ ≤ ⇑(schwartz_map.seminorm 𝕜 k n) f

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 : ℝ) :

|x| ^ k * ‖iterated_deriv n ⇑f x‖ ≤ ⇑(schwartz_map.seminorm 𝕜 k 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} [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) (n : ℕ) (x₀ : E) :

‖iterated_fderiv ℝ n ⇑f x₀‖ ≤ ⇑(schwartz_map.seminorm 𝕜 0 n) 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) :

‖⇑f x₀‖ ≤ ⇑(schwartz_map.seminorm 𝕜 0 0) f

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] :

seminorm_family 𝕜 (schwartz_map E F) (ℕ × ℕ)

The family of Schwartz seminorms.

Equations

schwartz_seminorm_family 𝕜 E F = λ (m : ℕ × ℕ), schwartz_map.seminorm 𝕜 m.fst m.snd

@[simp]

theorem schwartz_map.schwartz_seminorm_family_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] (n k : ℕ) :

schwartz_seminorm_family 𝕜 E F (n, k) = schwartz_map.seminorm 𝕜 n k

@[simp]

theorem schwartz_map.schwartz_seminorm_family_apply_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] [normed_field 𝕜] [normed_space 𝕜 F] [smul_comm_class ℝ 𝕜 F] :

schwartz_seminorm_family 𝕜 E F 0 = schwartz_map.seminorm 𝕜 0 0

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) :

(1 + ‖x‖) ^ k * ‖iterated_fderiv ℝ n ⇑f x‖ ≤ 2 ^ m.fst * ⇑((finset.Iic m).sup (λ (m : ℕ × ℕ), schwartz_map.seminorm 𝕜 m.fst 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) [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

topological_space (schwartz_map E F)

Equations

schwartz_map.topological_space E F = (schwartz_seminorm_family ℝ E F).module_filter_basis.topology'

theorem schwartz_with_seminorms (𝕜 : 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] :

with_seminorms (schwartz_seminorm_family 𝕜 E F)

@[protected, instance]

def schwartz_map.has_continuous_smul {𝕜 : 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] :

has_continuous_smul 𝕜 (schwartz_map E F)

@[protected, instance]

def schwartz_map.topological_add_group {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

topological_add_group (schwartz_map E F)

@[protected, instance]

noncomputable def schwartz_map.uniform_space {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

uniform_space (schwartz_map E F)

Equations

schwartz_map.uniform_space = (schwartz_seminorm_family ℝ E F).add_group_filter_basis.uniform_space

@[protected, instance]

def schwartz_map.uniform_add_group {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

uniform_add_group (schwartz_map E F)

@[protected, instance]

def schwartz_map.locally_convex_space {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

locally_convex_space ℝ (schwartz_map E F)

@[protected, instance]

def schwartz_map.topological_space.first_countable_topology {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] :

topological_space.first_countable_topology (schwartz_map E F)

Functions of temperate growth #

def function.has_temperate_growth {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) :

Prop

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

Equations

function.has_temperate_growth f = (cont_diff ℝ ⊤ f ∧ ∀ (n : ℕ), ∃ (k : ℕ) (C : ℝ), ∀ (x : E), ‖iterated_fderiv ℝ n f x‖ ≤ C * (1 + ‖x‖) ^ k)

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) :

schwartz_map D E →ₛₗ[σ] schwartz_map F G

Create a semilinear map between Schwartz spaces.

Note: This is a helper definition for mk_clm.

Equations

schwartz_map.mk_lm A hadd hsmul hsmooth hbound = {to_fun := λ (f : schwartz_map D E), {to_fun := A ⇑f, smooth' := _, decay' := _}, map_add' := _, map_smul' := _}

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) :

schwartz_map D E →SL[σ] schwartz_map F G

Create a continuous semilinear map between Schwartz spaces.

For an example of using this definition, see fderiv_clm.

Equations

schwartz_map.mk_clm A hadd hsmul hsmooth hbound = {to_linear_map := schwartz_map.mk_lm A hadd hsmul hsmooth hbound, cont := _}

@[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) :

schwartz_map E (E →L[ℝ ] F) →L[𝕜] schwartz_map E F

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

Equations

schwartz_map.eval_clm m = schwartz_map.mk_clm (λ (f : E → (E →L[ℝ ] F)) (x : E), ⇑(f x) m) _ _ _ _

noncomputable def schwartz_map.bilin_left_clm {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_add_comm_group D] [normed_space ℝ D] [normed_add_comm_group G] [normed_space ℝ G] (B : E →L[ℝ ] F →L[ℝ ] G) {g : D → F} (hg : function.has_temperate_growth g) :

schwartz_map D E →L[ℝ ] schwartz_map D G

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

schwartz_map.bilin_left_clm B hg = schwartz_map.mk_clm (λ (f : D → E) (x : D), ⇑(⇑B (f x)) (g x)) _ _ _ _

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) :

schwartz_map E F →L[𝕜] schwartz_map D 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

schwartz_map.comp_clm 𝕜 hg hg_upper = schwartz_map.mk_clm (λ (f : E → F) (x : D), f (g x)) schwartz_map.comp_clm._proof_2 _ _ _

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] :

schwartz_map E F →L[𝕜] schwartz_map E (E →L[ℝ ] F)

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

Equations

schwartz_map.fderiv_clm 𝕜 = schwartz_map.mk_clm (fderiv ℝ) 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} [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) :

⇑(⇑(schwartz_map.fderiv_clm 𝕜) f) x = fderiv ℝ ⇑f x

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] :

schwartz_map ℝ F →L[𝕜] schwartz_map ℝ F

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

Equations

schwartz_map.deriv_clm 𝕜 = schwartz_map.mk_clm (λ (f : ℝ → F), deriv f) schwartz_map.deriv_clm._proof_2 _ schwartz_map.deriv_clm._proof_4 _

@[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 : ℝ) :

⇑(⇑(schwartz_map.deriv_clm 𝕜) f) x = deriv ⇑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) :

schwartz_map E F →L[𝕜] schwartz_map E F

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

Equations

schwartz_map.pderiv_clm 𝕜 m = (schwartz_map.eval_clm m).comp (schwartz_map.fderiv_clm 𝕜)

@[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) :

⇑(⇑(schwartz_map.pderiv_clm 𝕜 m) f) x = ⇑(fderiv ℝ ⇑f x) m

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 : ℕ} :

(fin n → E) → (schwartz_map E F →L[𝕜] schwartz_map E F)

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

Equations

schwartz_map.iterated_pderiv 𝕜 = n.rec_on (λ (x : fin 0 → E), continuous_linear_map.id 𝕜 (schwartz_map E F)) (λ (n : ℕ) (rec : (fin n → E) → (schwartz_map E F →L[𝕜] schwartz_map E F)) (x : fin n.succ → E), (schwartz_map.pderiv_clm 𝕜 (x 0)).comp (rec (fin.tail x)))

@[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) :

⇑(schwartz_map.iterated_pderiv 𝕜 m) f = f

@[simp]

theorem schwartz_map.iterated_pderiv_one (𝕜 : 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 1 → E) (f : schwartz_map E F) :

⇑(schwartz_map.iterated_pderiv 𝕜 m) f = ⇑(schwartz_map.pderiv_clm 𝕜 (m 0)) f

theorem schwartz_map.iterated_pderiv_succ_left (𝕜 : 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 : ℕ} (m : fin (n + 1) → E) (f : schwartz_map E F) :

⇑(schwartz_map.iterated_pderiv 𝕜 m) f = ⇑(schwartz_map.pderiv_clm 𝕜 (m 0)) (⇑(schwartz_map.iterated_pderiv 𝕜 (fin.tail m)) f)

theorem schwartz_map.iterated_pderiv_succ_right (𝕜 : 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 : ℕ} (m : fin (n + 1) → E) (f : schwartz_map E F) :

⇑(schwartz_map.iterated_pderiv 𝕜 m) f = ⇑(schwartz_map.iterated_pderiv 𝕜 (fin.init m)) (⇑(schwartz_map.pderiv_clm 𝕜 (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} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] (f : schwartz_map E F) :

bounded_continuous_function E F

Schwartz functions as bounded continuous functions

Equations

f.to_bounded_continuous_function = bounded_continuous_function.of_normed_add_comm_group ⇑f _ (⇑(schwartz_map.seminorm ℝ 0 0) f) _

@[simp]

theorem schwartz_map.to_bounded_continuous_function_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 : schwartz_map E F) (x : E) :

⇑(f.to_bounded_continuous_function) x = ⇑f x

noncomputable def schwartz_map.to_continuous_map {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) :

Schwartz functions as continuous functions

Equations

f.to_continuous_map = f.to_bounded_continuous_function.to_continuous_map

noncomputable def schwartz_map.to_bounded_continuous_function_lm (𝕜 : 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] :

schwartz_map E F →ₗ[𝕜] bounded_continuous_function E F

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' := _}

@[simp]

theorem schwartz_map.to_bounded_continuous_function_lm_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) :

⇑(⇑(schwartz_map.to_bounded_continuous_function_lm 𝕜 E F) f) x = ⇑f x

noncomputable def schwartz_map.to_bounded_continuous_function_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] :

schwartz_map E F →L[𝕜] bounded_continuous_function E F

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 := _}

@[simp]

theorem schwartz_map.to_bounded_continuous_function_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) :

⇑(⇑(schwartz_map.to_bounded_continuous_function_clm 𝕜 E F) f) x = ⇑f x

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) :

schwartz_map E F →L[𝕜] F

The Dirac delta distribution

Equations

schwartz_map.delta 𝕜 F x = (bounded_continuous_function.eval_clm 𝕜 x).comp (schwartz_map.to_bounded_continuous_function_clm 𝕜 E F)

@[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₀