feat: define HasSummableGeomSeries to unify results between normed …

…field and complete normed algebras (#17002)

Currently, several analogous results are proved separately in complete normed algebras, and in normed fields. For instance, the fact that inversion is differentiable is called `differentiableAt_inv'` in the former, and `differentiableAt_inv` in the latter, with similar proofs relying on the convergence of geometric series, due to completeness in the former and to the existence of the inverse in the latter.

We unify these results by defining a typeclass `HasSummableGeomSeries` saying that `∑ x ^ n` converges for all `x` with norm `< 1`. We show that this is satisfied both in complete normed rings and in normed fields. And we show that many results follow solely from this assumption, deduplicating statements and proofs.

Along the way, we show that inversion is analytic on rings with summable geometric series, and deduce in particular that it is strictly differentiable, clearing an existing TODO. This adds a few imports (importing analytic functions in files where they were not needed before), but with the upcoming refactor of smooth functions, analytic functions will in any case need to be imported earlier on, so this doesn't look like a real issue to me.

Mathlib/Analysis/Analytic/Constructions.lean

@@ -6,6 +6,7 @@ Authors: David Loeffler, Geoffrey Irving
 import Mathlib.Analysis.Analytic.Composition
 import Mathlib.Analysis.Analytic.Linear
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Mul
+import Mathlib.Analysis.Normed.Ring.Units
 
 /-!
 # Various ways to combine analytic functions
@@ -603,19 +604,36 @@ lemma AnalyticOn.pow {f : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (n : 
 section Geometric
 
 variable (𝕜 A : Type*) [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A]
-  [NormOneClass A]
 
 /-- The geometric series `1 + x + x ^ 2 + ...` as a `FormalMultilinearSeries`. -/
 def formalMultilinearSeries_geometric : FormalMultilinearSeries 𝕜 A A :=
   fun n ↦ ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A
 
-lemma formalMultilinearSeries_geometric_apply_norm (n : ℕ) :
+lemma formalMultilinearSeries_geometric_apply_norm_le (n : ℕ) :
+    ‖formalMultilinearSeries_geometric 𝕜 A n‖ ≤ max 1 ‖(1 : A)‖ :=
+  ContinuousMultilinearMap.norm_mkPiAlgebraFin_le
+
+lemma formalMultilinearSeries_geometric_apply_norm [NormOneClass A] (n : ℕ) :
     ‖formalMultilinearSeries_geometric 𝕜 A n‖ = 1 :=
   ContinuousMultilinearMap.norm_mkPiAlgebraFin
 
 end Geometric
 
-lemma formalMultilinearSeries_geometric_radius (𝕜) [NontriviallyNormedField 𝕜]
+lemma one_le_formalMultilinearSeries_geometric_radius (𝕜 : Type*) [NontriviallyNormedField 𝕜]
+    (A : Type*) [NormedRing A] [NormedAlgebra 𝕜 A] :
+    1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius := by
+  refine le_of_forall_nnreal_lt (fun r hr ↦ ?_)
+  rw [← Nat.cast_one, ENNReal.coe_lt_natCast, Nat.cast_one] at hr
+  apply FormalMultilinearSeries.le_radius_of_isBigO
+  apply isBigO_of_le' (c := max 1 ‖(1 : A)‖) atTop (fun n ↦ ?_)
+  simp only [norm_mul, norm_norm, norm_pow, Real.norm_eq_abs, NNReal.abs_eq, norm_one, mul_one,
+    abs_norm]
+  apply le_trans ?_ (formalMultilinearSeries_geometric_apply_norm_le 𝕜 A n)
+  conv_rhs => rw [← mul_one (‖formalMultilinearSeries_geometric 𝕜 A n‖)]
+  gcongr
+  exact pow_le_one _ (coe_nonneg r) hr.le
+
+lemma formalMultilinearSeries_geometric_radius (𝕜 : Type*) [NontriviallyNormedField 𝕜]
     (A : Type*) [NormedRing A] [NormOneClass A] [NormedAlgebra 𝕜 A] :
     (formalMultilinearSeries_geometric 𝕜 A).radius = 1 := by
   apply le_antisymm
@@ -641,20 +659,61 @@ lemma formalMultilinearSeries_geometric_radius (𝕜) [NontriviallyNormedField 
     rw [norm_one, Real.norm_of_nonneg (pow_nonneg (coe_nonneg r) _)]
     exact pow_le_one _ (coe_nonneg r) hr.le
 
-lemma hasFPowerSeriesOnBall_inv_one_sub
-    (𝕜 𝕝 : Type*) [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝] :
-    HasFPowerSeriesOnBall (fun x : 𝕝 ↦ (1 - x)⁻¹) (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1 := by
+lemma hasFPowerSeriesOnBall_inverse_one_sub
+    (𝕜 : Type*) [NontriviallyNormedField 𝕜]
+    (A : Type*) [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] :
+    HasFPowerSeriesOnBall (fun x : A ↦ Ring.inverse (1 - x))
+      (formalMultilinearSeries_geometric 𝕜 A) 0 1 := by
   constructor
-  · exact le_of_eq (formalMultilinearSeries_geometric_radius 𝕜 𝕝).symm
+  · exact one_le_formalMultilinearSeries_geometric_radius 𝕜 A
   · exact one_pos
   · intro y hy
-    simp_rw [zero_add, formalMultilinearSeries_geometric,
-        ContinuousMultilinearMap.mkPiAlgebraFin_apply,
-        List.prod_ofFn, Finset.prod_const,
-        Finset.card_univ, Fintype.card_fin]
-    apply hasSum_geometric_of_norm_lt_one
-    simpa only [← ofReal_one, Metric.emetric_ball, Metric.ball,
-      dist_eq_norm, sub_zero] using hy
+    simp only [EMetric.mem_ball, edist_dist, dist_zero_right, ofReal_lt_one] at hy
+    simp only [zero_add, NormedRing.inverse_one_sub _ hy, Units.oneSub, Units.inv_mk,
+      formalMultilinearSeries_geometric, ContinuousMultilinearMap.mkPiAlgebraFin_apply,
+      List.ofFn_const, List.prod_replicate]
+    exact (summable_geometric_of_norm_lt_one hy).hasSum
+
+lemma analyticAt_inverse_one_sub (𝕜 : Type*) [NontriviallyNormedField 𝕜]
+    (A : Type*) [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] :
+    AnalyticAt 𝕜 (fun x : A ↦ Ring.inverse (1 - x)) 0 :=
+  ⟨_, ⟨_, hasFPowerSeriesOnBall_inverse_one_sub 𝕜 A⟩⟩
+
+/-- If `A` is a normed algebra over `𝕜` with summable geometric series, then inversion on `A` is
+analytic at any unit. -/
+lemma analyticAt_inverse {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+    {A : Type*} [NormedRing A] [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] (z : Aˣ) :
+    AnalyticAt 𝕜 Ring.inverse (z : A) := by
+  rcases subsingleton_or_nontrivial A with hA|hA
+  · convert analyticAt_const (v := (0 : A))
+  · let f1 : A → A := fun a ↦ a * z.inv
+    let f2 : A → A := fun b ↦ Ring.inverse (1 - b)
+    let f3 : A → A := fun c ↦ 1 - z.inv * c
+    have feq : ∀ᶠ y in 𝓝 (z : A), (f1 ∘ f2 ∘ f3) y = Ring.inverse y := by
+      have : Metric.ball (z : A) (‖(↑z⁻¹ : A)‖⁻¹) ∈ 𝓝 (z : A) := by
+        apply Metric.ball_mem_nhds
+        simp
+      filter_upwards [this] with y hy
+      simp only [Metric.mem_ball, dist_eq_norm] at hy
+      have : y = Units.ofNearby z y hy := rfl
+      rw [this, Eq.comm]
+      simp only [Ring.inverse_unit, Function.comp_apply]
+      simp [Units.ofNearby, f1, f2, f3, Units.add, _root_.mul_sub]
+      rw [← Ring.inverse_unit]
+      congr
+      simp
+    apply AnalyticAt.congr _ feq
+    apply (analyticAt_id.mul analyticAt_const).comp
+    apply AnalyticAt.comp
+    · simp only [Units.inv_eq_val_inv, Units.inv_mul, sub_self, f2, f3]
+      exact analyticAt_inverse_one_sub 𝕜 A
+    · exact analyticAt_const.sub (analyticAt_const.mul analyticAt_id)
+
+lemma hasFPowerSeriesOnBall_inv_one_sub
+    (𝕜 𝕝 : Type*) [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝] :
+    HasFPowerSeriesOnBall (fun x : 𝕝 ↦ (1 - x)⁻¹) (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1 := by
+  convert hasFPowerSeriesOnBall_inverse_one_sub 𝕜 𝕝
+  exact Ring.inverse_eq_inv'.symm
 
 lemma analyticAt_inv_one_sub (𝕝 : Type*) [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝] :
     AnalyticAt 𝕜 (fun x : 𝕝 ↦ (1 - x)⁻¹) 0 :=
@@ -663,19 +722,8 @@ lemma analyticAt_inv_one_sub (𝕝 : Type*) [NontriviallyNormedField 𝕝] [Norm
 /-- If `𝕝` is a normed field extension of `𝕜`, then the inverse map `𝕝 → 𝕝` is `𝕜`-analytic
 away from 0. -/
 lemma analyticAt_inv {z : 𝕝} (hz : z ≠ 0) : AnalyticAt 𝕜 Inv.inv z := by
-  let f1 : 𝕝 → 𝕝 := fun a ↦ 1 / z * a
-  let f2 : 𝕝 → 𝕝 := fun b ↦ (1 - b)⁻¹
-  let f3 : 𝕝 → 𝕝 := fun c ↦ 1 - c / z
-  have feq : f1 ∘ f2 ∘ f3 = Inv.inv := by
-    ext1 x
-    dsimp only [f1, f2, f3, Function.comp_apply]
-    field_simp
-  have f3val : f3 z = 0 := by simp only [f3, div_self hz, sub_self]
-  have f3an : AnalyticAt 𝕜 f3 z := by
-    apply analyticAt_const.sub
-    simpa only [div_eq_inv_mul] using analyticAt_const.mul analyticAt_id
-  exact feq ▸ (analyticAt_const.mul analyticAt_id).comp
-    ((f3val.symm ▸ analyticAt_inv_one_sub 𝕝).comp f3an)
+  convert analyticAt_inverse (𝕜 := 𝕜) (Units.mk0 _ hz)
+  exact Ring.inverse_eq_inv'.symm
 
 /-- `x⁻¹` is analytic away from zero -/
 lemma analyticOn_inv : AnalyticOn 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0} := by

Mathlib/Analysis/Calculus/Deriv/Inv.lean

@@ -63,20 +63,13 @@ theorem hasDerivWithinAt_inv (x_ne_zero : x ≠ 0) (s : Set 𝕜) :
     HasDerivWithinAt (fun x => x⁻¹) (-(x ^ 2)⁻¹) s x :=
   (hasDerivAt_inv x_ne_zero).hasDerivWithinAt
 
-theorem differentiableAt_inv : DifferentiableAt 𝕜 (fun x => x⁻¹) x ↔ x ≠ 0 :=
+theorem differentiableAt_inv_iff : DifferentiableAt 𝕜 (fun x => x⁻¹) x ↔ x ≠ 0 :=
   ⟨fun H => NormedField.continuousAt_inv.1 H.continuousAt, fun H =>
     (hasDerivAt_inv H).differentiableAt⟩
 
-theorem differentiableWithinAt_inv (x_ne_zero : x ≠ 0) :
-    DifferentiableWithinAt 𝕜 (fun x => x⁻¹) s x :=
-  (differentiableAt_inv.2 x_ne_zero).differentiableWithinAt
-
-theorem differentiableOn_inv : DifferentiableOn 𝕜 (fun x : 𝕜 => x⁻¹) { x | x ≠ 0 } := fun _x hx =>
-  differentiableWithinAt_inv hx
-
 theorem deriv_inv : deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹ := by
   rcases eq_or_ne x 0 with (rfl | hne)
-  · simp [deriv_zero_of_not_differentiableAt (mt differentiableAt_inv.1 (not_not.2 rfl))]
+  · simp [deriv_zero_of_not_differentiableAt (mt differentiableAt_inv_iff.1 (not_not.2 rfl))]
   · exact (hasDerivAt_inv hne).deriv
 
 @[simp]
@@ -85,13 +78,17 @@ theorem deriv_inv' : (deriv fun x : 𝕜 => x⁻¹) = fun x => -(x ^ 2)⁻¹ :=
 
 theorem derivWithin_inv (x_ne_zero : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
     derivWithin (fun x => x⁻¹) s x = -(x ^ 2)⁻¹ := by
-  rw [DifferentiableAt.derivWithin (differentiableAt_inv.2 x_ne_zero) hxs]
+  rw [DifferentiableAt.derivWithin (differentiableAt_inv x_ne_zero) hxs]
   exact deriv_inv
 
 theorem hasFDerivAt_inv (x_ne_zero : x ≠ 0) :
     HasFDerivAt (fun x => x⁻¹) (smulRight (1 : 𝕜 →L[𝕜] 𝕜) (-(x ^ 2)⁻¹) : 𝕜 →L[𝕜] 𝕜) x :=
   hasDerivAt_inv x_ne_zero
 
+theorem hasStrictFDerivAt_inv (x_ne_zero : x ≠ 0) :
+    HasStrictFDerivAt (fun x => x⁻¹) (smulRight (1 : 𝕜 →L[𝕜] 𝕜) (-(x ^ 2)⁻¹) : 𝕜 →L[𝕜] 𝕜) x :=
+  hasStrictDerivAt_inv x_ne_zero
+
 theorem hasFDerivWithinAt_inv (x_ne_zero : x ≠ 0) :
     HasFDerivWithinAt (fun x => x⁻¹) (smulRight (1 : 𝕜 →L[𝕜] 𝕜) (-(x ^ 2)⁻¹) : 𝕜 →L[𝕜] 𝕜) s x :=
   (hasFDerivAt_inv x_ne_zero).hasFDerivWithinAt
@@ -101,7 +98,7 @@ theorem fderiv_inv : fderiv 𝕜 (fun x => x⁻¹) x = smulRight (1 : 𝕜 →L[
 
 theorem fderivWithin_inv (x_ne_zero : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
     fderivWithin 𝕜 (fun x => x⁻¹) s x = smulRight (1 : 𝕜 →L[𝕜] 𝕜) (-(x ^ 2)⁻¹) := by
-  rw [DifferentiableAt.fderivWithin (differentiableAt_inv.2 x_ne_zero) hxs]
+  rw [DifferentiableAt.fderivWithin (differentiableAt_inv x_ne_zero) hxs]
   exact fderiv_inv
 
 variable {c : 𝕜 → 𝕜} {h : E → 𝕜} {c' : 𝕜} {z : E} {S : Set E}
@@ -116,22 +113,6 @@ theorem HasDerivAt.inv (hc : HasDerivAt c c' x) (hx : c x ≠ 0) :
   rw [← hasDerivWithinAt_univ] at *
   exact hc.inv hx
 
-theorem DifferentiableWithinAt.inv (hf : DifferentiableWithinAt 𝕜 h S z) (hz : h z ≠ 0) :
-    DifferentiableWithinAt 𝕜 (fun x => (h x)⁻¹) S z :=
-  (differentiableAt_inv.mpr hz).comp_differentiableWithinAt z hf
-
-@[simp]
-theorem DifferentiableAt.inv (hf : DifferentiableAt 𝕜 h z) (hz : h z ≠ 0) :
-    DifferentiableAt 𝕜 (fun x => (h x)⁻¹) z :=
-  (differentiableAt_inv.mpr hz).comp z hf
-
-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)
-
-@[simp]
-theorem Differentiable.inv (hf : Differentiable 𝕜 h) (hz : ∀ x, h x ≠ 0) :
-    Differentiable 𝕜 fun x => (h x)⁻¹ := fun x => (hf x).inv (hz x)
-
 theorem derivWithin_inv' (hc : DifferentiableWithinAt 𝕜 c s x) (hx : c x ≠ 0)
     (hxs : UniqueDiffWithinAt 𝕜 s x) :
     derivWithin (fun x => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2 :=

Mathlib/Analysis/Calculus/DiffContOnCl.lean

@@ -3,8 +3,9 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Analysis.Calculus.Deriv.Inv
 import Mathlib.Analysis.NormedSpace.Real
+import Mathlib.Analysis.Calculus.FDeriv.Add
+import Mathlib.Analysis.Calculus.FDeriv.Mul
 
 /-!
 # Functions differentiable on a domain and continuous on its closure

Mathlib/Analysis/Calculus/Dslope.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Analysis.Calculus.Deriv.Slope
-import Mathlib.Analysis.Calculus.Deriv.Inv
+import Mathlib.Analysis.Calculus.Deriv.Comp
+import Mathlib.Analysis.Calculus.FDeriv.Add
+import Mathlib.Analysis.Calculus.FDeriv.Mul
 
 /-!
 # Slope of a differentiable function

Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

@@ -58,6 +58,12 @@ theorem HasFPowerSeriesAt.fderiv_eq (h : HasFPowerSeriesAt f p x) :
     fderiv 𝕜 f x = continuousMultilinearCurryFin1 𝕜 E F (p 1) :=
   h.hasFDerivAt.fderiv
 
+theorem AnalyticAt.hasStrictFDerivAt (h : AnalyticAt 𝕜 f x) :
+    HasStrictFDerivAt f (fderiv 𝕜 f x) x := by
+  rcases h with ⟨p, hp⟩
+  rw [hp.fderiv_eq]
+  exact hp.hasStrictFDerivAt
+
 theorem HasFPowerSeriesOnBall.differentiableOn [CompleteSpace F]
     (h : HasFPowerSeriesOnBall f p x r) : DifferentiableOn 𝕜 f (EMetric.ball x r) := fun _ hy =>
   (h.analyticAt_of_mem hy).differentiableWithinAt