Spaces \(\mathcal{S}(\R^d)\)

DefinitionStability by derivation#

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

SchwartzMap.fderivCLM.{u_2, u_4, u_7} (𝕜 : Type u_2) (E : Type u_4) (F : Type u_7)
  [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℝ E] [RCLike 𝕜]
  [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] : SchwartzMap E F →L[𝕜] SchwartzMap E (E →L[ℝ] F)
Sources
MathlibSchwartzMap.fderivCLM
Uses 3
Statement usesAssociative algebra over a commutative ring · Completeness · Schwartz space

DefinitionStability by multiplication by a slowly growing smooth function#

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.

SchwartzMap.bilinLeftCLM.{u_2, u_4, u_5, u_6, u_7} {𝕜 : 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
Sources
MathlibSchwartzMap.bilinLeftCLM
Uses 4 · Used by 2
Statement usesAssociative algebra over a commutative ring · Hausdorff space · Schwartz space · Topological module
Used byConvolution of two functions of \(\mathcal{S}(\R^d)\) · Multiplication by a function \(C^\infty\) of slow growth

DefinitionFourier transforms on \(\mathcal{S}(\R^d)\)#

The Fourier transform on a real inner product space, as a continuous linear map on the Schwartz space.

This definition is only to define the Fourier transform, use FourierTransform.fourierCLM instead.

SchwartzMap.fourierTransformCLM.{u_1, u_2, u_3} (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_3}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V]
  [BorelSpace V] : SchwartzMap V E →L[𝕜] SchwartzMap V E
Sources
MathlibSchwartzMap.fourierTransformCLM
Uses 7
Statement usesBochner integral · Borel sigma-algebra · Cos (extension of trigonometric functions to the complex plane) · Finite-dimensionality · Inner product space, over \(R\) or \(C\) · Lebesgue measure (Measure theory) · Schwartz space

DefinitionConvolution of two functions of \(\mathcal{S}(\R^d)\)#

The bilinear convolution of Schwartz functions.

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

SchwartzMap.convolution.{u_1, u_3, u_5, u_6, u_7} {𝕜 : Type u_1} {E : Type u_3} {F₁ : Type u_5}
  {F₂ : Type u_6} {F₃ : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F₁]
  [NormedSpace ℂ F₁] [NormedSpace 𝕜 F₁] [SMulCommClass ℂ 𝕜 F₁] [NormedAddCommGroup F₂]
  [NormedSpace ℂ F₂] [NormedSpace 𝕜 F₂] [SMulCommClass ℂ 𝕜 F₂] [NormedAddCommGroup F₃]
  [NormedSpace ℂ F₃] [NormedSpace 𝕜 F₃] [SMulCommClass ℂ 𝕜 F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) :
  SchwartzMap E F₁ →ₗ[𝕜] SchwartzMap E F₂ →L[𝕜] SchwartzMap E F₃
Sources
MathlibSchwartzMap.convolution
Uses 7
Statement usesBorel sigma-algebra · Complex number · Finite-dimensionality · Fourier transforms · Inner product space, over \(R\) or \(C\) · Inverse Fourier transform · Stability by multiplication by a slowly growing smooth function

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.