From c8f905a5b4111c9462e2e9e3fff2672f35a631d9 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 16 Mar 2026 06:32:01 +0000
Subject: [PATCH 1/2] feat: Add `gradSchwartz`

---
 .../SpaceAndTime/Space/Derivatives/Grad.lean  | 35 +++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/PhysLean/SpaceAndTime/Space/Derivatives/Grad.lean b/PhysLean/SpaceAndTime/Space/Derivatives/Grad.lean
index db4bfaaf6..bfd93fe09 100644
--- a/PhysLean/SpaceAndTime/Space/Derivatives/Grad.lean
+++ b/PhysLean/SpaceAndTime/Space/Derivatives/Grad.lean
@@ -45,6 +45,7 @@ of the input function with respect to each spatial coordinate.
   - B.3. The gradient as a sum over basis vectors
   - B.4. The underlying function of the gradient distribution
   - B.5. The gradient applied to a Schwartz function
+  - B.6. The gradident of a Schwartz map
 
 ## iv. References
 
@@ -502,4 +503,38 @@ lemma distGrad_apply {d} (f : (Space d) →d[ℝ] ℝ) (ε : 𝓢(Space d, ℝ))
   change (distGrad f).toFun ε = fun i => distDeriv i f ε
   rw [distGrad_toFun_eq_distDeriv]
 
+/-!
+
+### B.6. The gradident of a Schwartz map
+
+-/
+
+/-- The gradient on Scwhwartz maps. -/
+noncomputable def gradSchwartz {d} : 𝓢(Space d, ℝ) →ₗ[ℝ] 𝓢(Space d, EuclideanSpace ℝ (Fin d)) where
+  toFun η :=
+    let smulCLM : ℝ →L[ℝ] EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d) := {
+      toFun a := {
+        toFun v := a • v
+        map_add' v1 v2 := by simp
+        map_smul' a v := by rw [smul_comm]; simp
+        cont := by fun_prop}
+      map_add' v1 v2 := by ext1 v; simp [add_smul]
+      map_smul' a v := by ext1 v; simp [smul_smul]
+      cont := continuous_clm_apply.mpr <| fun y => by
+        simp only [ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk]
+        fun_prop }
+    ∑ i, SchwartzMap.bilinLeftCLM smulCLM (.const (EuclideanSpace.single i 1))
+      (.evalCLM ℝ (Space d) ℝ (basis i) (.fderivCLM ℝ (E := _) (F := ℝ) η))
+  map_add' η1 η2 := by
+    ext x i
+    simp [Finset.sum_add_distrib]
+  map_smul' a η := by
+    ext x i
+    simp [Finset.smul_sum, smul_smul]
+
+lemma gradSchwartz_apply_eq_grad {d} (η : 𝓢(Space d, ℝ)) (x : Space d):
+    gradSchwartz η x = grad η x := by
+  simp [gradSchwartz, grad_eq_sum]
+  rfl
+
 end Space

From b7e5f9f8ecff8b52ddb17cf87b202602b010e17e Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 18 Mar 2026 08:35:01 +0000
Subject: [PATCH 2/2] refactor: Golf

---
 .../SpaceAndTime/Space/Derivatives/Grad.lean  | 26 ++++---------------
 1 file changed, 5 insertions(+), 21 deletions(-)

diff --git a/PhysLean/SpaceAndTime/Space/Derivatives/Grad.lean b/PhysLean/SpaceAndTime/Space/Derivatives/Grad.lean
index bfd93fe09..8f5f423bd 100644
--- a/PhysLean/SpaceAndTime/Space/Derivatives/Grad.lean
+++ b/PhysLean/SpaceAndTime/Space/Derivatives/Grad.lean
@@ -510,27 +510,11 @@ lemma distGrad_apply {d} (f : (Space d) →d[ℝ] ℝ) (ε : 𝓢(Space d, ℝ))
 -/
 
 /-- The gradient on Scwhwartz maps. -/
-noncomputable def gradSchwartz {d} : 𝓢(Space d, ℝ) →ₗ[ℝ] 𝓢(Space d, EuclideanSpace ℝ (Fin d)) where
-  toFun η :=
-    let smulCLM : ℝ →L[ℝ] EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d) := {
-      toFun a := {
-        toFun v := a • v
-        map_add' v1 v2 := by simp
-        map_smul' a v := by rw [smul_comm]; simp
-        cont := by fun_prop}
-      map_add' v1 v2 := by ext1 v; simp [add_smul]
-      map_smul' a v := by ext1 v; simp [smul_smul]
-      cont := continuous_clm_apply.mpr <| fun y => by
-        simp only [ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk]
-        fun_prop }
-    ∑ i, SchwartzMap.bilinLeftCLM smulCLM (.const (EuclideanSpace.single i 1))
-      (.evalCLM ℝ (Space d) ℝ (basis i) (.fderivCLM ℝ (E := _) (F := ℝ) η))
-  map_add' η1 η2 := by
-    ext x i
-    simp [Finset.sum_add_distrib]
-  map_smul' a η := by
-    ext x i
-    simp [Finset.smul_sum, smul_smul]
+noncomputable def gradSchwartz {d} : 𝓢(Space d, ℝ) →L[ℝ] 𝓢(Space d, EuclideanSpace ℝ (Fin d)) :=
+    ∑ i, SchwartzMap.bilinLeftCLM (ContinuousLinearMap.lsmul ℝ ℝ)
+          (.const (EuclideanSpace.single i (1 : ℝ)))
+      ∘L SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)
+      ∘L SchwartzMap.fderivCLM ℝ (Space d) ℝ
 
 lemma gradSchwartz_apply_eq_grad {d} (η : 𝓢(Space d, ℝ)) (x : Space d):
     gradSchwartz η x = grad η x := by