somewhat dubious fprop rules for the linear part of revCDeriv

lecopivo · Oct 4, 2023 · 1098375 · 1098375
1 parent 976cedd
commit 1098375
Show file tree

Hide file tree

Showing 4 changed files with 34 additions and 8 deletions.
diff --git a/SciLean/Core/FunctionPropositions/Diffeomorphism.lean b/SciLean/Core/FunctionPropositions/Diffeomorphism.lean
@@ -213,7 +213,7 @@ by
   constructor
   . fprop
   . fprop
-  . ftrans; simp; fprop
+  . ftrans; fprop
 
 @[fprop]
 def HMul.hMul.arg_a1.Diffeomorphism_rule
@@ -224,7 +224,7 @@ by
   constructor
   . fprop
   . fprop
-  . ftrans; simp; fprop
+  . ftrans; fprop
 
 
 -- SMul.sMul -------------------------------------------------------------------
@@ -239,7 +239,7 @@ by
   constructor
   . fprop
   . fprop
-  . ftrans; simp; fprop
+  . ftrans; fprop
 
 
 -- HDiv.hDiv -------------------------------------------------------------------
@@ -255,7 +255,7 @@ by
   constructor
   . fprop
   . fprop
-  . ftrans; sorry_proof 
+  . ftrans; sorry_proof
 
 
 -- HPow.hPow -------------------------------------------------------------------

diff --git a/SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean b/SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean
@@ -467,9 +467,11 @@ end InnerProductSpace
 
 @[fprop]
 theorem SciLean.semiAdjoint.arg_a3.HasSemiAdjoint_rule
-  (f : X → Y) (a0 : W → Y) (hf : HasSemiAdjoint K f) (ha0 : HasSemiAdjoint K a0)
+  (f : X → Y) (a0 : W → Y) (ha0 : HasSemiAdjoint K a0)
   : HasSemiAdjoint K (fun w => semiAdjoint K f (a0 w)) :=
 by
+  -- either `f` has semiadjoint then the total adjoint id `a0† f†`
+  -- or `f` does not have semiadjoint and `f†` is zero thus map and that has adjoint
   sorry_proof
 
 
diff --git a/SciLean/Core/FunctionTransformations/RevCDeriv.lean b/SciLean/Core/FunctionTransformations/RevCDeriv.lean
@@ -1245,11 +1245,35 @@ theorem SciLean.semiAdjoint.arg_a3.revCDeriv_rule
     fun w => 
       let ada := revCDeriv K a0 w
       (semiAdjoint K f ada.1,
-       fun dx => 
-         ada.2 (f dx)) := 
+       fun dx => ada.2 (f dx)) := 
 by
   have ⟨_,_⟩ := ha0
   unfold revCDeriv
   funext x; simp; ftrans; ftrans
 
 
+-- slightly odd rules that are needed when dealing with expressions like:
+--
+--  let ydg := <∂ (x':=x), g x'
+--  <∂ (x':=x), semiAdjoint K ydg.2 (x' - x)
+--
+-- here we need to know that `ydg.2` has semi-adjoint
+--
+-- TODO: `fprop` is not designed to use rules like this! It works mainly by accident
+--       fom the support for monadic `fwd/revCDerivValM`. This should have first 
+--       class support.
+@[fprop]
+theorem Prod.snd.arg.IsDifferentiable_rule_of_revCDeriv 
+  (f : X → Y) (x : X) (hf : HasAdjDiff K f) 
+  : IsDifferentiable K (revCDeriv K f x).2 := by unfold revCDeriv; simp; fprop
+
+@[fprop]
+theorem Prod.snd.arg.HasSemiAdjoint_rule_revCDeriv 
+  (f : X → Y) (x : X) (hf : HasAdjDiff K f) 
+  : HasSemiAdjoint K (revCDeriv K f x).2 := by unfold revCDeriv; simp; fprop
+
+@[fprop]
+theorem Prod.snd.arg.HasAdjDiff_rule_revCDeriv 
+  (f : X → Y) (x : X)
+  : HasAdjDiff K (revCDeriv K f x).2 := by unfold revCDeriv; simp; fprop
+
diff --git a/SciLean/Core/Monads/StateT.lean b/SciLean/Core/Monads/StateT.lean
@@ -415,7 +415,7 @@ theorem _root_.modifyThe.arg_f.revDerivM_rule
               pure dxs.1)) := 
 by 
   simp[modifyThe, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet,revDerivM, bind, StateT.bind, getThe, MonadStateOf.get, StateT.get, setThe, set, StateT.set]
-  ftrans; simp; congr
+  ftrans; congr
 
 
 -- modify ----------------------------------------------------------------------