differentiation rules for HPow R Nat R

lecopivo · Jul 26, 2023 · 9008600 · 9008600
1 parent a690ecf
commit 9008600
Show file tree

Hide file tree

Showing 3 changed files with 47 additions and 0 deletions.
diff --git a/SciLean/FTrans/FwdDeriv/Basic.lean b/SciLean/FTrans/FwdDeriv/Basic.lean
@@ -468,3 +468,30 @@ theorem HDiv.hDiv.arg_a4a5.fwdDeriv_comp
       (ydy.1 / zdz.1, (ydy.2 * zdz.1 - ydy.1 * zdz.2) / zdz.1^2) :=
 by 
   unfold fwdDeriv; ftrans
+
+
+-- HPow.hPow ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[ftrans_rule]
+def HPow.hPow.arg_a4.fwdDeriv_at_comp
+  (n : Nat) (x : X) (f : X → K) (hf : DifferentiableAt K f x) 
+  : fwdDeriv K (fun x => f x ^ n) x
+    =
+    fun dx =>
+      let ydy := fwdDeriv K f x dx
+      (ydy.1 ^ n, n * ydy.2 * (ydy.1 ^ (n-1))) :=
+by 
+  unfold fwdDeriv; ftrans
+
+
+@[ftrans_rule]
+def HPow.hPow.arg_a4.fwdDeriv_comp
+  (n : Nat) (f : X → K) (hf : Differentiable K f) 
+  : fwdDeriv K (fun x => f x ^ n)
+    =
+    fun x dx =>
+      let ydy := fwdDeriv K f x dx
+      (ydy.1 ^ n, n * ydy.2 * (ydy.1 ^ (n-1))) :=
+by 
+  unfold fwdDeriv; ftrans
diff --git a/SciLean/FunctionSpaces/Differentiable/Basic.lean b/SciLean/FunctionSpaces/Differentiable/Basic.lean
@@ -299,3 +299,14 @@ def HDiv.hDiv.arg_a4a5.Differentiable_comp
   (hf : Differentiable R f) (hg : Differentiable R g) (hx : ∀ x, g x ≠ 0)
   : Differentiable R (fun x => f x / g x)
   := Differentiable.div hf hg hx
+
+
+
+-- HPow.hPow ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[fprop_rule]
+def HPow.hPow.arg_a4a5.Differentiable_comp
+  (n : Nat) (f : X → R) (hf : Differentiable R f) 
+  : Differentiable R (fun x => f x ^ n)
+  := Differentiable.pow hf n
diff --git a/SciLean/FunctionSpaces/DifferentiableAt/Basic.lean b/SciLean/FunctionSpaces/DifferentiableAt/Basic.lean
@@ -312,3 +312,12 @@ def HDiv.hDiv.arg_a4a5.DifferentiableAt_comp
   : DifferentiableAt R (fun x => f x / g x) x 
   := DifferentiableAt.div hf hg hx
 
+
+-- HPow.hPow ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[fprop_rule]
+def HPow.hPow.arg_a4a5.DifferentiableAt_comp
+  (n : Nat) (x : X) (f : X → R) (hf : DifferentiableAt R f x) 
+  : DifferentiableAt R (fun x => f x ^ n) x
+  := DifferentiableAt.pow hf n