rename HasShockDeriv to HasParamFDerivWithJumps

lecopivo · Jun 24, 2024 · d247282 · d247282
1 parent 43893fc
commit d247282
Show file tree

Hide file tree

Showing 4 changed files with 794 additions and 0 deletions.
diff --git a/SciLean/Core/FunctionTransformations/RevFDeriv.lean b/SciLean/Core/FunctionTransformations/RevFDeriv.lean
@@ -18,6 +18,11 @@ def revFDeriv
   (f : X → Y) (x : X) : Y×(Y→X) :=
   (f x, adjoint K (fun dx => fderiv K f x dx))
 
+noncomputable
+def fgradient
+  {K : Type _} [RCLike K]
+  {X : Type _} [NormedAddCommGroup X] [AdjointSpace K X] [CompleteSpace X]
+  (f : X → K) (x : X) : X := (revFDeriv K f x).2 1
 
 namespace revFDeriv