From 857a7cd85c2a9b5a225a09b574479e7d5704473a Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Fri, 23 Aug 2024 15:19:07 -0400
Subject: [PATCH] add derivative theorems for norm

---
 .../Calculus/Monad/RevFDerivMonad.lean        |  1 +
 SciLean/Analysis/Calculus/RevFDeriv.lean      |  6 ++
 SciLean/Analysis/SpecialFunctions/Norm2.lean  | 79 ++++++++++++++++++-
 SciLean/Geometry/FrontierSpeed.lean           |  3 +
 4 files changed, 87 insertions(+), 2 deletions(-)

diff --git a/SciLean/Analysis/Calculus/Monad/RevFDerivMonad.lean b/SciLean/Analysis/Calculus/Monad/RevFDerivMonad.lean
index 3fdd7a75..73079276 100644
--- a/SciLean/Analysis/Calculus/Monad/RevFDerivMonad.lean
+++ b/SciLean/Analysis/Calculus/Monad/RevFDerivMonad.lean
@@ -139,6 +139,7 @@ by
     rw[revFDerivM_bind f (fun x => pure (g x))
          hf (DifferentiableM_pure _ hg)]
     simp[revFDerivM_pure g hg]
+  rfl
 
 @[fun_trans]
 theorem let_rule
diff --git a/SciLean/Analysis/Calculus/RevFDeriv.lean b/SciLean/Analysis/Calculus/RevFDeriv.lean
index df9a48eb..3e92b850 100644
--- a/SciLean/Analysis/Calculus/RevFDeriv.lean
+++ b/SciLean/Analysis/Calculus/RevFDeriv.lean
@@ -41,6 +41,12 @@ variable
   {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, AdjointSpace K (E i)] [∀ i, CompleteSpace (E i)]
 
 
+-- Basic simp lemmas -----------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[simp, simp_core]
+theorem revFDeriv_fst (f : X → Y) (x : X) : (revFDeriv K f x).1 = f x := by rfl
+
 -- Basic lambda calculus rules -------------------------------------------------
 --------------------------------------------------------------------------------
 
diff --git a/SciLean/Analysis/SpecialFunctions/Norm2.lean b/SciLean/Analysis/SpecialFunctions/Norm2.lean
index 895a7a01..0e83ab7d 100644
--- a/SciLean/Analysis/SpecialFunctions/Norm2.lean
+++ b/SciLean/Analysis/SpecialFunctions/Norm2.lean
@@ -1,4 +1,5 @@
 import SciLean.Analysis.SpecialFunctions.Inner
+import SciLean.Analysis.SpecialFunctions.Pow
 import SciLean.Meta.GenerateFunProp
 
 namespace SciLean
@@ -9,6 +10,7 @@ variable
   {R} [RealScalar R]
   {X} [NormedAddCommGroup X] [NormedSpace R X]
   {U} [NormedAddCommGroup U] [AdjointSpace R U] [CompleteSpace U]
+  {V} [NormedAddCommGroup V] [AdjointSpace R V] [CompleteSpace V]
 
 def_fun_prop with_transitive : Differentiable R (fun u : U => ‖u‖₂²[R]) by
   unfold Norm2.norm2; fun_prop [Norm2.norm2]
@@ -33,11 +35,84 @@ theorem Norm2.norm2.arg_a0.fwdFDeriv_rule :
   unfold fwdFDeriv
   fun_trans
 
-
 @[fun_trans]
 theorem Norm2.norm2.arg_a0.revFDeriv_rule :
     revFDeriv R (fun x : U => ‖x‖₂²[R])
     =
-    fun x => (‖x‖₂²[R], fun dr => (2 * dr)•x) := by
+    fun x =>
+      (‖x‖₂²[R], fun dy => (2 * dy) • x) := by
   unfold revFDeriv
   fun_trans [smul_smul]
+
+
+
+--  ‖·‖₂ --------------------------------------------------------------------------------------------
+----------------------------------------------------------------------------------------------------
+
+def_fun_prop (x : U) (hx : x ≠ 0) : DifferentiableAt R (norm₂ R) x by
+  unfold norm₂; simp[Norm2.norm2]; fun_prop (disch:=aesop)
+
+def_fun_prop (f : X → U) (hf : Differentiable R f) (hx' : ∀ x, f x ≠ 0) :
+    Differentiable R (fun x : X => ‖f x‖₂[R]) by intro x; fun_prop (disch:=aesop)
+
+
+-- TODO: how can we streamline writing all of these theorems?
+
+@[fun_trans]
+theorem norm₂.arg_x.fderiv_rule_at (x : U) (hx : x ≠ 0) :
+    fderiv R (fun x : U => ‖x‖₂[R]) x
+    =
+    fun dx =>L[R] ⟪dx,x⟫[R] / ‖x‖₂[R] := by
+  unfold norm₂; simp[Norm2.norm2]; fun_trans (disch:=aesop)
+  ext dx; simp
+  rw [← AdjointSpace.inner_conj_symm]
+  simp; ring
+
+@[fun_trans]
+theorem norm₂.arg_x.fderiv_rule (f : X → U) (hf : Differentiable R f) (hf' : ∀ x, f x ≠ 0) :
+    fderiv R (fun x => ‖f x‖₂[R])
+    =
+    fun x =>
+      let y := f x
+      fun dx =>L[R]
+        let dy := fderiv R f x dx
+        ⟪dy,y⟫[R] / ‖y‖₂[R] := by
+  funext x; fun_trans (disch:=aesop)
+
+@[fun_trans]
+theorem norm₂.arg_x.fwdFDeriv_rule_at (x : U) (hx : x ≠ 0) :
+    fwdFDeriv R (fun x : U => ‖x‖₂[R]) x
+    =
+    fun dx =>
+      let y := ‖x‖₂[R]
+      (y, ⟪dx,x⟫[R] / y) := by
+  unfold fwdFDeriv; fun_trans (disch:=assumption)
+
+@[fun_trans]
+theorem norm₂.arg_x.fwdFDeriv_rule (f : X → U) (hf : Differentiable R f) (hf' : ∀ x, f x ≠ 0) :
+    fwdFDeriv R (fun x => ‖f x‖₂[R])
+    =
+    fun x dx =>
+      let ydy := fwdFDeriv R f x dx
+      let yn := ‖ydy.1‖₂[R]
+      (yn, ⟪ydy.2,ydy.1⟫[R] / yn) := by
+  unfold fwdFDeriv; fun_trans (disch:=assumption)
+
+@[fun_trans]
+theorem norm₂.arg_x.revFDeriv_rule_at (x : U) (hx : x ≠ 0) :
+    revFDeriv R (fun x : U => ‖x‖₂[R]) x
+    =
+    let y := ‖x‖₂[R]
+    (y, fun dy => (y⁻¹ * dy) • x) := by
+  unfold revFDeriv; fun_trans (disch:=assumption) [smul_smul]
+
+
+@[fun_trans]
+theorem norm₂.arg_x.revFDeriv_rule (f : U → V) (hf : Differentiable R f) (hf' : ∀ x, f x ≠ 0) :
+    revFDeriv R (fun x : U => ‖f x‖₂[R])
+    =
+    fun x =>
+      let ydf := revFDeriv R f x
+      let y := ‖ydf.1‖₂[R]
+      (y, fun dy => ydf.2 ((y⁻¹ * dy) • ydf.1)) := by
+  funext x; fun_trans (disch:=apply hf')
diff --git a/SciLean/Geometry/FrontierSpeed.lean b/SciLean/Geometry/FrontierSpeed.lean
index bfbc52c7..fa647084 100644
--- a/SciLean/Geometry/FrontierSpeed.lean
+++ b/SciLean/Geometry/FrontierSpeed.lean
@@ -8,6 +8,7 @@ import SciLean.Tactic.Autodiff
 -- import SciLean.Tactic.GTrans
 
 set_option linter.unusedVariables false
+set_option deprecated.oldSectionVars true
 
 open MeasureTheory Topology Filter FiniteDimensional
 
@@ -145,6 +146,8 @@ theorem closedBall₂.arg_xr.frontierSpeed_rule :
   unfold closedBall₂
   funext w dw x
   conv => autodiff
+  set_option trace.Meta.Tactic.fun_trans true in
+  conv => autodiff
   simp[smul_sub]
 
 @[fun_trans]