derivative theorems for Inv.inv

SciLean/Analysis/Calculus/FDeriv.lean

@@ -68,7 +68,7 @@ theorem fderiv.comp_rule_at
       dz :=
 by
   rw[show (fun x => f (g x)) = f ∘ g by rfl]
-  rw[fderiv.comp x hf hg]
+  rw[fderiv_comp x hf hg]
   ext dx; simp
 
 @[fun_trans]
@@ -103,7 +103,7 @@ by
   conv =>
     lhs
     rw[h]
-    rw[fderiv.comp x hf (DifferentiableAt.prod (by simp) hg)]
+    rw[fderiv_comp x hf (DifferentiableAt.prod (by simp) hg)]
     rw[DifferentiableAt.fderiv_prod (by simp) hg]
   ext dx; simp[ContinuousLinearMap.comp]
 
@@ -317,6 +317,35 @@ theorem HDiv.hDiv.arg_a0a1.fderiv_rule_at
   simp
 
 
+-- Inv.inv -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+set_option linter.unusedVariables false in
+@[fun_prop]
+theorem _root_.Inv.inv.arg_a0.DifferentiableAt_rule
+    {R} [RCLike R]
+    {W} [NormedAddCommGroup W] [NormedSpace R W]
+    (w : W) (a0 : W → R)
+    (ha0 : DifferentiableAt R a0 w) (ha0' : a0 w ≠ 0) :
+    DifferentiableAt R (fun w => (a0 w)⁻¹) w := sorry_proof
+
+@[fun_trans]
+theorem HInv.hInv.arg_a0a1.fderiv_rule_at
+    (x : X) (f : X → K)
+    (hf : DifferentiableAt K f x) (hx : f x ≠ 0) :
+    (fderiv K fun x => (f x)⁻¹) x
+    =
+    let y := f x
+    fun dx =>L[K]
+      let dy := fderiv K f x dx
+      (-dy) / y^2 := by
+  ext dx
+  rw[fderiv_comp']
+  rw[fderiv_inv]
+  simp; ring
+  apply differentiableAt_inv hx
+  apply hf
+
+
 -- HPow.hPow ---------------------------------------------------------------------
 --------------------------------------------------------------------------------
 

SciLean/Analysis/Calculus/FwdFDeriv.lean

@@ -329,6 +329,22 @@ theorem HDiv.hDiv.arg_a0a1.fwdFDeriv_rule_at (x : X)
   field_simp ; sorry_proof --ring
 
 
+-- Inv.inv -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+@[fun_trans]
+theorem HInv.hInv.arg_a0a1.fwdFDeriv_rule_at
+    (x : X) (f : X → K)
+    (hf : DifferentiableAt K f x) (hx : f x ≠ 0) :
+    (fwdFDeriv K fun x => (f x)⁻¹) x
+    =
+    fun dx =>
+      let ydy := fwdFDeriv K f x dx
+      let y := ydy.1
+      let dy := ydy.2
+      (y⁻¹, -dy / y^2) := by
+  unfold fwdFDeriv; fun_trans (disch:=assumption)
+
+
 -- HPow.hPow -------------------------------------------------------------------
 --------------------------------------------------------------------------------
 

SciLean/Analysis/Calculus/RevFDeriv.lean

@@ -458,6 +458,21 @@ theorem HDiv.hDiv.arg_a0a1.revFDeriv_rule
   fun_trans (disch:=apply hx)
 
 
+-- Inv.inv -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+@[fun_trans]
+theorem HInv.hInv.arg_a0a1.revFDeriv_rule_at
+    (x : X) (f : X → K)
+    (hf : DifferentiableAt K f x) (hx : f x ≠ 0) :
+    (revFDeriv K fun x => (f x)⁻¹) x
+    =
+    let ydf := revFDeriv K f x
+    let y := ydf.1
+    let df := ydf.2
+    (y⁻¹, fun dy => - (conj y^2)⁻¹ • (df dy)) := by
+  unfold revFDeriv; fun_trans (disch:=assumption)
+
+
 -- HPow.hPow ---------------------------------------------------------------------
 --------------------------------------------------------------------------------