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.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_5) (F : Type u_6) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Type (max u_5 u_6)

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

• toFun : E → F

  The underlying function.

  Do NOT use directly. Use the coercion instead.

• 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_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : FunLike (SchwartzMap E F) E F

theorem SchwartzMap.decay {E : Type u_5} {F : Type u_6} [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_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) (n : ℕ∞) : ContDiff ℝ ↑n ⇑f

Every Schwartz function is smooth.

theorem SchwartzMap.contDiffAt {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) (n : ℕ∞) {x : E} : ContDiffAt ℝ (↑n) (⇑f) x

Every Schwartz function is smooth at any point.

theorem SchwartzMap.continuous {E : Type u_5} {F : Type u_6} [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_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ContinuousMapClass (SchwartzMap E F) E F

theorem SchwartzMap.differentiable {E : Type u_5} {F : Type u_6} [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_5} {F : Type u_6} [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_5} {F : Type u_6} [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_5} {F : Type u_6} [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_5} {F : Type u_6} [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_5} {F : Type u_6} [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_5} {F : Type u_6} [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.tendsto_cocompact {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [ProperSpace E] (f : SchwartzMap E F) : Filter.Tendsto (⇑f) (Filter.cocompact E) (nhds 0)

Algebraic properties

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

@[simp]

theorem SchwartzMap.smul_apply {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [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_2} {𝕜' : Type u_3} {E : Type u_5} {F : Type u_6} [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_2} {𝕜' : Type u_3} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass ℝ 𝕜' F] [SMulCommClass 𝕜 𝕜' F] : SMulCommClass 𝕜 𝕜' (SchwartzMap E F)

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

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

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem SchwartzMap.neg_apply {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) (x : E) : (-f) x = -f x

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

@[simp]

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

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

@[simp]

theorem SchwartzMap.sub_apply {E : Type u_5} {F : Type u_6} [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_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : AddCommGroup (SchwartzMap E F)

@[simp]

theorem SchwartzMap.sum_apply {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ι : Type u_10} (s : Finset ι) (f : ι → SchwartzMap E F) (x : E) : (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x

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

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

instance SchwartzMap.instModule {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [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_2) {E : Type u_5} {F : Type u_6} [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_apply (𝕜 : Type u_2) {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] {k n : ℕ} (f : SchwartzMap E F) : (SchwartzMap.seminorm 𝕜 k n) f = sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}

The seminorm is given by infimum over all c such that the estimate ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ c holds.

Note that it is usually better to use seminorm_le_bound or le_seminorm instead of this lemma.

theorem SchwartzMap.seminorm_le_bound (𝕜 : Type u_2) {E : Type u_5} {F : Type u_6} [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_2) {F : Type u_6} [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_2) {E : Type u_5} {F : Type u_6} [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_2) {F : Type u_6} [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_2) {E : Type u_5} {F : Type u_6} [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_2) {E : Type u_5} {F : Type u_6} [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_2) {E : Type u_5} {F : Type u_6} [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_2) (E : Type u_5) (F : Type u_6) [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_2) (E : Type u_5) (F : Type u_6) [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_2) (E : Type u_5) (F : Type u_6) [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_2} {E : Type u_5} {F : Type u_6} [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_5) (F : Type u_6) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : TopologicalSpace (SchwartzMap E F)

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

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

instance SchwartzMap.instIsTopologicalAddGroup {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : IsTopologicalAddGroup (SchwartzMap E F)

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

instance SchwartzMap.instIsUniformAddGroup {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : IsUniformAddGroup (SchwartzMap E F)

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

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

theorem SchwartzMap.hasTemperateGrowth {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) : Function.HasTemperateGrowth ⇑f

def HasCompactSupport.toSchwartzMap {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (h₁ : HasCompactSupport f) (h₂ : ContDiff ℝ (↑⊤) f) : SchwartzMap E F

A smooth compactly supported function is a Schwartz function.

@[simp]

theorem HasCompactSupport.toSchwartzMap_toFun {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (h₁ : HasCompactSupport f) (h₂ : ContDiff ℝ (↑⊤) f) (a✝ : E) : (h₁.toSchwartzMap h₂) a✝ = f a✝

Construction of continuous linear maps between Schwartz spaces

def SchwartzMap.mkLM {𝕜 : Type u_2} {𝕜' : Type u_3} {D : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [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 : SchwartzMap 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_2} {𝕜' : Type u_3} {D : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [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 : SchwartzMap 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_2} {𝕜' : Type u_3} {D : Type u_4} {E : Type u_5} {G : Type u_7} [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_2) (E : Type u_5) {F : Type u_6} (G : Type u_7) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 G] [SMulCommClass ℝ 𝕜 G] (m : F) : SchwartzMap E (F →L[ℝ] G) →L[𝕜] SchwartzMap E G

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

@[simp]

theorem SchwartzMap.evalCLM_apply_apply {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} {G : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 G] [SMulCommClass ℝ 𝕜 G] (f : SchwartzMap E (F →L[ℝ] G)) (m : F) (x : E) : ((SchwartzMap.evalCLM 𝕜 E G m) f) x = (f x) m

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

@[simp]

theorem SchwartzMap.bilinLeftCLM_apply {𝕜 : Type u_2} {D : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {g : D → F} (hg : Function.HasTemperateGrowth g) (f : SchwartzMap D E) : ⇑((bilinLeftCLM B hg) f) = fun (x : D) => (B (f x)) (g x)

def SchwartzMap.smulLeftCLM {𝕜 : Type u_2} {E : Type u_5} (F : Type u_6) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] (g : E → 𝕜) : SchwartzMap E F →L[𝕜] SchwartzMap E F

The map f ↦ (x ↦ g x • f x) as a continuous 𝕜-linear map on Schwartz space, where g is a function of temperate growth.

theorem SchwartzMap.smulLeftCLM_apply {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] {g : E → 𝕜} (hg : Function.HasTemperateGrowth g) (f : SchwartzMap E F) : ⇑((smulLeftCLM F g) f) = fun (x : E) => g x • f x

@[simp]

theorem SchwartzMap.smulLeftCLM_apply_apply {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] {g : E → 𝕜} (hg : Function.HasTemperateGrowth g) (f : SchwartzMap E F) (x : E) : ((smulLeftCLM F g) f) x = g x • f x

@[simp]

theorem SchwartzMap.smulLeftCLM_const {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] (c : 𝕜) : (smulLeftCLM F fun (x : E) => c) = c • ContinuousLinearMap.id 𝕜 (SchwartzMap E F)

@[simp]

theorem SchwartzMap.smulLeftCLM_smulLeftCLM_apply {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] {g₁ g₂ : E → 𝕜} (hg₁ : Function.HasTemperateGrowth g₁) (hg₂ : Function.HasTemperateGrowth g₂) (f : SchwartzMap E F) : (smulLeftCLM F g₁) ((smulLeftCLM F g₂) f) = (smulLeftCLM F (g₁ * g₂)) f

theorem SchwartzMap.smulLeftCLM_compL_smulLeftCLM {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] {g₁ g₂ : E → 𝕜} (hg₁ : Function.HasTemperateGrowth g₁) (hg₂ : Function.HasTemperateGrowth g₂) : (smulLeftCLM F g₁).comp (smulLeftCLM F g₂) = smulLeftCLM F (g₁ * g₂)

theorem SchwartzMap.smulLeftCLM_smul {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] {g : E → 𝕜} (hg : Function.HasTemperateGrowth g) (c : 𝕜) : smulLeftCLM F (c • g) = c • smulLeftCLM F g

theorem SchwartzMap.smulLeftCLM_add {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] {g₁ g₂ : E → 𝕜} (hg₁ : Function.HasTemperateGrowth g₁) (hg₂ : Function.HasTemperateGrowth g₂) : smulLeftCLM F (g₁ + g₂) = smulLeftCLM F g₁ + smulLeftCLM F g₂

theorem SchwartzMap.smulLeftCLM_sub {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] {g₁ g₂ : E → 𝕜} (hg₁ : Function.HasTemperateGrowth g₁) (hg₂ : Function.HasTemperateGrowth g₂) : smulLeftCLM F (g₁ - g₂) = smulLeftCLM F g₁ - smulLeftCLM F g₂

theorem SchwartzMap.smulLeftCLM_neg {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] {g : E → 𝕜} (hg : Function.HasTemperateGrowth g) : smulLeftCLM F (-g) = -smulLeftCLM F g

theorem SchwartzMap.smulLeftCLM_fun_neg {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] {g : E → 𝕜} (hg : Function.HasTemperateGrowth g) : (smulLeftCLM F fun (x : E) => -g x) = -smulLeftCLM F g

theorem SchwartzMap.smulLeftCLM_sum {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] {g : ι → E → 𝕜} {s : Finset ι} (hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)) : (smulLeftCLM F fun (x : E) => ∑ i ∈ s, g i x) = ∑ i ∈ s, smulLeftCLM F (g i)

theorem SchwartzMap.smulLeftCLM_ofReal {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (𝕜' : Type u_10) [RCLike 𝕜'] [NormedSpace 𝕜' F] {g : E → ℝ} (hg : Function.HasTemperateGrowth g) (f : SchwartzMap E F) : (smulLeftCLM F fun (x : E) => ↑(g x)) f = (smulLeftCLM F g) f

theorem SchwartzMap.smulLeftCLM_real_smul {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {𝕜' : Type u_10} [RCLike 𝕜'] [NormedSpace 𝕜' F] {g : E → 𝕜'} (hg : Function.HasTemperateGrowth g) (c : ℝ) : smulLeftCLM F (c • g) = c • smulLeftCLM F g

theorem SchwartzMap.tsupport_smulLeftCLM_subset {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 F] (g : E → 𝕜) (f : SchwartzMap E F) : tsupport ⇑((smulLeftCLM F g) f) ⊆ tsupport ⇑f ∩ tsupport g

def SchwartzMap.pairing {𝕜 : Type u_2} {D : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) : SchwartzMap D E →ₗ[𝕜] SchwartzMap D F →L[𝕜] SchwartzMap D G

The bilinear pairing of Schwartz functions.

The continuity in the left argument is provided in SchwartzMap.pairing_continuous_left.

theorem SchwartzMap.pairing_apply {𝕜 : Type u_2} {D : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) (f : SchwartzMap D E) (g : SchwartzMap D F) : ⇑(((pairing B) f) g) = fun (x : D) => (B (f x)) (g x)

@[simp]

theorem SchwartzMap.pairing_apply_apply {𝕜 : Type u_2} {D : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) (f : SchwartzMap D E) (g : SchwartzMap D F) (x : D) : (((pairing B) f) g) x = (B (f x)) (g x)

theorem SchwartzMap.pairing_continuous_left {𝕜 : Type u_2} {D : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) (g : SchwartzMap D F) : Continuous fun (x : SchwartzMap D E) => ((pairing B) x) g

The pairing is continuous in the left argument.

Note that since 𝓢(E, F) is not a normed space, uncurried and curried continuity do not coincide.

def SchwartzMap.smulRightCLM (𝕜 : Type u_2) {E : Type u_5} (F : Type u_6) {G : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] (L : E →L[ℝ] G →L[ℝ] ℝ) : SchwartzMap E F →L[𝕜] SchwartzMap E (G →L[ℝ] F)

Scalar multiplication with a continuous linear map as a continuous linear map on Schwartz functions.

@[simp]

theorem SchwartzMap.smulRightCLM_apply_apply {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} {G : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 F] (L : E →L[ℝ] G →L[ℝ] ℝ) (f : SchwartzMap E F) (x : E) : ((smulRightCLM 𝕜 F L) f) x = (L x).smulRight (f x)

def SchwartzMap.compCLM (𝕜 : Type u_2) {D : Type u_4} {E : Type u_5} {F : Type u_6} [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_2) {D : Type u_4} {E : Type u_5} {F : Type u_6} [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_2) {D : Type u_4} {E : Type u_5} {F : Type u_6} [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_2) {D : Type u_4} {E : Type u_5} {F : Type u_6} [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_2) {D : Type u_4} {E : Type u_5} {F : Type u_6} [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_2) {D : Type u_4} {E : Type u_5} {F : Type u_6} [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

theorem SchwartzMap.smulLeftCLM_compCLMOfContinuousLinearEquiv (𝕜 : Type u_2) {𝕜' : Type u_3} {D : Type u_4} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [RCLike 𝕜] [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [NontriviallyNormedField 𝕜'] [NormedAlgebra ℝ 𝕜'] [NormedSpace 𝕜' F] {u : D → 𝕜'} (hu : Function.HasTemperateGrowth u) (g : D ≃L[ℝ] E) (f : SchwartzMap E F) : (smulLeftCLM F u) ((compCLMOfContinuousLinearEquiv 𝕜 g) f) = (compCLMOfContinuousLinearEquiv 𝕜 g) ((smulLeftCLM F (u ∘ ⇑g.symm)) f)

Integration

theorem SchwartzMap.integral_pow_mul_iteratedFDeriv_le (𝕜 : Type u_2) {D : Type u_4} {V : Type u_9} [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_4} {V : Type u_9} [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_4} {V : Type u_9} [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_4} {V : Type u_9} [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_2) {D : Type u_4} {V : Type u_9} [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_2) {D : Type u_4} {V : Type u_9} [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_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : BoundedContinuousMapClass (SchwartzMap E F) E F

def SchwartzMap.toBoundedContinuousFunction {E : Type u_5} {F : Type u_6} [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_5} {F : Type u_6} [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_5} {F : Type u_6} [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_2) (E : Type u_5) (F : Type u_6) [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_2) (E : Type u_5) (F : Type u_6) [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

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

def SchwartzMap.toZeroAtInfty {E : Type u_5} {F : Type u_6} [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_5} {F : Type u_6} [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_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [ProperSpace E] (f : SchwartzMap E F) : f.toZeroAtInfty.toBCF = f.toBoundedContinuousFunction

def SchwartzMap.toZeroAtInftyCLM (𝕜 : Type u_2) (E : Type u_5) (F : Type u_6) [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_2) (E : Type u_5) (F : Type u_6) [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_2) {E : Type u_5} (F : Type u_6) [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μ : μ.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_5} {F : Type u_6} [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μ : μ.HasTemperateGrowth] : MeasureTheory.eLpNorm (⇑f) p μ < ⊤

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

theorem SchwartzMap.memLp_top {E : Type u_5} {F : Type u_6} [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.

theorem SchwartzMap.memLp {E : Type u_5} {F : Type u_6} [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μ : μ.HasTemperateGrowth] : MeasureTheory.MemLp (⇑f) p μ

Schwartz functions are in L^p for any p.

def SchwartzMap.toLp {E : Type u_5} {F : Type u_6} [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μ : μ.HasTemperateGrowth] : ↥(MeasureTheory.Lp F p μ)

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

theorem SchwartzMap.coeFn_toLp {E : Type u_5} {F : Type u_6} [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μ : μ.HasTemperateGrowth] : ↑↑(f.toLp p μ) =ᵐ[μ] ⇑f

theorem SchwartzMap.norm_toLp {E : Type u_5} {F : Type u_6} [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_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F] (p : ENNReal) (μ : MeasureTheory.Measure E := by volume_tac) [hμ : μ.HasTemperateGrowth] [μ.IsOpenPosMeasure] : Function.Injective fun (f : SchwartzMap E F) => f.toLp p μ

theorem SchwartzMap.norm_toLp_le_seminorm (𝕜 : Type u_2) {E : Type u_5} (F : Type u_6) [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μ : μ.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_2) {E : Type u_5} (F : Type u_6) [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μ : μ.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_2} {E : Type u_5} {F : Type u_6} [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_5} {F : Type u_6} [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 μ

theorem SchwartzMap.denseRange_toLpCLM {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F] [FiniteDimensional ℝ E] [BorelSpace E] {p : ENNReal} (hp : p ≠ ⊤) [hp' : Fact (1 ≤ p)] {μ : MeasureTheory.Measure E} [hμ : μ.HasTemperateGrowth] [MeasureTheory.IsFiniteMeasureOnCompacts μ] : DenseRange ⇑(toLpCLM ℝ F p μ)

Schwartz functions are dense in Lp.

@[simp]

theorem SchwartzMap.inner_toL2_toL2_eq {H : Type u_8} {V : Type u_9} [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] [MeasurableSpace H] [BorelSpace H] [NormedAddCommGroup V] [InnerProductSpace ℂ V] (f g : SchwartzMap H V) (μ : MeasureTheory.Measure H := by volume_tac) [μ.HasTemperateGrowth] : inner ℂ (f.toLp 2 μ) (g.toLp 2 μ) = ∫ (x : H), inner ℂ (f x) (g x) ∂μ