Tensor products of Schwartz functions

For a real Schwartz function ψ on D and a Schwartz function u on E, the function (t, x) ↦ ψ t • u x on D × E is again a Schwartz function, SchwartzMap.prodSMul ψ u. Its directional derivative in the direction (s, a) is the sum of the tensor products of the derivative of one factor with the other factor (SchwartzMap.lineDerivOp_prodSMul).

Such tensor products separate the variables of a product space. A typical use is to transfer an estimate from D × E to E by testing it against ψ ⊗ u with ψ a fixed profile.

Main declarations

• SchwartzMap.prodSMul: the Schwartz function (t, x) ↦ ψ t • u x.
• SchwartzMap.lineDerivOp_prodSMul: ∂_{(s, a)} (ψ ⊗ u) = (∂_s ψ) ⊗ u + ψ ⊗ ∂_a u.

def SchwartzMap.prodSMul {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ψ : SchwartzMap D ℝ) (u : SchwartzMap E F) : SchwartzMap (D × E) F

The tensor product (t, x) ↦ ψ t • u x of a real Schwartz function ψ on D and a Schwartz function u on E, a Schwartz function on D × E.

@[simp]

theorem SchwartzMap.prodSMul_apply {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ψ : SchwartzMap D ℝ) (u : SchwartzMap E F) (z : D × E) : (ψ.prodSMul u) z = ψ z.1 • u z.2

theorem SchwartzMap.coe_prodSMul {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ψ : SchwartzMap D ℝ) (u : SchwartzMap E F) : ⇑(ψ.prodSMul u) = fun (z : D × E) => ψ z.1 • u z.2

@[simp]

theorem SchwartzMap.zero_prodSMul {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (u : SchwartzMap E F) : prodSMul 0 u = 0

@[simp]

theorem SchwartzMap.prodSMul_zero {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ψ : SchwartzMap D ℝ) : ψ.prodSMul 0 = 0

@[simp]

theorem SchwartzMap.add_prodSMul {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ψ φ : SchwartzMap D ℝ) (u : SchwartzMap E F) : (ψ + φ).prodSMul u = ψ.prodSMul u + φ.prodSMul u

@[simp]

theorem SchwartzMap.prodSMul_add {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ψ : SchwartzMap D ℝ) (u v : SchwartzMap E F) : ψ.prodSMul (u + v) = ψ.prodSMul u + ψ.prodSMul v

@[simp]

theorem SchwartzMap.smul_prodSMul {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (ψ : SchwartzMap D ℝ) (u : SchwartzMap E F) : (c • ψ).prodSMul u = c • ψ.prodSMul u

@[simp]

theorem SchwartzMap.prodSMul_smul {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {𝕜 : Type u_4} [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (ψ : SchwartzMap D ℝ) (c : 𝕜) (u : SchwartzMap E F) : ψ.prodSMul (c • u) = c • ψ.prodSMul u

@[simp]

theorem SchwartzMap.lineDerivOp_prodSMul {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ψ : SchwartzMap D ℝ) (u : SchwartzMap E F) (s : D) (a : E) : LineDeriv.lineDerivOp (s, a) (ψ.prodSMul u) = (LineDeriv.lineDerivOp s ψ).prodSMul u + ψ.prodSMul (LineDeriv.lineDerivOp a u)

Derivatives of a tensor product. The directional derivative of ψ ⊗ u in the direction (s, a) is (∂_s ψ) ⊗ u + ψ ⊗ ∂_a u.