basic definition of reverse derivative

lecopivo · Jul 27, 2023 · 2ea6000 · 2ea6000
1 parent b8c9503
commit 2ea6000
Show file tree

Hide file tree

Showing 3 changed files with 548 additions and 3 deletions.
diff --git a/SciLean/FTrans/Adjoint/Basic.lean b/SciLean/FTrans/Adjoint/Basic.lean
@@ -27,7 +27,6 @@ instance {E : ι → Type _} [∀ i, UniformSpace (E i)] [∀ i, CompleteSpace (
 
 -- Set up custom notation for adjoint. Mathlib's notation for adjoint seems to be broken
 instance (f : X →L[K] Y) : SciLean.Dagger f (ContinuousLinearMap.adjoint f : Y →L[K] X) := ⟨⟩
-variable (g : X → Y) (hg : SciLean.IsContinuousLinearMap K g)
 
 
 -- Basic lambda calculus rules -------------------------------------------------
@@ -237,7 +236,7 @@ by sorry
 --------------------------------------------------------------------------------
 
 @[ftrans_rule]
-theorem Prod.fst.arg_self.fderiv_comp
+theorem Prod.fst.arg_self.adjoint_comp
   (f : X → Y×Z) (hf : SciLean.IsContinuousLinearMap K f)
   : (fun x =>L[K] (f x).1)†
     =
@@ -250,7 +249,7 @@ by
 --------------------------------------------------------------------------------
 
 @[ftrans_rule]
-theorem Prod.snd.arg_self.fderiv_comp
+theorem Prod.snd.arg_self.adjoint_comp
   (f : X → Y×Z) (hf : SciLean.IsContinuousLinearMap K f)
   : (fun x =>L[K] (f x).2)†
     =

diff --git a/SciLean/FTrans/FDeriv/Basic.lean b/SciLean/FTrans/FDeriv/Basic.lean
@@ -135,6 +135,15 @@ theorem fderiv.pi_rule
   := by funext x; apply fderiv_pi (fun i => hf i x)
 
 
+theorem fderiv.proj_rule
+  [DecidableEq ι] (i : ι)
+  : (fderiv K fun (x : (i : ι) → E i) => x i)
+    =
+    fun x => fun dx =>L[K] dx i := 
+by 
+  funext x; sorry
+
+
 
 -- Register `fderiv` as function transformation --------------------------------
 --------------------------------------------------------------------------------