Merge branch 'let_alt'

lecopivo · Oct 4, 2023 · e7f7fb5 · e7f7fb5
2 parents 53e4dc2 + 1098375
commit e7f7fb5
Show file tree

Hide file tree

Showing 14 changed files with 627 additions and 112 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/FunctionPropositions/IsDifferentiable.lean b/SciLean/Core/FunctionPropositions/IsDifferentiable.lean
@@ -1,5 +1,6 @@
 import SciLean.Core.Objects.Scalar
 import SciLean.Core.Objects.SemiInnerProductSpace
+import SciLean.Core.Objects.FinVec
 
 import SciLean.Core.FunctionPropositions.IsDifferentiableAt
 
@@ -272,6 +273,20 @@ def HSMul.hSMul.arg_a0a1.IsDifferentiable_rule
   : IsDifferentiable K (fun x => f x • g x)
   := by sorry_proof
 
+@[fprop]
+theorem HSMul.hSMul.arg_a1.IsDifferentiable_rule_nat
+  (c : ℕ) (f : X → Y) (hf : IsDifferentiable K f)
+  : IsDifferentiable K fun x => c • f x :=
+by
+  sorry_proof
+
+@[fprop]
+theorem HSMul.hSMul.arg_a1.IsDifferentiable_rule_int
+  (c : ℤ) (f : X → Y) (hf : IsDifferentiable K f)
+  : IsDifferentiable K fun x => c • f x :=
+by
+  sorry_proof
+
 
 -- HDiv.hDiv -------------------------------------------------------------------
 -------------------------------------------------------------------------------- 
@@ -348,3 +363,34 @@ by
 
 
 end InnerProductSpace
+
+--------------------------------------------------------------------------------
+
+namespace SciLean
+section OnFinVec 
+
+
+variable 
+  {K : Type _} [IsROrC K]
+  {IX : Type} [EnumType IX] {X : Type _} [FinVec IX K X]
+  {IY : Type} [EnumType IY] {Y : Type _} [FinVec IY K Y]
+  {IZ : Type} [EnumType IZ] {Z : Type _} [FinVec IZ K Z]
+
+@[fprop]
+theorem Basis.proj.arg_x.IsDifferentiable_rule (i : IX)
+  : IsDifferentiable K (fun x : X => ℼ i x) := by sorry_proof
+
+@[fprop]
+theorem DualBasis.dualProj.arg_x.IsDifferentiable_rule (i : IX)
+  : IsDifferentiable K (fun x : X => ℼ' i x) := by sorry_proof
+
+@[fprop]
+theorem BasisDuality.toDual.arg_x.IsDifferentiable_rule
+  : IsDifferentiable K (fun x : X => BasisDuality.toDual x) := by sorry_proof
+
+@[fprop]
+theorem BasisDuality.fromDual.arg_x.IsDifferentiable_rule
+  : IsDifferentiable K (fun x : X => BasisDuality.fromDual x) := by sorry_proof
+
+end OnFinVec
+end SciLean