Commit 2024-09-24 06:06 4b28fd7c

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.