The tensor product of Schwartz functions

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #126(i), out of #122.

★★ SchwartzMap.tensorProd — (p, q) ↦ f p · g q is Schwartz on D₁ × D₂ when f and g are Schwartz on the factors. Mathlib has no such lemma, and #126 needs it: a composite integral kernel is built from a product of two kernels, one variable then integrated out.

The two ingredients

• the Leibniz bound norm_iteratedFDeriv_mul_le expands the derivatives of the product, and ★ norm_iteratedFDeriv_comp_clm_le drops each factor's derivative from the product to its own variable — a derivative along a continuous linear map of norm at most one is no bigger than the derivative of the function it is composed with, which is what the two projections are;
• the weight splits multiplicatively: ‖(p, q)‖ ≤ (1 + ‖p‖)·(1 + ‖q‖), because the product norm is a max. So one weight on the pair becomes one weight on each factor, and SchwartzMap.one_add_le_sup_seminorm_apply bounds each side by a Finset.sup of that factor's seminorms. The same bound then serves every term of the Leibniz sum, which is what keeps the constant short.

Honest scope

⚠️ Not bilinear-continuous. tensorProd is a function of two Schwartz functions, not a continuous bilinear map 𝓢(D₁, ℂ) →L 𝓢(D₂, ℂ) →L 𝓢(D₁ × D₂, ℂ). The estimate here is linear in one Finset.sup of each factor's seminorms, which is what continuity in each argument separately would need, so the stronger statement is a packaging exercise — but nothing needs it, and SchwartzMap.decay' asks only that a bound exist.

⚠️ Scalar-valued. Both factors are ℂ-valued and the product is multiplication. The version for a general bounded bilinear map is the same proof with norm_iteratedFDeriv_clm_apply_const_le in place of the Leibniz bound; it is not needed here.

References: SchwartzPartialIntegral.lean (#126(ii), which consumes this), WeylComposition.lean (#126(iii)(iv)); specs/BACKLOG.md #126, #122.

theorem norm_iteratedFDeriv_comp_clm_le {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Type u_4} {E : Type u_5} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (L : D →L[ℝ] E) (hL : ‖L‖ ≤ 1) {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (i : ℕ) (x : D) : ‖iteratedFDeriv ℝ i (fun (y : D) => f (L y)) x‖ ≤ ‖iteratedFDeriv ℝ i f (L x)‖

★ A derivative along a short linear map is no bigger than the derivative itself. The two projections of a product are short, which is how the Leibniz expansion below returns each factor's derivative to its own variable.

theorem norm_fst_clm_le_one {D₁ : Type u_1} [NormedAddCommGroup D₁] [NormedSpace ℝ D₁] {D₂ : Type u_2} [NormedAddCommGroup D₂] [NormedSpace ℝ D₂] : ‖ContinuousLinearMap.fst ℝ D₁ D₂‖ ≤ 1

Both projections of a product are short.

theorem norm_snd_clm_le_one {D₁ : Type u_1} [NormedAddCommGroup D₁] [NormedSpace ℝ D₁] {D₂ : Type u_2} [NormedAddCommGroup D₂] [NormedSpace ℝ D₂] : ‖ContinuousLinearMap.snd ℝ D₁ D₂‖ ≤ 1

theorem norm_le_one_add_mul_one_add {D₁ : Type u_1} [NormedAddCommGroup D₁] {D₂ : Type u_2} [NormedAddCommGroup D₂] (r : D₁ × D₂) : ‖r‖ ≤ (1 + ‖r.1‖) * (1 + ‖r.2‖)

The weight on a pair splits multiplicatively, because the product norm is a max.

noncomputable def SchwartzMap.tensorProd {D₁ : Type u_1} [NormedAddCommGroup D₁] [NormedSpace ℝ D₁] {D₂ : Type u_2} [NormedAddCommGroup D₂] [NormedSpace ℝ D₂] (f : SchwartzMap D₁ ℂ) (g : SchwartzMap D₂ ℂ) : SchwartzMap (D₁ × D₂) ℂ

★★ The tensor product of two Schwartz functions is Schwartz.

Equations

• f.tensorProd g = { toFun := fun (r : D₁ × D₂) => f r.1 * g r.2, smooth' := ⋯, decay' := ⋯ }

@[simp]

theorem SchwartzMap.tensorProd_apply {D₁ : Type u_1} [NormedAddCommGroup D₁] [NormedSpace ℝ D₁] {D₂ : Type u_2} [NormedAddCommGroup D₂] [NormedSpace ℝ D₂] (f : SchwartzMap D₁ ℂ) (g : SchwartzMap D₂ ℂ) (r : D₁ × D₂) : (f.tensorProd g) r = f r.1 * g r.2