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 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 * ‖iteratedFDeriv ℝ 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 SeminormFamily.moduleFilterBasis and WithSeminorms.toLocallyConvexSpace turns the Schwartz space into a locally convex topological vector space.

Main definitions

• SchwartzMap: The Schwartz space is the space of smooth functions such that all derivatives decay faster than any power of ‖x‖.
• SchwartzMap.seminorm: The family of seminorms as described above
• SchwartzMap.fderivCLM: The differential as a continuous linear map 𝓢(E, F) →L[𝕜] 𝓢(E, E →L[ℝ] F)
• SchwartzMap.derivCLM: The one-dimensional derivative as a continuous linear map 𝓢(ℝ, F) →L[𝕜] 𝓢(ℝ, F)

Main statements

• SchwartzMap.instUniformAddGroup and SchwartzMap.instLocallyConvexSpace: The Schwartz space is a locally convex topological vector space.
• SchwartzMap.one_add_le_sup_seminorm_apply: For a Schwartz function f there is a uniform bound on (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖.

Implementation details

The implementation of the seminorms is taken almost literally from ContinuousLinearMap.opNorm.

Notation

• 𝓢(E, F): The Schwartz space SchwartzMap E F localized in SchwartzSpace

Tags

Schwartz space, tempered distributions

structure SchwartzMap (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Type (max u_4 u_5)

• toFun : E → F
• smooth' : ContDiff ℝ ⊤ s.toFun
• decay' : ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n s.toFun x‖ ≤ C

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

def SchwartzSpace.«term𝓢(_,_)» : Lean.ParserDescr

instance SchwartzMap.instFunLike {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : FunLike (SchwartzMap E F) E fun x => F

instance SchwartzMap.instCoeFun {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : CoeFun (SchwartzMap E F) fun x => E → F

Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun.

theorem SchwartzMap.decay {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) (k : ℕ) (n : ℕ) : ∃ C, 0 < C ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (↑f) x‖ ≤ C

All derivatives of a Schwartz function are rapidly decaying.

theorem SchwartzMap.smooth {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) (n : ℕ∞) : ContDiff ℝ n ↑f

Every Schwartz function is smooth.

theorem SchwartzMap.continuous {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) : Continuous ↑f

Every Schwartz function is continuous.

theorem SchwartzMap.differentiable {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) : Differentiable ℝ ↑f

Every Schwartz function is differentiable.

theorem SchwartzMap.differentiableAt {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) {x : E} : DifferentiableAt ℝ (↑f) x

Every Schwartz function is differentiable at any point.

theorem SchwartzMap.ext {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : SchwartzMap E F} {g : SchwartzMap E F} (h : ∀ (x : E), ↑f x = ↑g x) : f = g

theorem SchwartzMap.isBigO_cocompact_zpow_neg_nat {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) (k : ℕ) : ↑f =O[Filter.cocompact E] fun x => ‖x‖ ^ (-↑k)

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

theorem SchwartzMap.isBigO_cocompact_rpow {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) [ProperSpace E] (s : ℝ) : ↑f =O[Filter.cocompact E] fun x => ‖x‖ ^ s

theorem SchwartzMap.isBigO_cocompact_zpow {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) [ProperSpace E] (k : ℤ) : ↑f =O[Filter.cocompact E] fun x => ‖x‖ ^ k

theorem SchwartzMap.bounds_nonempty {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (n : ℕ) (f : SchwartzMap E F) : ∃ c, c ∈ {c | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (↑f) x‖ ≤ c}

theorem SchwartzMap.bounds_bddBelow {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (n : ℕ) (f : SchwartzMap E F) : BddBelow {c | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (↑f) x‖ ≤ c}

theorem SchwartzMap.decay_add_le_aux {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (n : ℕ) (f : SchwartzMap E F) (g : SchwartzMap E F) (x : E) : ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (↑f + ↑g) x‖ ≤ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (↑f) x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (↑g) x‖

theorem SchwartzMap.decay_neg_aux {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (n : ℕ) (f : SchwartzMap E F) (x : E) : ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (-↑f) x‖ = ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (↑f) x‖

theorem SchwartzMap.decay_smul_aux {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (k : ℕ) (n : ℕ) (f : SchwartzMap E F) (c : 𝕜) (x : E) : ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ↑f) x‖ = ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (↑f) x‖

def SchwartzMap.seminormAux {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (n : ℕ) (f : SchwartzMap E F) : ℝ

Helper definition for the seminorms of the Schwartz space.

theorem SchwartzMap.seminormAux_nonneg {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (n : ℕ) (f : SchwartzMap E F) : 0 ≤ SchwartzMap.seminormAux k n f

theorem SchwartzMap.le_seminormAux {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (n : ℕ) (f : SchwartzMap E F) (x : E) : ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (↑f) x‖ ≤ SchwartzMap.seminormAux k n f

theorem SchwartzMap.seminormAux_le_bound {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (n : ℕ) (f : SchwartzMap E F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (↑f) x‖ ≤ M) : SchwartzMap.seminormAux k n f ≤ M

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

Algebraic properties

instance SchwartzMap.instSMul {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] : SMul 𝕜 (SchwartzMap E F)

@[simp]

theorem SchwartzMap.smul_apply {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {f : SchwartzMap E F} {c : 𝕜} {x : E} : ↑(c • f) x = c • ↑f x

instance SchwartzMap.instIsScalarTower {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass ℝ 𝕜' F] [SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' F] : IsScalarTower 𝕜 𝕜' (SchwartzMap E F)

instance SchwartzMap.instSMulCommClass {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass ℝ 𝕜' F] [SMulCommClass 𝕜 𝕜' F] : SMulCommClass 𝕜 𝕜' (SchwartzMap E F)

theorem SchwartzMap.seminormAux_smul_le {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (k : ℕ) (n : ℕ) (c : 𝕜) (f : SchwartzMap E F) : SchwartzMap.seminormAux k n (c • f) ≤ ‖c‖ * SchwartzMap.seminormAux k n f

instance SchwartzMap.instNSMul {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : SMul ℕ (SchwartzMap E F)

instance SchwartzMap.instZSMul {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : SMul ℤ (SchwartzMap E F)

instance SchwartzMap.instZero {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Zero (SchwartzMap E F)

instance SchwartzMap.instInhabited {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Inhabited (SchwartzMap E F)

theorem SchwartzMap.coe_zero {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ↑0 = 0

@[simp]

theorem SchwartzMap.coeFn_zero {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ↑0 = 0

@[simp]

theorem SchwartzMap.zero_apply {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {x : E} : ↑0 x = 0

theorem SchwartzMap.seminormAux_zero {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (n : ℕ) : SchwartzMap.seminormAux k n 0 = 0

instance SchwartzMap.instNeg {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Neg (SchwartzMap E F)

instance SchwartzMap.instAdd {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Add (SchwartzMap E F)

@[simp]

theorem SchwartzMap.add_apply {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : SchwartzMap E F} {g : SchwartzMap E F} {x : E} : ↑(f + g) x = ↑f x + ↑g x

theorem SchwartzMap.seminormAux_add_le {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (n : ℕ) (f : SchwartzMap E F) (g : SchwartzMap E F) : SchwartzMap.seminormAux k n (f + g) ≤ SchwartzMap.seminormAux k n f + SchwartzMap.seminormAux k n g

instance SchwartzMap.instSub {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Sub (SchwartzMap E F)

@[simp]

theorem SchwartzMap.sub_apply {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : SchwartzMap E F} {g : SchwartzMap E F} {x : E} : ↑(f - g) x = ↑f x - ↑g x

instance SchwartzMap.instAddCommGroup {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : AddCommGroup (SchwartzMap E F)

def SchwartzMap.coeHom (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : SchwartzMap E F →+ E → F

Coercion as an additive homomorphism.

theorem SchwartzMap.coe_coeHom {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ↑(SchwartzMap.coeHom E F) = FunLike.coe

theorem SchwartzMap.coeHom_injective {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Function.Injective ↑(SchwartzMap.coeHom E F)

instance SchwartzMap.instModule {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] : Module 𝕜 (SchwartzMap E F)

Seminorms on Schwartz space

def SchwartzMap.seminorm (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (k : ℕ) (n : ℕ) : Seminorm 𝕜 (SchwartzMap E F)

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

theorem SchwartzMap.seminorm_le_bound (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (k : ℕ) (n : ℕ) (f : SchwartzMap E F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (↑f) x‖ ≤ M) : ↑(SchwartzMap.seminorm 𝕜 k n) f ≤ M

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

theorem SchwartzMap.seminorm_le_bound' (𝕜 : Type u_1) {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (k : ℕ) (n : ℕ) (f : SchwartzMap ℝ F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (↑f) x‖ ≤ M) : ↑(SchwartzMap.seminorm 𝕜 k n) f ≤ M

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

Variant for functions 𝓢(ℝ, F).

theorem SchwartzMap.le_seminorm (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (k : ℕ) (n : ℕ) (f : SchwartzMap E F) (x : E) : ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (↑f) x‖ ≤ ↑(SchwartzMap.seminorm 𝕜 k n) f

The seminorm controls the Schwartz estimate for any fixed x.

theorem SchwartzMap.le_seminorm' (𝕜 : Type u_1) {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (k : ℕ) (n : ℕ) (f : SchwartzMap ℝ F) (x : ℝ) : |x| ^ k * ‖iteratedDeriv n (↑f) x‖ ≤ ↑(SchwartzMap.seminorm 𝕜 k n) f

The seminorm controls the Schwartz estimate for any fixed x.

Variant for functions 𝓢(ℝ, F).

theorem SchwartzMap.norm_iteratedFDeriv_le_seminorm (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (n : ℕ) (x₀ : E) : ‖iteratedFDeriv ℝ n (↑f) x₀‖ ≤ ↑(SchwartzMap.seminorm 𝕜 0 n) f

theorem SchwartzMap.norm_pow_mul_le_seminorm (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (k : ℕ) (x₀ : E) : ‖x₀‖ ^ k * ‖↑f x₀‖ ≤ ↑(SchwartzMap.seminorm 𝕜 k 0) f

theorem SchwartzMap.norm_le_seminorm (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (x₀ : E) : ‖↑f x₀‖ ≤ ↑(SchwartzMap.seminorm 𝕜 0 0) f

def schwartzSeminormFamily (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] : SeminormFamily 𝕜 (SchwartzMap E F) (ℕ × ℕ)

The family of Schwartz seminorms.

@[simp]

theorem SchwartzMap.schwartzSeminormFamily_apply (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (n : ℕ) (k : ℕ) : schwartzSeminormFamily 𝕜 E F (n, k) = SchwartzMap.seminorm 𝕜 n k

@[simp]

theorem SchwartzMap.schwartzSeminormFamily_apply_zero (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] : schwartzSeminormFamily 𝕜 E F 0 = SchwartzMap.seminorm 𝕜 0 0

theorem SchwartzMap.one_add_le_sup_seminorm_apply {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {m : ℕ × ℕ} {k : ℕ} {n : ℕ} (hk : k ≤ m.fst) (hn : n ≤ m.snd) (f : SchwartzMap E F) (x : E) : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (↑f) x‖ ≤ ↑(2 ^ m.fst) * ↑(Finset.sup (Finset.Iic m) fun m => SchwartzMap.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

instance SchwartzMap.instTopologicalSpace (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : TopologicalSpace (SchwartzMap E F)

theorem schwartz_withSeminorms (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] : WithSeminorms (schwartzSeminormFamily 𝕜 E F)

instance SchwartzMap.instContinuousSMul {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] : ContinuousSMul 𝕜 (SchwartzMap E F)

instance SchwartzMap.instTopologicalAddGroup {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : TopologicalAddGroup (SchwartzMap E F)

instance SchwartzMap.instUniformSpace {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : UniformSpace (SchwartzMap E F)

instance SchwartzMap.instUniformAddGroup {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : UniformAddGroup (SchwartzMap E F)

instance SchwartzMap.instLocallyConvexSpace {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : LocallyConvexSpace ℝ (SchwartzMap E F)

instance SchwartzMap.instFirstCountableTopology {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : TopologicalSpace.FirstCountableTopology (SchwartzMap E F)

Functions of temperate growth

def Function.HasTemperateGrowth {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) : Prop

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

theorem Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hf_temperate : Function.HasTemperateGrowth f) (n : ℕ) : ∃ k C x, ∀ (N : ℕ), N ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k

Construction of continuous linear maps between Schwartz spaces

def SchwartzMap.mkLM {𝕜 : Type u_1} {𝕜' : Type u_2} {D : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedField 𝕜'] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedSpace 𝕜 E] [SMulCommClass ℝ 𝕜 E] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜' G] [SMulCommClass ℝ 𝕜' G] {σ : 𝕜 →+* 𝕜'} (A : (D → E) → F → G) (hadd : ∀ (f g : SchwartzMap D E) (x : F), A (↑f + ↑g) x = A (↑f) x + A (↑g) x) (hsmul : ∀ (a : 𝕜) (f : SchwartzMap D E) (x : F), A (↑(a • f)) x = ↑σ a • A (↑f) x) (hsmooth : ∀ (f : SchwartzMap D E), ContDiff ℝ ⊤ (A ↑f)) (hbound : ∀ (n : ℕ × ℕ), ∃ s C, 0 ≤ C ∧ ∀ (f : SchwartzMap D E) (x : F), ‖x‖ ^ n.fst * ‖iteratedFDeriv ℝ n.snd (A ↑f) x‖ ≤ C * ↑(Finset.sup s (schwartzSeminormFamily 𝕜 D E)) f) : SchwartzMap D E →ₛₗ[σ] SchwartzMap F G

Create a semilinear map between Schwartz spaces.

Note: This is a helper definition for mkCLM.

def SchwartzMap.mkCLM {𝕜 : Type u_1} {𝕜' : Type u_2} {D : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedField 𝕜'] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedSpace 𝕜 E] [SMulCommClass ℝ 𝕜 E] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜' G] [SMulCommClass ℝ 𝕜' G] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] (A : (D → E) → F → G) (hadd : ∀ (f g : SchwartzMap D E) (x : F), A (↑f + ↑g) x = A (↑f) x + A (↑g) x) (hsmul : ∀ (a : 𝕜) (f : SchwartzMap D E) (x : F), A (↑(a • f)) x = ↑σ a • A (↑f) x) (hsmooth : ∀ (f : SchwartzMap D E), ContDiff ℝ ⊤ (A ↑f)) (hbound : ∀ (n : ℕ × ℕ), ∃ s C, 0 ≤ C ∧ ∀ (f : SchwartzMap D E) (x : F), ‖x‖ ^ n.fst * ‖iteratedFDeriv ℝ n.snd (A ↑f) x‖ ≤ C * ↑(Finset.sup s (schwartzSeminormFamily 𝕜 D E)) f) : SchwartzMap D E →SL[σ] SchwartzMap F G

Create a continuous semilinear map between Schwartz spaces.

For an example of using this definition, see fderivCLM.

def SchwartzMap.evalCLM {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (m : E) : SchwartzMap E (E →L[ℝ] F) →L[𝕜] SchwartzMap E F

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

def SchwartzMap.bilinLeftCLM {D : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) {g : D → F} (hg : Function.HasTemperateGrowth g) : SchwartzMap D E →L[ℝ] SchwartzMap 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.

def SchwartzMap.compCLM (𝕜 : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {g : D → E} (hg : Function.HasTemperateGrowth g) (hg_upper : ∃ k C, ∀ (x : D), ‖x‖ ≤ C * (1 + ‖g x‖) ^ k) : SchwartzMap E F →L[𝕜] SchwartzMap 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.

Derivatives of Schwartz functions

def SchwartzMap.fderivCLM (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] : SchwartzMap E F →L[𝕜] SchwartzMap E (E →L[ℝ] F)

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

@[simp]

theorem SchwartzMap.fderivCLM_apply (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (x : E) : ↑(↑(SchwartzMap.fderivCLM 𝕜) f) x = fderiv ℝ (↑f) x

def SchwartzMap.derivCLM (𝕜 : Type u_1) {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] : SchwartzMap ℝ F →L[𝕜] SchwartzMap ℝ F

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

@[simp]

theorem SchwartzMap.derivCLM_apply (𝕜 : Type u_1) {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (f : SchwartzMap ℝ F) (x : ℝ) : ↑(↑(SchwartzMap.derivCLM 𝕜) f) x = deriv (↑f) x

def SchwartzMap.pderivCLM (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (m : E) : SchwartzMap E F →L[𝕜] SchwartzMap E F

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

@[simp]

theorem SchwartzMap.pderivCLM_apply (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (m : E) (f : SchwartzMap E F) (x : E) : ↑(↑(SchwartzMap.pderivCLM 𝕜 m) f) x = ↑(fderiv ℝ (↑f) x) m

def SchwartzMap.iteratedPDeriv (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {n : ℕ} : (Fin n → E) → SchwartzMap E F →L[𝕜] SchwartzMap E F

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

@[simp]

theorem SchwartzMap.iteratedPDeriv_zero (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (m : Fin 0 → E) (f : SchwartzMap E F) : ↑(SchwartzMap.iteratedPDeriv 𝕜 m) f = f

@[simp]

theorem SchwartzMap.iteratedPDeriv_one (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (m : Fin 1 → E) (f : SchwartzMap E F) : ↑(SchwartzMap.iteratedPDeriv 𝕜 m) f = ↑(SchwartzMap.pderivCLM 𝕜 (m 0)) f

theorem SchwartzMap.iteratedPDeriv_succ_left (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {n : ℕ} (m : Fin (n + 1) → E) (f : SchwartzMap E F) : ↑(SchwartzMap.iteratedPDeriv 𝕜 m) f = ↑(SchwartzMap.pderivCLM 𝕜 (m 0)) (↑(SchwartzMap.iteratedPDeriv 𝕜 (Fin.tail m)) f)

theorem SchwartzMap.iteratedPDeriv_succ_right (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {n : ℕ} (m : Fin (n + 1) → E) (f : SchwartzMap E F) : ↑(SchwartzMap.iteratedPDeriv 𝕜 m) f = ↑(SchwartzMap.iteratedPDeriv 𝕜 (Fin.init m)) (↑(SchwartzMap.pderivCLM 𝕜 (m (Fin.last n))) f)

Inclusion into the space of bounded continuous functions

def SchwartzMap.toBoundedContinuousFunction {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) : BoundedContinuousFunction E F

Schwartz functions as bounded continuous functions

@[simp]

theorem SchwartzMap.toBoundedContinuousFunction_apply {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) (x : E) : ↑(SchwartzMap.toBoundedContinuousFunction f) x = ↑f x

def SchwartzMap.toContinuousMap {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) : C(E, F)

Schwartz functions as continuous functions

def SchwartzMap.toBoundedContinuousFunctionLM (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] : SchwartzMap E F →ₗ[𝕜] BoundedContinuousFunction E F

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

@[simp]

theorem SchwartzMap.toBoundedContinuousFunctionLM_apply (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (x : E) : ↑(↑(SchwartzMap.toBoundedContinuousFunctionLM 𝕜 E F) f) x = ↑f x

def SchwartzMap.toBoundedContinuousFunctionCLM (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] : SchwartzMap E F →L[𝕜] BoundedContinuousFunction E F

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

@[simp]

theorem SchwartzMap.toBoundedContinuousFunctionCLM_apply (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (x : E) : ↑(↑(SchwartzMap.toBoundedContinuousFunctionCLM 𝕜 E F) f) x = ↑f x

def SchwartzMap.delta (𝕜 : Type u_1) {E : Type u_4} (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (x : E) : SchwartzMap E F →L[𝕜] F

The Dirac delta distribution

@[simp]

theorem SchwartzMap.delta_apply (𝕜 : Type u_1) {E : Type u_4} (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsROrC 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (x₀ : E) (f : SchwartzMap E F) : ↑(SchwartzMap.delta 𝕜 F x₀) f = ↑f x₀