feat(Analysis/SchwartzMap): translation of arguments (#35781)

We only define the translation with subtraction, because this is more common in applications.

Co-authored-by: Michael Douglas <mdouglas@scgp.stonybrook.edu>

Author: mcdoll

Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean

@@ -913,7 +913,7 @@ section Comp
 variable (𝕜)
 variable [RCLike 𝕜]
 variable [NormedAddCommGroup D] [NormedSpace ℝ D]
-variable [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]
+variable [NormedSpace 𝕜 F]
 
 /-- 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. -/
@@ -1061,6 +1061,35 @@ theorem postcompCLM_postcompCLM (L₁ : F →L[𝕜] G) (L₂ : G →L[𝕜] H)
 
 end Postcomp
 
+section Translate
+
+variable [RCLike 𝕜] [NormedSpace 𝕜 F]
+
+variable (𝕜) in
+/-- Translating the argument as a continuous linear map on Schwartz space. -/
+def compSubConstCLM (a : E) : 𝓢(E, F) →L[𝕜] 𝓢(E, F) :=
+  compCLMOfAntilipschitz (g := fun x ↦ x - a) (K := 1) 𝕜 (by fun_prop)
+    (fun _ _ ↦ by simp [edist_dist, dist_eq_norm])
+
+@[simp]
+theorem compSubConstCLM_apply (f : 𝓢(E, F)) (a x : E) :
+    f.compSubConstCLM 𝕜 a x = f (x - a) := rfl
+
+@[simp]
+theorem compSubConstCLM_zero : compSubConstCLM 𝕜 (0 : E) (F := F) = ContinuousLinearMap.id _ _ := by
+  ext f x
+  simp
+
+@[simp]
+theorem compSubConstCLM_comp (f : 𝓢(E, F)) (a b : E) :
+    (f.compSubConstCLM 𝕜 a).compSubConstCLM 𝕜 b = f.compSubConstCLM 𝕜 (a + b) := by
+  ext x
+  simp only [compSubConstCLM_apply]
+  congr 1
+  exact (sub_add_eq_sub_sub_swap x a b).symm
+
+end Translate
+
 section Integration
 
 /-! ### Integration -/

Mathlib/Analysis/Distribution/SchwartzSpace/Deriv.lean

@@ -73,10 +73,12 @@ theorem derivCLM_apply (f : 𝓢(ℝ, F)) (x : ℝ) : derivCLM 𝕜 F f x = deri
 theorem hasDerivAt (f : 𝓢(ℝ, F)) (x : ℝ) : HasDerivAt f (deriv f x) x :=
   f.differentiableAt.hasDerivAt
 
-variable [SMulCommClass ℝ 𝕜 F]
-
 open LineDeriv
 
+section fderiv
+
+variable [SMulCommClass ℝ 𝕜 F]
+
 variable (E F) in
 /-- The Fréchet derivative on Schwartz space as a continuous `𝕜`-linear map. -/
 def fderivCLM : 𝓢(E, F) →L[𝕜] 𝓢(E, E →L[ℝ] F) :=
@@ -133,14 +135,6 @@ alias pderivCLM_apply := LineDeriv.lineDerivOpCLM_apply
 theorem lineDerivOp_apply (m : E) (f : 𝓢(E, F)) (x : E) : ∂_{m} f x = lineDeriv ℝ f x m :=
   f.differentiableAt.lineDeriv_eq_fderiv.symm
 
-variable [NormedAddCommGroup D] [NormedSpace ℝ D]
-
-theorem lineDerivOp_compCLMOfContinuousLinearEquiv (m : D) (g : D ≃L[ℝ] E) (f : 𝓢(E, F)) :
-    ∂_{m} (compCLMOfContinuousLinearEquiv 𝕜 g f) =
-    compCLMOfContinuousLinearEquiv 𝕜 g (∂_{g m} f) := by
-  ext x
-  simp [lineDerivOp_apply_eq_fderiv, ContinuousLinearEquiv.comp_right_fderiv]
-
 @[deprecated (since := "2025-11-25")]
 alias iteratedPDeriv := LineDeriv.iteratedLineDerivOpCLM
 
@@ -169,6 +163,16 @@ theorem iteratedLineDerivOp_eq_iteratedFDeriv {n : ℕ} {m : Fin n → E} {f : 
 @[deprecated (since := "2025-11-25")]
 alias iteratedPDeriv_eq_iteratedFDeriv := iteratedLineDerivOp_eq_iteratedFDeriv
 
+end fderiv
+
+variable [NormedAddCommGroup D] [NormedSpace ℝ D]
+
+theorem lineDerivOp_compCLMOfContinuousLinearEquiv (m : D) (g : D ≃L[ℝ] E) (f : 𝓢(E, F)) :
+    ∂_{m} (compCLMOfContinuousLinearEquiv 𝕜 g f) =
+    compCLMOfContinuousLinearEquiv 𝕜 g (∂_{g m} f) := by
+  ext x
+  simp [lineDerivOp_apply_eq_fderiv, ContinuousLinearEquiv.comp_right_fderiv]
+
 end Derivatives
 
 section support