chore: forward-port leanprover-community/mathlib#19127 (#5889)

Mathlib/Analysis/Calculus/FDeriv/Mul.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Sébastien Gouëzel, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.calculus.fderiv.mul
-! leanprover-community/mathlib commit e3fb84046afd187b710170887195d50bada934ee
+! leanprover-community/mathlib commit d608fc5d4e69d4cc21885913fb573a88b0deb521
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -525,14 +525,112 @@ theorem hasFDerivAt_ring_inverse (x : Rˣ) :
   by simpa [hasFDerivAt_iff_isLittleO_nhds_zero] using this
 #align has_fderiv_at_ring_inverse hasFDerivAt_ring_inverse
 
-theorem differentiableAt_inverse (x : Rˣ) : DifferentiableAt 𝕜 (@Ring.inverse R _) x :=
-  (hasFDerivAt_ring_inverse x).differentiableAt
-#align differentiable_at_inverse differentiableAt_inverse
+theorem differentiableAt_inverse {x : R} (hx : IsUnit x) :
+    DifferentiableAt 𝕜 (@Ring.inverse R _) x :=
+  let ⟨u, hu⟩ := hx; hu ▸ (hasFDerivAt_ring_inverse u).differentiableAt
+
+theorem differentiableWithinAt_inverse {x : R} (hx : IsUnit x) (s : Set R) :
+    DifferentiableWithinAt 𝕜 (@Ring.inverse R _) s x :=
+  (differentiableAt_inverse hx).differentiableWithinAt
+#align differentiable_within_at_inverse differentiableWithinAt_inverse
+
+theorem differentiableOn_inverse : DifferentiableOn 𝕜 (@Ring.inverse R _) {x | IsUnit x} :=
+  fun _x hx => differentiableWithinAt_inverse hx _
+#align differentiable_on_inverse differentiableOn_inverse
 
 theorem fderiv_inverse (x : Rˣ) : fderiv 𝕜 (@Ring.inverse R _) x = -mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹ :=
   (hasFDerivAt_ring_inverse x).fderiv
 #align fderiv_inverse fderiv_inverse
 
+variable {h : E → R} {z : E} {S : Set E}
+
+theorem DifferentiableWithinAt.inverse (hf : DifferentiableWithinAt 𝕜 h S z) (hz : IsUnit (h z)) :
+    DifferentiableWithinAt 𝕜 (fun x => Ring.inverse (h x)) S z :=
+  (differentiableAt_inverse hz).comp_differentiableWithinAt z hf
+#align differentiable_within_at.inverse DifferentiableWithinAt.inverse
+
+@[simp]
+theorem DifferentiableAt.inverse (hf : DifferentiableAt 𝕜 h z) (hz : IsUnit (h z)) :
+    DifferentiableAt 𝕜 (fun x => Ring.inverse (h x)) z :=
+  (differentiableAt_inverse hz).comp z hf
+#align differentiable_at.inverse DifferentiableAt.inverse
+
+theorem DifferentiableOn.inverse (hf : DifferentiableOn 𝕜 h S) (hz : ∀ x ∈ S, IsUnit (h x)) :
+    DifferentiableOn 𝕜 (fun x => Ring.inverse (h x)) S := fun x h => (hf x h).inverse (hz x h)
+#align differentiable_on.inverse DifferentiableOn.inverse
+
+@[simp]
+theorem Differentiable.inverse (hf : Differentiable 𝕜 h) (hz : ∀ x, IsUnit (h x)) :
+    Differentiable 𝕜 fun x => Ring.inverse (h x) := fun x => (hf x).inverse (hz x)
+#align differentiable.inverse Differentiable.inverse
+
 end AlgebraInverse
 
+/-! ### Derivative of the inverse in a division ring
+
+Note these lemmas are primed as they need `complete_space R`, whereas the other lemmas in
+`deriv/inv.lean` do not, but instead need `nontrivially_normed_field R`.
+-/
+
+section DivisionRingInverse
+
+variable {R : Type _} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R]
+
+open NormedRing ContinuousLinearMap Ring
+
+/-- At an invertible element `x` of a normed division algebra `R`, the Fréchet derivative of the
+inversion operation is the linear map `λ t, - x⁻¹ * t * x⁻¹`. -/
+theorem hasFDerivAt_inv' {x : R} (hx : x ≠ 0) : HasFDerivAt Inv.inv (-mulLeftRight 𝕜 R x⁻¹ x⁻¹) x :=
+  by simpa using hasFDerivAt_ring_inverse (Units.mk0 _ hx)
+#align has_fderiv_at_inv' hasFDerivAt_inv'
+
+theorem differentiableAt_inv' {x : R} (hx : x ≠ 0) : DifferentiableAt 𝕜 Inv.inv x :=
+  (hasFDerivAt_inv' hx).differentiableAt
+#align differentiable_at_inv' differentiableAt_inv'
+
+theorem differentiableWithinAt_inv' {x : R} (hx : x ≠ 0) (s : Set R) :
+    DifferentiableWithinAt 𝕜 (fun x => x⁻¹) s x :=
+  (differentiableAt_inv' hx).differentiableWithinAt
+#align differentiable_within_at_inv' differentiableWithinAt_inv'
+
+theorem differentiableOn_inv' : DifferentiableOn 𝕜 (fun x : R => x⁻¹) {x | x ≠ 0} := fun _x hx =>
+  differentiableWithinAt_inv' hx _
+#align differentiable_on_inv' differentiableOn_inv'
+
+/-- Non-commutative version of `fderiv_inv` -/
+theorem fderiv_inv' {x : R} (hx : x ≠ 0) : fderiv 𝕜 Inv.inv x = -mulLeftRight 𝕜 R x⁻¹ x⁻¹ :=
+  (hasFDerivAt_inv' hx).fderiv
+#align fderiv_inv' fderiv_inv'
+
+/-- Non-commutative version of `fderiv_within_inv` -/
+theorem fderivWithin_inv' {s : Set R} {x : R} (hx : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
+    fderivWithin 𝕜 (fun x => x⁻¹) s x = -mulLeftRight 𝕜 R x⁻¹ x⁻¹ := by
+  rw [DifferentiableAt.fderivWithin (differentiableAt_inv' hx) hxs]
+  exact fderiv_inv' hx
+#align fderiv_within_inv' fderivWithin_inv'
+
+variable {h : E → R} {z : E} {S : Set E}
+
+theorem DifferentiableWithinAt.inv' (hf : DifferentiableWithinAt 𝕜 h S z) (hz : h z ≠ 0) :
+    DifferentiableWithinAt 𝕜 (fun x => (h x)⁻¹) S z :=
+  (differentiableAt_inv' hz).comp_differentiableWithinAt z hf
+#align differentiable_within_at.inv' DifferentiableWithinAt.inv'
+
+@[simp]
+theorem DifferentiableAt.inv' (hf : DifferentiableAt 𝕜 h z) (hz : h z ≠ 0) :
+    DifferentiableAt 𝕜 (fun x => (h x)⁻¹) z :=
+  (differentiableAt_inv' hz).comp z hf
+#align differentiable_at.inv' DifferentiableAt.inv'
+
+theorem DifferentiableOn.inv' (hf : DifferentiableOn 𝕜 h S) (hz : ∀ x ∈ S, h x ≠ 0) :
+    DifferentiableOn 𝕜 (fun x => (h x)⁻¹) S := fun x h => (hf x h).inv' (hz x h)
+#align differentiable_on.inv' DifferentiableOn.inv'
+
+@[simp]
+theorem Differentiable.inv' (hf : Differentiable 𝕜 h) (hz : ∀ x, h x ≠ 0) :
+    Differentiable 𝕜 fun x => (h x)⁻¹ := fun x => (hf x).inv' (hz x)
+#align differentiable.inv' Differentiable.inv'
+
+end DivisionRingInverse
+
 end

Mathlib/Analysis/NormedSpace/Spectrum.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 
 ! This file was ported from Lean 3 source module analysis.normed_space.spectrum
-! leanprover-community/mathlib commit 58a272265b5e05f258161260dd2c5d247213cbd3
+! leanprover-community/mathlib commit d608fc5d4e69d4cc21885913fb573a88b0deb521
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -330,7 +330,7 @@ theorem differentiableOn_inverse_one_sub_smul [CompleteSpace A] {a : A} {r : ℝ
     simpa only [norm_toNNReal, Real.toNNReal_coe] using
       Real.toNNReal_mono (mem_closedBall_zero_iff.mp z_mem)
   have H₁ : Differentiable 𝕜 fun w : 𝕜 => 1 - w • a := (differentiable_id.smul_const a).const_sub 1
-  exact DifferentiableAt.comp z (differentiableAt_inverse hu.unit) H₁.differentiableAt
+  exact DifferentiableAt.comp z (differentiableAt_inverse hu) H₁.differentiableAt
 #align spectrum.differentiable_on_inverse_one_sub_smul spectrum.differentiableOn_inverse_one_sub_smul
 
 end OneSubSmul