Some Facts about Schwartz Functions

In this file, we prove some useful facts about Schwartz Functions. It is possible that some of them apply to cases more general than just ℝ-vector spaces, but we do not worry about that here.

Main Definitions

1. linearEquiv_of_linearEquiv_domain : Given a linear equivalence between finite-dimensional real vector spaces, composition with this equivalence gives a continuous linear equivalence between any two Schwartz spaces that have these equivalent spaces for a domain.
2. SchwartzMap_one_of_SchwartzMap_two : Given a Schwartz function in two variables, we can consider it as a Schwartz function in one variable by fixing a coordinate. The action of mapping the Schwartz function in two variables to the Schwartz function in one variable is continuous and linear.

noncomputable def SchwartzMap.linearEquiv_of_linearEquiv_domain {E : Type u_1} {F : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] (eq_l : E ≃ₗ[ℝ] H) : SchwartzMap H F ≃L[ℝ] SchwartzMap E F

Given a linear equivalence between finite-dimensional real vector spaces, composition on the left with this equivalence gives a continuous linear isomorphism between any two Schwartz spaces that have these equivalent spaces for a domain.

Equations

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

In this section, we explore Schwartzness in the different variables of a multivariable Schwartz function. The theory in this section would be necessary for an inductive proof of Poisson Summation Formula over the canonical lattice ℤ^n, which is used to prove the result for other lattices.

def SchwartzMap.coordinateEmbedding₁₂ (x : ℝ) : Euc(1) → Euc(2)

The family of embeddings of Euc(1) into Euc(2) by fixing a coordinate, indexed by elements of ℝ. The subscripts indicate it is an embedding of Euc(1) into Euc(2).

Equations

• SchwartzMap.coordinateEmbedding₁₂ x y = !₂[x, (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ) y]

theorem SchwartzMap.coordinateEmbedding₁₂_injective (x : ℝ) : Function.Injective (coordinateEmbedding₁₂ x)

coordinateEmbedding₁₂ is injective.

theorem SchwartzMap.coordinateEmbedding₁₂_smooth (x : ℝ) : ContDiff ℝ ⊤ (coordinateEmbedding₁₂ x)

coordinateEmbedding₁₂ is smooth.

def SchwartzMap.coordinateEmbedding₁₂_fderiv (x : ℝ) : Euc(1) →L[ℝ] Euc(2)

The Jacobian of coordinateEmbedding₁₂ x for all x : ℝ.

Equations

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

theorem SchwartzMap.coordinateEmbedding₁₂_hasDerivAt (x : ℝ) (p : Euc(1)) : HasFDerivAt (coordinateEmbedding₁₂ x) (coordinateEmbedding₁₂_fderiv x) p

The Jacobian of coordinateEmbedding₁₂ x is the constant !₂[0, 1].

theorem SchwartzMap.fderiv_coordinateEmbedding₁₂_hasTemperateGrowth (x : ℝ) : Function.HasTemperateGrowth (fderiv ℝ (coordinateEmbedding₁₂ x))

The Jacobian of coordinateEmbedding₁₂ has temperate growth.

theorem SchwartzMap.coordinateEmbedding₁₂_hasTemperateGrowth (x : ℝ) : Function.HasTemperateGrowth (coordinateEmbedding₁₂ x)

coordinateEmbedding₁₂ has temperate growth.

theorem SchwartzMap.coordinateEmbedding₁₂_antiLipschitzWith (x : ℝ) : AntilipschitzWith 1 (coordinateEmbedding₁₂ x)

coordinateEmbedding₁₂ is AntilipschitzWith 1.

def SchwartzMap.SchwartzMap_one_of_SchwartzMap_two (x : ℝ) : SchwartzMap Euc(2) ℂ →L[ℝ] SchwartzMap Euc(1) ℂ

A Schwartz function in multiple variables is Schwartz in each variable. (2 variable case)

Equations

• SchwartzMap.SchwartzMap_one_of_SchwartzMap_two x = SchwartzMap.compCLMOfAntilipschitz ℝ ⋯ ⋯