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.compCLM: Composition with a function on the right as a continuous linear map 𝓢(E, F) →L[𝕜] 𝓢(D, F), provided that the function is temperate and grows polynomially near infinity
• 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.instIsUniformAddGroup 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

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‖.

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

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

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 g : SchwartzMap E F} (h : ∀ (x : E), f x = g x) : f = g

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

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 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 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 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 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] : ⇑(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 ⇑(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.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)

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.instIsTopologicalAddGroup {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : IsTopologicalAddGroup (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.instIsUniformAddGroup {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : IsUniformAddGroup (SchwartzMap E F)

@[deprecated SchwartzMap.instIsUniformAddGroup (since := "2025-03-31")]

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

Alias of SchwartzMap.instIsUniformAddGroup.

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] : 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 : 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 : HasTemperateGrowth (fderiv ℝ f)) (hf : Differentiable ℝ f) {k : ℕ} {C : ℝ} (h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k) : HasTemperateGrowth f

theorem Function.HasTemperateGrowth.zero {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : 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) : 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] (μ : Measure D) : Prop

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

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

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

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

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] {μ : Measure D} [h : IsFiniteMeasure μ] : μ.HasTemperateGrowth

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

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.

theorem MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_top {D : Type u_3} [NormedAddCommGroup D] [MeasurableSpace D] (p : ENNReal) {μ : Measure D} (hμ : μ.HasTemperateGrowth) : ∃ (k : ℕ), eLpNorm (fun (x : D) => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤

For any HasTemperateGrowth measure and p, there exists an integer power k such that (1 + ‖x‖) ^ (-k) is in L^p.

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.

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.

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.

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 {𝕜 : Type u_1} {D : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [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] [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.

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

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

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

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

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

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

@[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) : (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) : (iteratedPDeriv 𝕜 m) f = (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) : (iteratedPDeriv 𝕜 m) f = (pderivCLM 𝕜 (m 0)) ((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) : (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((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} : ((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.

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

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

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.

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

@[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) : (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) : integralCLM 𝕜 (MeasureTheory.Measure.dirac x) = 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

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.

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

@[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) : ((toZeroAtInftyCLM 𝕜 E F) f) x = f x

Inclusion into L^p space

theorem SchwartzMap.eLpNorm_le_seminorm (𝕜 : Type u_1) {E : Type u_4} (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (p : ENNReal) (μ : MeasureTheory.Measure E := by volume_tac) [hμ : MeasureTheory.Measure.HasTemperateGrowth μ] : ∃ (k : ℕ) (C : NNReal), ∀ (f : SchwartzMap E F), MeasureTheory.eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

The L^p norm of a Schwartz function is controlled by a finite family of Schwartz seminorms.

The maximum index k and the constant C depend on p and μ.

theorem SchwartzMap.eLpNorm_lt_top {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] (f : SchwartzMap E F) (p : ENNReal) (μ : MeasureTheory.Measure E := by volume_tac) [hμ : MeasureTheory.Measure.HasTemperateGrowth μ] : MeasureTheory.eLpNorm (⇑f) p μ < ⊤

The L^p norm of a Schwartz function is finite.

theorem SchwartzMap.memLp_top {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F] (f : SchwartzMap E F) (μ : MeasureTheory.Measure E := by volume_tac) : MeasureTheory.MemLp ⇑f ⊤ μ

Schwartz functions are in L^∞; does not require hμ.HasTemperateGrowth.

@[deprecated SchwartzMap.memLp_top (since := "2025-02-21")]

theorem SchwartzMap.memℒp_top {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F] (f : SchwartzMap E F) (μ : MeasureTheory.Measure E := by volume_tac) : MeasureTheory.MemLp ⇑f ⊤ μ

Alias of SchwartzMap.memLp_top.

---

Schwartz functions are in L^∞; does not require hμ.HasTemperateGrowth.

theorem SchwartzMap.memLp {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F] (f : SchwartzMap E F) (p : ENNReal) (μ : MeasureTheory.Measure E := by volume_tac) [hμ : MeasureTheory.Measure.HasTemperateGrowth μ] : MeasureTheory.MemLp (⇑f) p μ

Schwartz functions are in L^p for any p.

@[deprecated SchwartzMap.memLp (since := "2025-02-21")]

theorem SchwartzMap.memℒp {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F] (f : SchwartzMap E F) (p : ENNReal) (μ : MeasureTheory.Measure E := by volume_tac) [hμ : MeasureTheory.Measure.HasTemperateGrowth μ] : MeasureTheory.MemLp (⇑f) p μ

Alias of SchwartzMap.memLp.

---

Schwartz functions are in L^p for any p.

def SchwartzMap.toLp {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F] (f : SchwartzMap E F) (p : ENNReal) (μ : MeasureTheory.Measure E := by volume_tac) [hμ : MeasureTheory.Measure.HasTemperateGrowth μ] : ↥(MeasureTheory.Lp F p μ)

Map a Schwartz function to an Lp function for any p.

theorem SchwartzMap.coeFn_toLp {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F] (f : SchwartzMap E F) (p : ENNReal) (μ : MeasureTheory.Measure E := by volume_tac) [hμ : MeasureTheory.Measure.HasTemperateGrowth μ] : ↑↑(f.toLp p μ) =ᵐ[μ] ⇑f

theorem SchwartzMap.norm_toLp {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F] {f : SchwartzMap E F} {p : ENNReal} {μ : MeasureTheory.Measure E} [hμ : μ.HasTemperateGrowth] : ‖f.toLp p μ‖ = (MeasureTheory.eLpNorm (⇑f) p μ).toReal

theorem SchwartzMap.injective_toLp {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F] (p : ENNReal) (μ : MeasureTheory.Measure E := by volume_tac) [hμ : MeasureTheory.Measure.HasTemperateGrowth μ] [MeasureTheory.Measure.IsOpenPosMeasure μ] : Function.Injective fun (f : SchwartzMap E F) => f.toLp p μ

theorem SchwartzMap.norm_toLp_le_seminorm (𝕜 : Type u_1) {E : Type u_4} (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [SecondCountableTopologyEither E F] (p : ENNReal) (μ : MeasureTheory.Measure E := by volume_tac) [hμ : MeasureTheory.Measure.HasTemperateGrowth μ] : ∃ (k : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ (f : SchwartzMap E F), ‖f.toLp p μ‖ ≤ C * ((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f

def SchwartzMap.toLpCLM (𝕜 : Type u_1) {E : Type u_4} (F : Type u_5) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [SecondCountableTopologyEither E F] (p : ENNReal) [Fact (1 ≤ p)] (μ : MeasureTheory.Measure E := by volume_tac) [hμ : MeasureTheory.Measure.HasTemperateGrowth μ] : SchwartzMap E F →L[𝕜] ↥(MeasureTheory.Lp F p μ)

Continuous linear map from Schwartz functions to L^p.

@[simp]

theorem SchwartzMap.toLpCLM_apply {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [SecondCountableTopologyEither E F] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure E} [hμ : μ.HasTemperateGrowth] {f : SchwartzMap E F} : (toLpCLM 𝕜 F p μ) f = f.toLp p μ

theorem SchwartzMap.continuous_toLp {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure E} [hμ : μ.HasTemperateGrowth] : Continuous fun (f : SchwartzMap E F) => f.toLp p μ