# Schwartz space #

This file defines the Schwartz space. Usually, the Schwartz space is defined as the set of smooth functions $f : β^n β β$ such that there exists $C_{Ξ±Ξ²} > 0$ with $$|x^Ξ± β^Ξ² f(x)| < C_{Ξ±Ξ²}$$ for all $x β β^n$ and for all multiindices $Ξ±, Ξ²$. In mathlib, we use a slightly different approach and define the Schwartz space as all smooth functions f : E β F, where E and F are real normed vector spaces such that for all natural numbers k and n we have uniform bounds βxβ^k * βiteratedFDeriv β n f xβ < C. This approach completely avoids using partial derivatives as well as polynomials. We construct the topology on the Schwartz space by a family of seminorms, which are the best constants in the above estimates. The abstract theory of topological vector spaces developed in SeminormFamily.moduleFilterBasis and WithSeminorms.toLocallyConvexSpace turns the Schwartz space into a locally convex topological vector space.

## Main definitions #

• SchwartzMap: The Schwartz space is the space of smooth functions such that all derivatives decay faster than any power of βxβ.
• SchwartzMap.seminorm: The family of seminorms as described above
• SchwartzMap.fderivCLM: The differential as a continuous linear map π’(E, F) βL[π] π’(E, E βL[β] F)
• SchwartzMap.derivCLM: The one-dimensional derivative as a continuous linear map π’(β, F) βL[π] π’(β, F)
• SchwartzMap.integralCLM: Integration as a continuous linear map π’(β, F) βL[β] F

## Main statements #

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

## Implementation details #

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

## Notation #

• π’(E, F): The Schwartz space SchwartzMap E F localized in SchwartzSpace

## Tags #

Schwartz space, tempered distributions

structure SchwartzMap (E : Type u_4) (F : Type u_5) [] [] :
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β.

Instances For
theorem SchwartzMap.smooth' {E : Type u_4} {F : Type u_5} [] [] (self : ) :
theorem SchwartzMap.decay' {E : Type u_4} {F : Type u_5} [] [] (self : ) (k : β) (n : β) :
β (C : β), β (x : E), ^ k * βiteratedFDeriv β n self.toFun xβ β€ C

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance SchwartzMap.instFunLike {E : Type u_4} {F : Type u_5} [] [] :
FunLike () E F
Equations
• SchwartzMap.instFunLike = { coe := fun (f : ) => f.toFun, coe_injective' := β― }
instance SchwartzMap.instCoeFun {E : Type u_4} {F : Type u_5} [] [] :
CoeFun () fun (x : ) => E β F

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

Equations
• SchwartzMap.instCoeFun = DFunLike.hasCoeToFun
theorem SchwartzMap.decay {E : Type u_4} {F : Type u_5} [] [] (f : ) (k : β) (n : β) :
β (C : β), 0 < C β§ β (x : E), ^ 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} [] [] (f : ) (n : ββ) :
ContDiff β n βf

Every Schwartz function is smooth.

theorem SchwartzMap.continuous {E : Type u_4} {F : Type u_5} [] [] (f : ) :
Continuous βf

Every Schwartz function is continuous.

instance SchwartzMap.instContinuousMapClass {E : Type u_4} {F : Type u_5} [] [] :
Equations
• β― = β―
theorem SchwartzMap.differentiable {E : Type u_4} {F : Type u_5} [] [] (f : ) :

Every Schwartz function is differentiable.

theorem SchwartzMap.differentiableAt {E : Type u_4} {F : Type u_5} [] [] (f : ) {x : E} :

Every Schwartz function is differentiable at any point.

theorem SchwartzMap.ext {E : Type u_4} {F : Type u_5} [] [] {f : } {g : } (h : β (x : E), f x = g x) :
f = g
theorem SchwartzMap.isBigO_cocompact_zpow_neg_nat {E : Type u_4} {F : Type u_5} [] [] (f : ) (k : β) :
βf =O[] fun (x : E) => ^ (-β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} [] [] (f : ) [] (s : β) :
βf =O[] fun (x : E) => ^ s
theorem SchwartzMap.isBigO_cocompact_zpow {E : Type u_4} {F : Type u_5} [] [] (f : ) [] (k : β€) :
βf =O[] fun (x : E) => ^ k
theorem SchwartzMap.bounds_nonempty {E : Type u_4} {F : Type u_5} [] [] (k : β) (n : β) (f : ) :
β (c : β), c β {c : β | 0 β€ c β§ β (x : E), ^ k * βiteratedFDeriv β n (βf) xβ β€ c}
theorem SchwartzMap.bounds_bddBelow {E : Type u_4} {F : Type u_5} [] [] (k : β) (n : β) (f : ) :
BddBelow {c : β | 0 β€ c β§ β (x : E), ^ k * βiteratedFDeriv β n (βf) xβ β€ c}
theorem SchwartzMap.decay_add_le_aux {E : Type u_4} {F : Type u_5} [] [] (k : β) (n : β) (f : ) (g : ) (x : E) :
theorem SchwartzMap.decay_neg_aux {E : Type u_4} {F : Type u_5} [] [] (k : β) (n : β) (f : ) (x : E) :
theorem SchwartzMap.decay_smul_aux {π : Type u_1} {E : Type u_4} {F : Type u_5} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] (k : β) (n : β) (f : ) (c : π) (x : E) :
def SchwartzMap.seminormAux {E : Type u_4} {F : Type u_5} [] [] (k : β) (n : β) (f : ) :

Helper definition for the seminorms of the Schwartz space.

Equations
Instances For
theorem SchwartzMap.seminormAux_nonneg {E : Type u_4} {F : Type u_5} [] [] (k : β) (n : β) (f : ) :
theorem SchwartzMap.le_seminormAux {E : Type u_4} {F : Type u_5} [] [] (k : β) (n : β) (f : ) (x : E) :
theorem SchwartzMap.seminormAux_le_bound {E : Type u_4} {F : Type u_5} [] [] (k : β) (n : β) (f : ) {M : β} (hMp : 0 β€ M) (hM : β (x : E), ^ k * βiteratedFDeriv β n (βf) xβ β€ 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} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] :
SMul π ()
Equations
• SchwartzMap.instSMul = { smul := fun (c : π) (f : ) => { toFun := c β’ βf, smooth' := β―, decay' := β― } }
@[simp]
theorem SchwartzMap.smul_apply {π : Type u_1} {E : Type u_4} {F : Type u_5} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] {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} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] [NormedField π'] [NormedSpace π' F] [SMulCommClass β π' F] [SMul π π'] [IsScalarTower π π' F] :
IsScalarTower π π' ()
Equations
• β― = β―
instance SchwartzMap.instSMulCommClass {π : Type u_1} {π' : Type u_2} {E : Type u_4} {F : Type u_5} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] [NormedField π'] [NormedSpace π' F] [SMulCommClass β π' F] [SMulCommClass π π' F] :
SMulCommClass π π' ()
Equations
• β― = β―
theorem SchwartzMap.seminormAux_smul_le {π : Type u_1} {E : Type u_4} {F : Type u_5} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] (k : β) (n : β) (c : π) (f : ) :
instance SchwartzMap.instNSMul {E : Type u_4} {F : Type u_5} [] [] :
Equations
• SchwartzMap.instNSMul = { smul := fun (c : β) (f : ) => { toFun := c β’ βf, smooth' := β―, decay' := β― } }
instance SchwartzMap.instZSMul {E : Type u_4} {F : Type u_5} [] [] :
Equations
• SchwartzMap.instZSMul = { smul := fun (c : β€) (f : ) => { toFun := c β’ βf, smooth' := β―, decay' := β― } }
instance SchwartzMap.instZero {E : Type u_4} {F : Type u_5} [] [] :
Zero ()
Equations
• SchwartzMap.instZero = { zero := { toFun := fun (x : E) => 0, smooth' := β―, decay' := β― } }
instance SchwartzMap.instInhabited {E : Type u_4} {F : Type u_5} [] [] :
Equations
• SchwartzMap.instInhabited = { default := 0 }
theorem SchwartzMap.coe_zero {E : Type u_4} {F : Type u_5} [] [] :
β0 = 0
@[simp]
theorem SchwartzMap.coeFn_zero {E : Type u_4} {F : Type u_5} [] [] :
β0 = 0
@[simp]
theorem SchwartzMap.zero_apply {E : Type u_4} {F : Type u_5} [] [] {x : E} :
0 x = 0
theorem SchwartzMap.seminormAux_zero {E : Type u_4} {F : Type u_5} [] [] (k : β) (n : β) :
= 0
instance SchwartzMap.instNeg {E : Type u_4} {F : Type u_5} [] [] :
Neg ()
Equations
• SchwartzMap.instNeg = { neg := fun (f : ) => { toFun := -βf, smooth' := β―, decay' := β― } }
instance SchwartzMap.instAdd {E : Type u_4} {F : Type u_5} [] [] :
Equations
• SchwartzMap.instAdd = { add := fun (f g : ) => { toFun := βf + βg, smooth' := β―, decay' := β― } }
@[simp]
theorem SchwartzMap.add_apply {E : Type u_4} {F : Type u_5} [] [] {f : } {g : } {x : E} :
(f + g) x = f x + g x
theorem SchwartzMap.seminormAux_add_le {E : Type u_4} {F : Type u_5} [] [] (k : β) (n : β) (f : ) (g : ) :
instance SchwartzMap.instSub {E : Type u_4} {F : Type u_5} [] [] :
Sub ()
Equations
• SchwartzMap.instSub = { sub := fun (f g : ) => { toFun := βf - βg, smooth' := β―, decay' := β― } }
@[simp]
theorem SchwartzMap.sub_apply {E : Type u_4} {F : Type u_5} [] [] {f : } {g : } {x : E} :
(f - g) x = f x - g x
instance SchwartzMap.instAddCommGroup {E : Type u_4} {F : Type u_5} [] [] :
Equations
def SchwartzMap.coeHom (E : Type u_4) (F : Type u_5) [] [] :
β+ E β F

Equations
• = { toFun := fun (f : ) => βf, map_zero' := β―, map_add' := β― }
Instances For
theorem SchwartzMap.coe_coeHom {E : Type u_4} {F : Type u_5} [] [] :
β() = DFunLike.coe
theorem SchwartzMap.coeHom_injective {E : Type u_4} {F : Type u_5} [] [] :
instance SchwartzMap.instModule {π : Type u_1} {E : Type u_4} {F : Type u_5} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] :
Module π ()
Equations

### Seminorms on Schwartz space #

def SchwartzMap.seminorm (π : Type u_1) {E : Type u_4} {F : Type u_5} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] (k : β) (n : β) :
Seminorm π ()

The seminorms of the Schwartz space given by the best constants in the definition of π’(E, F).

Equations
Instances For
theorem SchwartzMap.seminorm_le_bound (π : Type u_1) {E : Type u_4} {F : Type u_5} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] (k : β) (n : β) (f : ) {M : β} (hMp : 0 β€ M) (hM : β (x : E), ^ 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} [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] (k : β) (n : β) (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} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] (k : β) (n : β) (f : ) (x : E) :

The seminorm controls the Schwartz estimate for any fixed x.

theorem SchwartzMap.le_seminorm' (π : Type u_1) {F : Type u_5} [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] (k : β) (n : β) (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} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] (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} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] (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} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] (f : ) (xβ : E) :
βf xββ β€ (SchwartzMap.seminorm π 0 0) f
def schwartzSeminormFamily (π : Type u_1) (E : Type u_4) (F : Type u_5) [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] :
SeminormFamily π () ()

The family of Schwartz seminorms.

Equations
Instances For
@[simp]
theorem SchwartzMap.schwartzSeminormFamily_apply (π : Type u_1) (E : Type u_4) (F : Type u_5) [] [] [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) [] [] [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} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] {m : } {k : β} {n : β} (hk : k β€ m.1) (hn : n β€ m.2) (f : ) (x : E) :
(1 + ) ^ k * βiteratedFDeriv β n (βf) xβ β€ 2 ^ m.1 * (().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) [] [] :
Equations
• = ().moduleFilterBasis.topology'
theorem schwartz_withSeminorms (π : Type u_1) (E : Type u_4) (F : Type u_5) [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] :
instance SchwartzMap.instContinuousSMul {π : Type u_1} {E : Type u_4} {F : Type u_5} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] :
ContinuousSMul π ()
Equations
• β― = β―
instance SchwartzMap.instTopologicalAddGroup {E : Type u_4} {F : Type u_5} [] [] :
Equations
• β― = β―
instance SchwartzMap.instUniformSpace {E : Type u_4} {F : Type u_5} [] [] :
Equations
instance SchwartzMap.instUniformAddGroup {E : Type u_4} {F : Type u_5} [] [] :
Equations
• β― = β―
instance SchwartzMap.instLocallyConvexSpace {E : Type u_4} {F : Type u_5} [] [] :
Equations
• β― = β―
instance SchwartzMap.instFirstCountableTopology {E : Type u_4} {F : Type u_5} [] [] :
Equations
• β― = β―

### Functions of temperate growth #

def Function.HasTemperateGrowth {E : Type u_4} {F : Type u_5} [] [] (f : E β F) :

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

Equations
Instances For
theorem Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux {E : Type u_4} {F : Type u_5} [] [] {f : E β F} (hf_temperate : ) (n : β) :
β (k : β) (C : β), 0 β€ C β§ β N β€ n, β (x : E), ββ β€ C * (1 + ) ^ k
theorem Function.HasTemperateGrowth.of_fderiv {E : Type u_4} {F : Type u_5} [] [] {f : E β F} (h'f : ) (hf : ) {k : β} {C : β} (h : β (x : E), βf xβ β€ C * (1 + ) ^ k) :
theorem Function.HasTemperateGrowth.zero {E : Type u_4} {F : Type u_5} [] [] :
theorem Function.HasTemperateGrowth.const {E : Type u_4} {F : Type u_5} [] [] (c : F) :
theorem ContinuousLinearMap.hasTemperateGrowth {E : Type u_4} {F : Type u_5} [] [] (f : ) :
class MeasureTheory.Measure.HasTemperateGrowth {D : Type u_3} [] (ΞΌ : ) :

A measure ΞΌ has temperate growth if there is an n : β such that (1 + βxβ) ^ (- n) is ΞΌ-integrable.

Instances
theorem MeasureTheory.Measure.HasTemperateGrowth.exists_integrable {D : Type u_3} [] {ΞΌ : } [self : ΞΌ.HasTemperateGrowth] :
β (n : β), MeasureTheory.Integrable (fun (x : D) => (1 + ) ^ (-βn)) ΞΌ

An integer exponent l such that (1 + βxβ) ^ (-l) is integrable if ΞΌ has temperate growth.

Equations
• ΞΌ.integrablePower = if h : ΞΌ.HasTemperateGrowth then β―.choose else 0
Instances For
theorem SchwartzMap.integrable_pow_neg_integrablePower {D : Type u_3} [] (ΞΌ : ) [h : ΞΌ.HasTemperateGrowth] :
MeasureTheory.Integrable (fun (x : D) => (1 + ) ^ (-βΞΌ.integrablePower)) ΞΌ
instance MeasureTheory.Measure.IsFiniteMeasure.instHasTemperateGrowth {D : Type u_3} [] {ΞΌ : } [h : ] :
ΞΌ.HasTemperateGrowth
Equations
• β― = β―
instance MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth {D : Type u_3} [] [] [] [] {ΞΌ : } [h : ΞΌ.IsAddHaarMeasure] :
ΞΌ.HasTemperateGrowth
Equations
• β― = β―
theorem SchwartzMap.pow_mul_le_of_le_of_pow_mul_le {Cβ : β} {Cβ : β} {k : β} {l : β} {x : β} {f : β} (hx : 0 β€ x) (hf : 0 β€ f) (hβ : f β€ Cβ) (hβ : x ^ (k + l) * f β€ Cβ) :
x ^ k * f β€ 2 ^ l * (Cβ + Cβ) * (1 + x) ^ (-βl)

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

theorem SchwartzMap.integrable_of_le_of_pow_mul_le {D : Type u_3} {E : Type u_4} [] [] {ΞΌ : } [ΞΌ.HasTemperateGrowth] {f : D β E} {Cβ : β} {Cβ : β} {k : β} (hf : β (x : D), βf xβ β€ Cβ) (h'f : β (x : D), ^ (k + ΞΌ.integrablePower) * βf xβ β€ Cβ) (h''f : ) :
MeasureTheory.Integrable (fun (x : D) => ^ 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} {E : Type u_4} [] {ΞΌ : } [ΞΌ.HasTemperateGrowth] {f : D β E} {Cβ : β} {Cβ : β} {k : β} (hf : β (x : D), βf xβ β€ Cβ) (h'f : β (x : D), ^ (k + ΞΌ.integrablePower) * βf xβ β€ Cβ) :
β« (x : D), ^ k * βf xβ βΞΌ β€ (2 ^ ΞΌ.integrablePower * β« (x : D), (1 + ) ^ (-βΞΌ.integrablePower) βΞΌ) * (Cβ + Cβ)

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

### Construction of continuous linear maps between Schwartz spaces #

def SchwartzMap.mkLM {π : Type u_1} {π' : Type u_2} {D : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [] [] [NormedField π] [NormedField π'] [] [NormedSpace π E] [SMulCommClass β π E] [] [NormedSpace π' G] [SMulCommClass β π' G] {Ο : π β+* π'} (A : (D β E) β F β G) (hadd : β (f g : ) (x : F), A (βf + βg) x = A (βf) x + A (βg) x) (hsmul : β (a : π) (f : ) (x : F), A (a β’ βf) x = Ο a β’ A (βf) x) (hsmooth : β (f : ), ContDiff β β€ (A βf)) (hbound : β (n : ), β (s : Finset ()) (C : β), 0 β€ C β§ β (f : ) (x : F), ^ n.1 * βiteratedFDeriv β n.2 (A βf) xβ β€ C * (s.sup (schwartzSeminormFamily π D E)) f) :

Create a semilinear map between Schwartz spaces.

Note: This is a helper definition for mkCLM.

Equations
• SchwartzMap.mkLM A hadd hsmul hsmooth hbound = { toFun := fun (f : ) => { toFun := A βf, smooth' := β―, decay' := β― }, map_add' := β―, map_smul' := β― }
Instances For
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} [] [] [NormedField π] [NormedField π'] [] [NormedSpace π E] [SMulCommClass β π E] [] [NormedSpace π' G] [SMulCommClass β π' G] {Ο : π β+* π'} [] (A : (D β E) β F β G) (hadd : β (f g : ) (x : F), A (βf + βg) x = A (βf) x + A (βg) x) (hsmul : β (a : π) (f : ) (x : F), A (a β’ βf) x = Ο a β’ A (βf) x) (hsmooth : β (f : ), ContDiff β β€ (A βf)) (hbound : β (n : ), β (s : Finset ()) (C : β), 0 β€ C β§ β (f : ) (x : F), ^ n.1 * βiteratedFDeriv β n.2 (A βf) xβ β€ C * (s.sup (schwartzSeminormFamily π D E)) f) :

Create a continuous semilinear map between Schwartz spaces.

For an example of using this definition, see fderivCLM.

Equations
Instances For
def SchwartzMap.mkCLMtoNormedSpace {π : Type u_1} {π' : Type u_2} {D : Type u_3} {E : Type u_4} {G : Type u_6} [] [NormedField π] [NormedField π'] [] [NormedSpace π E] [SMulCommClass β π E] [NormedSpace π' G] {Ο : π β+* π'} [] (A : β G) (hadd : β (f g : ), A (f + g) = A f + A g) (hsmul : β (a : π) (f : ), A (a β’ f) = Ο a β’ A f) (hbound : β (s : Finset ()) (C : β), 0 β€ C β§ β (f : ), βA fβ β€ C * (s.sup (schwartzSeminormFamily π D E)) f) :
βSL[Ο] G

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

Equations
Instances For
def SchwartzMap.evalCLM {π : Type u_1} {E : Type u_4} {F : Type u_5} [] [] [NormedField π] [NormedSpace π F] [SMulCommClass β π F] (m : E) :
SchwartzMap E () βL[π]

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

Equations
• = SchwartzMap.mkCLM (fun (f : E β ) (x : E) => (f x) m) β― β― β― β―
Instances For
def SchwartzMap.bilinLeftCLM {D : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [] [] [] [] (B : E βL[β] ) {g : D β F} (hg : ) :

The map f β¦ (x β¦ B (f x) (g x)) as a continuous π-linear map on Schwartz space, where B is a continuous π-linear map and g is a function of temperate growth.

Equations
• = SchwartzMap.mkCLM (fun (f : D β E) (x : D) => (B (f x)) (g x)) β― β― β― β―
Instances For
def SchwartzMap.compCLM (π : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [] [NormedSpace π F] [SMulCommClass β π F] {g : D β E} (hg : ) (hg_upper : β (k : β) (C : β), β (x : D), β€ C * (1 + βg xβ) ^ k) :
βL[π]

Composition with a function on the right is a continuous linear map on Schwartz space provided that the function is temperate and growths polynomially near infinity.

Equations
Instances For
@[simp]
theorem SchwartzMap.compCLM_apply (π : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [] [NormedSpace π F] [SMulCommClass β π F] {g : D β E} (hg : ) (hg_upper : β (k : β) (C : β), β (x : D), β€ C * (1 + βg xβ) ^ k) (f : ) :
β((SchwartzMap.compCLM π hg hg_upper) f) = βf β g
def SchwartzMap.compCLMOfAntilipschitz (π : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [] [NormedSpace π F] [SMulCommClass β π F] {K : NNReal} {g : D β E} (hg : ) (h'g : ) :
βL[π]

Composition with a function on the right is a continuous linear map on Schwartz space provided that the function is temperate and antilipschitz.

Equations
Instances For
@[simp]
theorem SchwartzMap.compCLMOfAntilipschitz_apply (π : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [] [NormedSpace π F] [SMulCommClass β π F] {K : NNReal} {g : D β E} (hg : ) (h'g : ) (f : ) :
β((SchwartzMap.compCLMOfAntilipschitz π hg h'g) f) = βf β g
def SchwartzMap.compCLMOfContinuousLinearEquiv (π : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [] [NormedSpace π F] [SMulCommClass β π F] (g : ) :
βL[π]

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

Equations
Instances For
@[simp]
theorem SchwartzMap.compCLMOfContinuousLinearEquiv_apply (π : Type u_1) {D : Type u_3} {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [] [NormedSpace π F] [SMulCommClass β π F] (g : ) (f : ) :
β() = βf β βg

### Derivatives of Schwartz functions #

def SchwartzMap.fderivCLM (π : Type u_1) {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] :
βL[π] SchwartzMap E ()

The FrΓ©chet derivative on Schwartz space as a continuous π-linear map.

Equations
Instances For
@[simp]
theorem SchwartzMap.fderivCLM_apply (π : Type u_1) {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] (f : ) (x : E) :
(() f) x = fderiv β (βf) x
def SchwartzMap.derivCLM (π : Type u_1) {F : Type u_5} [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] :
βL[π]

The 1-dimensional derivative on Schwartz space as a continuous π-linear map.

Equations
Instances For
@[simp]
theorem SchwartzMap.derivCLM_apply (π : Type u_1) {F : Type u_5} [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] (f : ) (x : β) :
(() f) x = deriv (βf) x
def SchwartzMap.pderivCLM (π : Type u_1) {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] (m : E) :
βL[π]

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

Equations
• = .comp ()
Instances For
@[simp]
theorem SchwartzMap.pderivCLM_apply (π : Type u_1) {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] (m : E) (f : ) (x : E) :
(() f) x = (fderiv β (βf) x) m
theorem SchwartzMap.pderivCLM_eq_lineDeriv (π : Type u_1) {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] (m : E) (f : ) (x : E) :
(() f) x = lineDeriv β (βf) x m
def SchwartzMap.iteratedPDeriv (π : Type u_1) {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] {n : β} :
(Fin n β E) β βL[π]

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem SchwartzMap.iteratedPDeriv_zero (π : Type u_1) {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] (m : Fin 0 β E) (f : ) :
() f = f
@[simp]
theorem SchwartzMap.iteratedPDeriv_one (π : Type u_1) {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] (m : Fin 1 β E) (f : ) :
() f = (SchwartzMap.pderivCLM π (m 0)) f
theorem SchwartzMap.iteratedPDeriv_succ_left (π : Type u_1) {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] {n : β} (m : Fin (n + 1) β E) (f : ) :
() f = (SchwartzMap.pderivCLM π (m 0)) (() f)
theorem SchwartzMap.iteratedPDeriv_succ_right (π : Type u_1) {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] {n : β} (m : Fin (n + 1) β E) (f : ) :
() f = () ((SchwartzMap.pderivCLM π (m ())) f)
theorem SchwartzMap.iteratedPDeriv_eq_iteratedFDeriv (π : Type u_1) {E : Type u_4} {F : Type u_5} [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] {n : β} {m : Fin n β E} {f : } {x : E} :
(() f) x = (iteratedFDeriv β n (βf) x) m

### Integration #

theorem SchwartzMap.integrable_pow_mul_iteratedFDeriv {D : Type u_3} {V : Type u_7} [] [] [] [] (ΞΌ : ) [hΞΌ : ΞΌ.HasTemperateGrowth] (f : ) (k : β) (n : β) :
MeasureTheory.Integrable (fun (x : D) => ^ k * βiteratedFDeriv β n (βf) xβ) ΞΌ
theorem SchwartzMap.integrable_pow_mul {D : Type u_3} {V : Type u_7} [] [] [] [] (ΞΌ : ) [hΞΌ : ΞΌ.HasTemperateGrowth] (f : ) (k : β) :
MeasureTheory.Integrable (fun (x : D) => ^ k * βf xβ) ΞΌ
theorem SchwartzMap.integral_pow_mul_iteratedFDeriv_le (π : Type u_1) {D : Type u_3} {V : Type u_7} [RCLike π] [] [] [NormedSpace π V] [] (ΞΌ : ) [hΞΌ : ΞΌ.HasTemperateGrowth] (f : ) (k : β) (n : β) :
β« (x : D), ^ k * βiteratedFDeriv β n (βf) xβ βΞΌ β€ (2 ^ ΞΌ.integrablePower * β« (x : D), (1 + ) ^ (-βΞΌ.integrablePower) βΞΌ) * ((SchwartzMap.seminorm π 0 n) f + (SchwartzMap.seminorm π (k + ΞΌ.integrablePower) n) f)
theorem SchwartzMap.integrable {D : Type u_3} {V : Type u_7} [] [] [] [] {ΞΌ : } [hΞΌ : ΞΌ.HasTemperateGrowth] (f : ) :
def SchwartzMap.integralCLM (π : Type u_1) {D : Type u_3} {V : Type u_7} [RCLike π] [] [] [NormedSpace π V] [] [] (ΞΌ : ) [hΞΌ : ΞΌ.HasTemperateGrowth] :
βL[π] V

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

Equations
Instances For
@[simp]
theorem SchwartzMap.integralCLM_apply (π : Type u_1) {D : Type u_3} {V : Type u_7} [RCLike π] [] [] [NormedSpace π V] [] [] {ΞΌ : } [hΞΌ : ΞΌ.HasTemperateGrowth] (f : ) :
(SchwartzMap.integralCLM π ΞΌ) f = β« (x : D), f x βΞΌ

### Inclusion into the space of bounded continuous functions #

instance SchwartzMap.instBoundedContinuousMapClass {E : Type u_4} {F : Type u_5} [] [] :
Equations
• β― = β―
def SchwartzMap.toBoundedContinuousFunction {E : Type u_4} {F : Type u_5} [] [] (f : ) :

Schwartz functions as bounded continuous functions

Equations
Instances For
@[simp]
theorem SchwartzMap.toBoundedContinuousFunction_apply {E : Type u_4} {F : Type u_5} [] [] (f : ) (x : E) :
f.toBoundedContinuousFunction x = f x
def SchwartzMap.toContinuousMap {E : Type u_4} {F : Type u_5} [] [] (f : ) :
C(E, F)

Schwartz functions as continuous functions

Equations
• f.toContinuousMap = f.toBoundedContinuousFunction.toContinuousMap
Instances For
def SchwartzMap.toBoundedContinuousFunctionCLM (π : Type u_1) (E : Type u_4) (F : Type u_5) [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] :
βL[π]

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

Equations
Instances For
@[simp]
theorem SchwartzMap.toBoundedContinuousFunctionCLM_apply (π : Type u_1) (E : Type u_4) (F : Type u_5) [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] (f : ) (x : E) :
(() f) x = f x
def SchwartzMap.delta (π : Type u_1) {E : Type u_4} (F : Type u_5) [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] (x : E) :
βL[π] F

The Dirac delta distribution

Equations
Instances For
@[simp]
theorem SchwartzMap.delta_apply (π : Type u_1) {E : Type u_4} (F : Type u_5) [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] (xβ : E) (f : ) :
(SchwartzMap.delta π F xβ) f = f xβ
@[simp]
theorem SchwartzMap.integralCLM_dirac_eq_delta (π : Type u_1) {E : Type u_4} (F : Type u_5) [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] [] [] [] (x : E) :
= SchwartzMap.delta π F x

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

instance SchwartzMap.instZeroAtInftyContinuousMapClass {E : Type u_4} {F : Type u_5} [] [] [] :
Equations
• β― = β―
def SchwartzMap.toZeroAtInfty {E : Type u_4} {F : Type u_5} [] [] [] (f : ) :

Schwartz functions as continuous functions vanishing at infinity.

Equations
• f.toZeroAtInfty = { toFun := βf, continuous_toFun := β―, zero_at_infty' := β― }
Instances For
@[simp]
theorem SchwartzMap.toZeroAtInfty_apply {E : Type u_4} {F : Type u_5} [] [] [] (f : ) (x : E) :
f.toZeroAtInfty x = f x
@[simp]
theorem SchwartzMap.toZeroAtInfty_toBCF {E : Type u_4} {F : Type u_5} [] [] [] (f : ) :
f.toZeroAtInfty.toBCF = f.toBoundedContinuousFunction
def SchwartzMap.toZeroAtInftyCLM (π : Type u_1) (E : Type u_4) (F : Type u_5) [] [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] :
βL[π]

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

Equations
Instances For
@[simp]
theorem SchwartzMap.toZeroAtInftyCLM_apply (π : Type u_1) (E : Type u_4) (F : Type u_5) [] [] [] [RCLike π] [NormedSpace π F] [SMulCommClass β π F] (f : ) (x : E) :
(() f) x = f x