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)
• SchwartzMap.integralCLM: Integration 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)

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

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

theorem SchwartzMap.smooth' {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (self : SchwartzMap E F) : ContDiff ℝ ⊤ self.toFun

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• SchwartzMap.instFunLike = { coe := fun (f : SchwartzMap E F) => f.toFun, coe_injective' := ⋯ }

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.

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

Equations

• ⋯ = ⋯

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 : E) => ‖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 : E) => ‖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 : E) => ‖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.

Equations

• SchwartzMap.seminormAux k n f = sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}

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)

Equations

• SchwartzMap.instSMul = { smul := fun (c : 𝕜) (f : SchwartzMap E F) => { toFun := c • ⇑f, smooth' := ⋯, decay' := ⋯ } }

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

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• SchwartzMap.instNSMul = { smul := fun (c : ℕ) (f : SchwartzMap E F) => { toFun := c • ⇑f, smooth' := ⋯, decay' := ⋯ } }

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

Equations

• SchwartzMap.instZSMul = { smul := fun (c : ℤ) (f : SchwartzMap E F) => { toFun := c • ⇑f, smooth' := ⋯, decay' := ⋯ } }

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

Equations

• SchwartzMap.instZero = { zero := { toFun := fun (x : E) => 0, smooth' := ⋯, decay' := ⋯ } }

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

Equations

• SchwartzMap.instInhabited = { default := 0 }

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)

Equations

• SchwartzMap.instNeg = { neg := fun (f : SchwartzMap E F) => { toFun := -⇑f, smooth' := ⋯, decay' := ⋯ } }

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

Equations

• SchwartzMap.instAdd = { add := fun (f g : SchwartzMap E F) => { toFun := ⇑f + ⇑g, smooth' := ⋯, decay' := ⋯ } }

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

Equations

• SchwartzMap.instSub = { sub := fun (f g : SchwartzMap E F) => { toFun := ⇑f - ⇑g, smooth' := ⋯, decay' := ⋯ } }

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

Equations

• SchwartzMap.instAddCommGroup = Function.Injective.addCommGroup (fun (f : SchwartzMap E F) => ⇑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.

Equations

• SchwartzMap.coeHom E F = { toFun := fun (f : SchwartzMap E F) => ⇑f, map_zero' := ⋯, map_add' := ⋯ }

theorem SchwartzMap.coe_coeHom {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ⇑(SchwartzMap.coeHom E F) = DFunLike.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)

Equations

• SchwartzMap.instModule = Function.Injective.module 𝕜 (SchwartzMap.coeHom 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).

Equations

• SchwartzMap.seminorm 𝕜 k n = Seminorm.ofSMulLE (SchwartzMap.seminormAux k n) ⋯ ⋯ ⋯

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.

Equations

• schwartzSeminormFamily 𝕜 E F m = SchwartzMap.seminorm 𝕜 m.1 m.2

@[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.1) (hn : n ≤ m.2) (f : SchwartzMap E F) (x : E) : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ 2 ^ m.1 * ((Finset.Iic m).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm 𝕜 m.1 m.2) 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)

Equations

• SchwartzMap.instTopologicalSpace E F = (schwartzSeminormFamily ℝ E F).moduleFilterBasis.topology'

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)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• SchwartzMap.instUniformSpace = (schwartzSeminormFamily ℝ E F).addGroupFilterBasis.uniformSpace

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.

Equations

• Function.HasTemperateGrowth f = (ContDiff ℝ ⊤ f ∧ ∀ (n : ℕ), ∃ (k : ℕ) (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C * (1 + ‖x‖) ^ k)

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 : ℝ), 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k

theorem Function.HasTemperateGrowth.of_fderiv {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (h'f : Function.HasTemperateGrowth (fderiv ℝ f)) (hf : Differentiable ℝ f) {k : ℕ} {C : ℝ} (h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k) : Function.HasTemperateGrowth f

theorem Function.HasTemperateGrowth.zero {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Function.HasTemperateGrowth fun (x : E) => 0

theorem Function.HasTemperateGrowth.const {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : F) : Function.HasTemperateGrowth fun (x : E) => c

theorem ContinuousLinearMap.hasTemperateGrowth {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E →L[ℝ] F) : Function.HasTemperateGrowth ⇑f

class MeasureTheory.Measure.HasTemperateGrowth {D : Type u_3} [NormedAddCommGroup D] [MeasurableSpace D] (μ : MeasureTheory.Measure D) : Prop

A measure μ has temperate growth if there is an n : ℕ such that (1 + ‖x‖) ^ (- n) is μ-integrable.

• exists_integrable : ∃ (n : ℕ), MeasureTheory.Integrable (fun (x : D) => (1 + ‖x‖) ^ (-↑n)) μ

theorem MeasureTheory.Measure.HasTemperateGrowth.exists_integrable {D : Type u_3} : ∀ {inst : NormedAddCommGroup D} {inst_1 : MeasurableSpace D} {μ : MeasureTheory.Measure D} [self : μ.HasTemperateGrowth], ∃ (n : ℕ), MeasureTheory.Integrable (fun (x : D) => (1 + ‖x‖) ^ (-↑n)) μ

def MeasureTheory.Measure.integrablePower {D : Type u_3} [NormedAddCommGroup D] [MeasurableSpace D] (μ : MeasureTheory.Measure D) : ℕ

An integer exponent l such that (1 + ‖x‖) ^ (-l) is integrable if μ has temperate growth.

Equations

• μ.integrablePower = if h : μ.HasTemperateGrowth then ⋯.choose else 0

theorem SchwartzMap.integrable_pow_neg_integrablePower {D : Type u_3} [NormedAddCommGroup D] [MeasurableSpace D] (μ : MeasureTheory.Measure D) [h : μ.HasTemperateGrowth] : MeasureTheory.Integrable (fun (x : D) => (1 + ‖x‖) ^ (-↑μ.integrablePower)) μ

instance MeasureTheory.Measure.IsFiniteMeasure.instHasTemperateGrowth {D : Type u_3} [NormedAddCommGroup D] [MeasurableSpace D] {μ : MeasureTheory.Measure D} [h : MeasureTheory.IsFiniteMeasure μ] : μ.HasTemperateGrowth

Equations

• ⋯ = ⋯

instance MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth {D : Type u_3} [NormedAddCommGroup D] [MeasurableSpace D] [NormedSpace ℝ D] [FiniteDimensional ℝ D] [BorelSpace D] {μ : MeasureTheory.Measure D} [h : μ.IsAddHaarMeasure] : μ.HasTemperateGrowth

Equations

• ⋯ = ⋯

theorem SchwartzMap.pow_mul_le_of_le_of_pow_mul_le {C₁ : ℝ} {C₂ : ℝ} {k : ℕ} {l : ℕ} {x : ℝ} {f : ℝ} (hx : 0 ≤ x) (hf : 0 ≤ f) (h₁ : f ≤ C₁) (h₂ : x ^ (k + l) * f ≤ C₂) : x ^ k * f ≤ 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l)

Pointwise inequality to control x ^ k * f in terms of 1 / (1 + x) ^ l if one controls both f (with a bound C₁) and x ^ (k + l) * f (with a bound C₂). This will be used to check integrability of x ^ k * f x when f is a Schwartz function, and to control explicitly its integral in terms of suitable seminorms of f.

theorem SchwartzMap.integrable_of_le_of_pow_mul_le {D : Type u_3} [NormedAddCommGroup D] [MeasurableSpace D] [BorelSpace D] [SecondCountableTopology D] {E : Type u_8} [NormedAddCommGroup E] {μ : MeasureTheory.Measure D} [μ.HasTemperateGrowth] {f : D → E} {C₁ : ℝ} {C₂ : ℝ} {k : ℕ} (hf : ∀ (x : D), ‖f x‖ ≤ C₁) (h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂) (h''f : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.Integrable (fun (x : D) => ‖x‖ ^ k * ‖f x‖) μ

Given a function such that f and x ^ (k + l) * f are bounded for a suitable l, then x ^ k * f is integrable. The bounds are not relevant for the integrability conclusion, but they are relevant for bounding the integral in integral_pow_mul_le_of_le_of_pow_mul_le. We formulate the two lemmas with the same set of assumptions for ease of applications.

theorem SchwartzMap.integral_pow_mul_le_of_le_of_pow_mul_le {D : Type u_3} [NormedAddCommGroup D] [MeasurableSpace D] {E : Type u_8} [NormedAddCommGroup E] {μ : MeasureTheory.Measure D} [μ.HasTemperateGrowth] {f : D → E} {C₁ : ℝ} {C₂ : ℝ} {k : ℕ} (hf : ∀ (x : D), ‖f x‖ ≤ C₁) (h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂) : ∫ (x : D), ‖x‖ ^ k * ‖f x‖ ∂μ ≤ (2 ^ μ.integrablePower * ∫ (x : D), (1 + ‖x‖) ^ (-↑μ.integrablePower) ∂μ) * (C₁ + C₂)

Given a function such that f and x ^ (k + l) * f are bounded for a suitable l, then one can bound explicitly the integral of x ^ k * f.

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 : Finset (ℕ × ℕ)) (C : ℝ), 0 ≤ C ∧ ∀ (f : SchwartzMap D E) (x : F), ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (A ⇑f) x‖ ≤ C * (s.sup (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.

Equations

• SchwartzMap.mkLM A hadd hsmul hsmooth hbound = { toFun := fun (f : SchwartzMap D E) => { toFun := A ⇑f, smooth' := ⋯, decay' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

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 : Finset (ℕ × ℕ)) (C : ℝ), 0 ≤ C ∧ ∀ (f : SchwartzMap D E) (x : F), ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (A ⇑f) x‖ ≤ C * (s.sup (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.

Equations

• SchwartzMap.mkCLM A hadd hsmul hsmooth hbound = { toLinearMap := SchwartzMap.mkLM A hadd hsmul hsmooth hbound, cont := ⋯ }

def SchwartzMap.mkCLMtoNormedSpace {𝕜 : Type u_1} {𝕜' : Type u_2} {D : Type u_3} {E : Type u_4} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedField 𝕜] [NormedField 𝕜'] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedSpace 𝕜 E] [SMulCommClass ℝ 𝕜 E] [NormedAddCommGroup G] [NormedSpace 𝕜' G] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] (A : SchwartzMap D E → G) (hadd : ∀ (f g : SchwartzMap D E), A (f + g) = A f + A g) (hsmul : ∀ (a : 𝕜) (f : SchwartzMap D E), A (a • f) = σ a • A f) (hbound : ∃ (s : Finset (ℕ × ℕ)) (C : ℝ), 0 ≤ C ∧ ∀ (f : SchwartzMap D E), ‖A f‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f) : SchwartzMap D E →SL[σ] G

Define a continuous semilinear map from Schwartz space to a normed space.

Equations

• SchwartzMap.mkCLMtoNormedSpace A hadd hsmul hbound = { toFun := fun (x : SchwartzMap D E) => A x, map_add' := hadd, map_smul' := hsmul, cont := ⋯ }

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.

Equations

• SchwartzMap.evalCLM m = SchwartzMap.mkCLM (fun (f : E → E →L[ℝ] F) (x : E) => (f x) m) ⋯ ⋯ ⋯ ⋯

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.

Equations

• SchwartzMap.bilinLeftCLM B hg = SchwartzMap.mkCLM (fun (f : D → E) (x : D) => (B (f x)) (g x)) ⋯ ⋯ ⋯ ⋯

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] [RCLike 𝕜] [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.

Equations

• SchwartzMap.compCLM 𝕜 hg hg_upper = SchwartzMap.mkCLM (fun (f : E → F) (x : D) => f (g x)) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem SchwartzMap.compCLM_apply (𝕜 : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [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) (f : SchwartzMap E F) : ⇑((SchwartzMap.compCLM 𝕜 hg hg_upper) f) = ⇑f ∘ g

def SchwartzMap.compCLMOfAntilipschitz (𝕜 : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {K : NNReal} {g : D → E} (hg : Function.HasTemperateGrowth g) (h'g : AntilipschitzWith K g) : 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 antilipschitz.

Equations

• SchwartzMap.compCLMOfAntilipschitz 𝕜 hg h'g = SchwartzMap.compCLM 𝕜 hg ⋯

@[simp]

theorem SchwartzMap.compCLMOfAntilipschitz_apply (𝕜 : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {K : NNReal} {g : D → E} (hg : Function.HasTemperateGrowth g) (h'g : AntilipschitzWith K g) (f : SchwartzMap E F) : ⇑((SchwartzMap.compCLMOfAntilipschitz 𝕜 hg h'g) f) = ⇑f ∘ g

def SchwartzMap.compCLMOfContinuousLinearEquiv (𝕜 : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (g : D ≃L[ℝ] E) : SchwartzMap E F →L[𝕜] SchwartzMap D F

Composition with a continuous linear equiv on the right is a continuous linear map on Schwartz space.

Equations

• SchwartzMap.compCLMOfContinuousLinearEquiv 𝕜 g = SchwartzMap.compCLMOfAntilipschitz 𝕜 ⋯ ⋯

@[simp]

theorem SchwartzMap.compCLMOfContinuousLinearEquiv_apply (𝕜 : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (g : D ≃L[ℝ] E) (f : SchwartzMap E F) : ⇑((SchwartzMap.compCLMOfContinuousLinearEquiv 𝕜 g) f) = ⇑f ∘ ⇑g

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] [RCLike 𝕜] [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.

Equations

• SchwartzMap.fderivCLM 𝕜 = SchwartzMap.mkCLM (fderiv ℝ) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem SchwartzMap.fderivCLM_apply (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [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] [RCLike 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] : SchwartzMap ℝ F →L[𝕜] SchwartzMap ℝ F

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

Equations

• SchwartzMap.derivCLM 𝕜 = SchwartzMap.mkCLM deriv ⋯ ⋯ ⋯ ⋯

@[simp]

theorem SchwartzMap.derivCLM_apply (𝕜 : Type u_1) {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [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] [RCLike 𝕜] [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.

Equations

• SchwartzMap.pderivCLM 𝕜 m = (SchwartzMap.evalCLM m).comp (SchwartzMap.fderivCLM 𝕜)

@[simp]

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

theorem SchwartzMap.pderivCLM_eq_lineDeriv (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (m : E) (f : SchwartzMap E F) (x : E) : ((SchwartzMap.pderivCLM 𝕜 m) f) x = lineDeriv ℝ (⇑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] [RCLike 𝕜] [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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SchwartzMap.iteratedPDeriv_zero (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [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] [RCLike 𝕜] [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] [RCLike 𝕜] [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] [RCLike 𝕜] [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)

theorem SchwartzMap.iteratedPDeriv_eq_iteratedFDeriv (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {n : ℕ} {m : Fin n → E} {f : SchwartzMap E F} {x : E} : ((SchwartzMap.iteratedPDeriv 𝕜 m) f) x = (iteratedFDeriv ℝ n (⇑f) x) m

Integration

theorem SchwartzMap.integral_pow_mul_iteratedFDeriv_le (𝕜 : Type u_1) {D : Type u_3} {V : Type u_7} [RCLike 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedSpace 𝕜 V] [MeasurableSpace D] (μ : MeasureTheory.Measure D) [hμ : μ.HasTemperateGrowth] (f : SchwartzMap D V) (k : ℕ) (n : ℕ) : ∫ (x : D), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ∂μ ≤ (2 ^ μ.integrablePower * ∫ (x : D), (1 + ‖x‖) ^ (-↑μ.integrablePower) ∂μ) * ((SchwartzMap.seminorm 𝕜 0 n) f + (SchwartzMap.seminorm 𝕜 (k + μ.integrablePower) n) f)

theorem SchwartzMap.integrable_pow_mul_iteratedFDeriv {D : Type u_3} {V : Type u_7} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] [MeasurableSpace D] (μ : MeasureTheory.Measure D) [hμ : μ.HasTemperateGrowth] [BorelSpace D] [SecondCountableTopology D] (f : SchwartzMap D V) (k : ℕ) (n : ℕ) : MeasureTheory.Integrable (fun (x : D) => ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖) μ

theorem SchwartzMap.integrable_pow_mul {D : Type u_3} {V : Type u_7} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] [MeasurableSpace D] (μ : MeasureTheory.Measure D) [hμ : μ.HasTemperateGrowth] [BorelSpace D] [SecondCountableTopology D] (f : SchwartzMap D V) (k : ℕ) : MeasureTheory.Integrable (fun (x : D) => ‖x‖ ^ k * ‖f x‖) μ

theorem SchwartzMap.integrable {D : Type u_3} {V : Type u_7} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] [MeasurableSpace D] {μ : MeasureTheory.Measure D} [hμ : μ.HasTemperateGrowth] [BorelSpace D] [SecondCountableTopology D] (f : SchwartzMap D V) : MeasureTheory.Integrable (⇑f) μ

def SchwartzMap.integralCLM (𝕜 : Type u_1) {D : Type u_3} {V : Type u_7} [RCLike 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedSpace 𝕜 V] [MeasurableSpace D] (μ : MeasureTheory.Measure D) [hμ : μ.HasTemperateGrowth] [BorelSpace D] [SecondCountableTopology D] : SchwartzMap D V →L[𝕜] V

The integral as a continuous linear map from Schwartz space to the codomain.

Equations

• SchwartzMap.integralCLM 𝕜 μ = SchwartzMap.mkCLMtoNormedSpace (fun (x : SchwartzMap D V) => ∫ (x_1 : D), x x_1 ∂μ) ⋯ ⋯ ⋯

@[simp]

theorem SchwartzMap.integralCLM_apply (𝕜 : Type u_1) {D : Type u_3} {V : Type u_7} [RCLike 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedSpace 𝕜 V] [MeasurableSpace D] {μ : MeasureTheory.Measure D} [hμ : μ.HasTemperateGrowth] [BorelSpace D] [SecondCountableTopology D] (f : SchwartzMap D V) : (SchwartzMap.integralCLM 𝕜 μ) f = ∫ (x : D), f x ∂μ

Inclusion into the space of bounded continuous functions

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

Equations

• ⋯ = ⋯

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

Equations

• f.toBoundedContinuousFunction = BoundedContinuousFunction.ofNormedAddCommGroup ⇑f ⋯ ((SchwartzMap.seminorm ℝ 0 0) f) ⋯

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

Equations

• f.toContinuousMap = f.toBoundedContinuousFunction.toContinuousMap

def SchwartzMap.toBoundedContinuousFunctionCLM (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [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.

Equations

• SchwartzMap.toBoundedContinuousFunctionCLM 𝕜 E F = SchwartzMap.mkCLMtoNormedSpace SchwartzMap.toBoundedContinuousFunction ⋯ ⋯ ⋯

@[simp]

theorem SchwartzMap.toBoundedContinuousFunctionCLM_apply (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [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] [RCLike 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (x : E) : SchwartzMap E F →L[𝕜] F

The Dirac delta distribution

Equations

• SchwartzMap.delta 𝕜 F x = (BoundedContinuousFunction.evalCLM 𝕜 x).comp (SchwartzMap.toBoundedContinuousFunctionCLM 𝕜 E F)

@[simp]

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

@[simp]

theorem SchwartzMap.integralCLM_dirac_eq_delta (𝕜 : Type u_1) {E : Type u_4} (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace F] (x : E) : SchwartzMap.integralCLM 𝕜 (MeasureTheory.Measure.dirac x) = SchwartzMap.delta 𝕜 F x

Integrating against the Dirac measure is equal to the delta distribution.

instance SchwartzMap.instZeroAtInftyContinuousMapClass {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [ProperSpace E] : ZeroAtInftyContinuousMapClass (SchwartzMap E F) E F

Equations

• ⋯ = ⋯

def SchwartzMap.toZeroAtInfty {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [ProperSpace E] (f : SchwartzMap E F) : ZeroAtInftyContinuousMap E F

Schwartz functions as continuous functions vanishing at infinity.

Equations

• f.toZeroAtInfty = { toFun := ⇑f, continuous_toFun := ⋯, zero_at_infty' := ⋯ }

@[simp]

theorem SchwartzMap.toZeroAtInfty_apply {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [ProperSpace E] (f : SchwartzMap E F) (x : E) : f.toZeroAtInfty x = f x

@[simp]

theorem SchwartzMap.toZeroAtInfty_toBCF {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [ProperSpace E] (f : SchwartzMap E F) : f.toZeroAtInfty.toBCF = f.toBoundedContinuousFunction

def SchwartzMap.toZeroAtInftyCLM (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [ProperSpace E] [RCLike 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] : SchwartzMap E F →L[𝕜] ZeroAtInftyContinuousMap E F

The inclusion map from Schwartz functions to continuous functions vanishing at infinity as a continuous linear map.

Equations

• SchwartzMap.toZeroAtInftyCLM 𝕜 E F = SchwartzMap.mkCLMtoNormedSpace SchwartzMap.toZeroAtInfty ⋯ ⋯ ⋯

@[simp]

theorem SchwartzMap.toZeroAtInftyCLM_apply (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [ProperSpace E] [RCLike 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (x : E) : ((SchwartzMap.toZeroAtInftyCLM 𝕜 E F) f) x = f x