feat: improve the Analysis.Analytic.OfScalars API and implement it for geometric and exponential functions (#18407)

Following PR #17455, in which the ofScalars API was defined, this PR cleans up the file, fixes typos, adds additional infrastructure and implements the API in Analysis.Normed.Algebra.Exponential and Analysis.Analytic.Constructions.

Author: EdwardWatine

Mathlib/Analysis/Analytic/Constructions.lean

@@ -7,6 +7,7 @@ import Mathlib.Analysis.Analytic.Composition
 import Mathlib.Analysis.Analytic.Linear
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Mul
 import Mathlib.Analysis.Normed.Ring.Units
+import Mathlib.Analysis.Analytic.OfScalars
 
 /-!
 # Various ways to combine analytic functions
@@ -712,6 +713,12 @@ variable (𝕜 A : Type*) [NontriviallyNormedField 𝕜] [NormedRing A] [NormedA
 def formalMultilinearSeries_geometric : FormalMultilinearSeries 𝕜 A A :=
   fun n ↦ ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A
 
+/-- The geometric series as an `ofScalars` series. -/
+theorem formalMultilinearSeries_geometric_eq_ofScalars :
+    formalMultilinearSeries_geometric 𝕜 A = FormalMultilinearSeries.ofScalars A fun _ ↦ (1 : 𝕜) :=
+  by simp_rw [FormalMultilinearSeries.ext_iff, FormalMultilinearSeries.ofScalars,
+    formalMultilinearSeries_geometric, one_smul, implies_true]
+
 lemma formalMultilinearSeries_geometric_apply_norm_le (n : ℕ) :
     ‖formalMultilinearSeries_geometric 𝕜 A n‖ ≤ max 1 ‖(1 : A)‖ :=
   ContinuousMultilinearMap.norm_mkPiAlgebraFin_le
@@ -725,42 +732,15 @@ end Geometric
 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
+  convert formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
+    FormalMultilinearSeries.ofScalars_radius_ge_inv_of_tendsto A _ one_ne_zero (by simp) |>.le
+  simp
 
 lemma formalMultilinearSeries_geometric_radius (𝕜 : Type*) [NontriviallyNormedField 𝕜]
     (A : Type*) [NormedRing A] [NormOneClass A] [NormedAlgebra 𝕜 A] :
     (formalMultilinearSeries_geometric 𝕜 A).radius = 1 := by
-  apply le_antisymm
-  · refine le_of_forall_nnreal_lt (fun r hr ↦ ?_)
-    rw [← ENNReal.coe_one, ENNReal.coe_le_coe]
-    have := FormalMultilinearSeries.isLittleO_one_of_lt_radius _ hr
-    simp_rw [formalMultilinearSeries_geometric_apply_norm, one_mul] at this
-    contrapose! this
-    simp_rw [IsLittleO, IsBigOWith, not_forall, norm_one, mul_one,
-      not_eventually]
-    refine ⟨1, one_pos, ?_⟩
-    refine ((eventually_ne_atTop 0).mp (Eventually.of_forall ?_)).frequently
-    intro n hn
-    push_neg
-    rwa [norm_pow, one_lt_pow_iff_of_nonneg (norm_nonneg _) hn,
-      Real.norm_of_nonneg (NNReal.coe_nonneg _), ← NNReal.coe_one,
-      NNReal.coe_lt_coe]
-  · 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
-    simp_rw [formalMultilinearSeries_geometric_apply_norm, one_mul]
-    refine isBigO_of_le atTop (fun n ↦ ?_)
-    rw [norm_one, Real.norm_of_nonneg (pow_nonneg (coe_nonneg r) _)]
-    exact pow_le_one₀ (coe_nonneg r) hr.le
+  exact (formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
+    FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto A _ one_ne_zero (by simp))
 
 lemma hasFPowerSeriesOnBall_inverse_one_sub
     (𝕜 : Type*) [NontriviallyNormedField 𝕜]

Mathlib/Analysis/Analytic/OfScalars.lean

@@ -5,33 +5,100 @@ Authors: Edward Watine
 -/
 import Mathlib.Analysis.Analytic.Basic
 
-
 /-!
 # Scalar series
 
 This file contains API for analytic functions `∑ cᵢ • xⁱ` defined in terms of scalars
 `c₀, c₁, c₂, …`.
 ## Main definitions / results:
  * `FormalMultilinearSeries.ofScalars`: the formal power series `∑ cᵢ • xⁱ`.
- * `FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto`: the ratio test for an analytic function
-   defined in terms of a formal power series `∑ cᵢ • xⁱ`.
+ * `FormalMultilinearSeries.ofScalarsSum`: the sum of such a power series, if it exists, and zero
+   otherwise.
+ * `FormalMultilinearSeries.ofScalars_radius_eq_(zero/inv/top)_of_tendsto`:
+   the ratio test for an analytic function defined in terms of a formal power series `∑ cᵢ • xⁱ`.
+ * `FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto_ENNReal`:
+   the ratio test for an analytic function using `ENNReal` division for all values `ℝ≥0∞`.
 -/
 
 namespace FormalMultilinearSeries
 
 section Field
 
+open ContinuousMultilinearMap
+
 variable {𝕜 : Type*} (E : Type*) [Field 𝕜] [Ring E] [Algebra 𝕜 E] [TopologicalSpace E]
-  [TopologicalRing E] (c : ℕ → 𝕜)
+  [TopologicalRing E] {c : ℕ → 𝕜}
 
 /-- Formal power series of `∑ cᵢ • xⁱ` for some scalar field `𝕜` and ring algebra `E`-/
-def ofScalars : FormalMultilinearSeries 𝕜 E E :=
+def ofScalars (c : ℕ → 𝕜) : FormalMultilinearSeries 𝕜 E E :=
   fun n ↦ c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E
 
-variable {E}
+@[simp]
+theorem ofScalars_eq_zero [Nontrivial E] (n : ℕ) : ofScalars E c n = 0 ↔ c n = 0 := by
+  rw [ofScalars, smul_eq_zero (c := c n) (x := ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]
+  refine or_iff_left (ContinuousMultilinearMap.ext_iff.1.mt <| not_forall_of_exists_not ?_)
+  use fun _ ↦ 1
+  simp
 
-/-- The sum of the formal power series. Takes the value `0` outside the radius of convergence. -/
-noncomputable def ofScalarsSum (x : E) := (ofScalars E c).sum x
+@[simp]
+theorem ofScalars_eq_zero_of_scalar_zero {n : ℕ} (hc : c n = 0) : ofScalars E c n = 0 := by
+  rw [ofScalars, hc, zero_smul 𝕜 (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]
+
+@[simp]
+theorem ofScalars_series_eq_zero [Nontrivial E] : ofScalars E c = 0 ↔ c = 0 := by
+  simp [FormalMultilinearSeries.ext_iff, funext_iff]
+
+variable (𝕜) in
+@[simp]
+theorem ofScalars_series_eq_zero_of_scalar_zero : ofScalars E (0 : ℕ → 𝕜) = 0 := by
+  simp [FormalMultilinearSeries.ext_iff]
+
+@[simp]
+theorem ofScalars_series_of_subsingleton [Subsingleton E] : ofScalars E c = 0 := by
+  simp_rw [FormalMultilinearSeries.ext_iff, ofScalars, ContinuousMultilinearMap.ext_iff]
+  exact fun _ _ ↦ Subsingleton.allEq _ _
+
+variable (𝕜) in
+theorem ofScalars_series_injective [Nontrivial E] : Function.Injective (ofScalars E (𝕜 := 𝕜)) := by
+  intro _ _
+  refine Function.mtr fun h ↦ ?_
+  simp_rw [FormalMultilinearSeries.ext_iff, ofScalars, ContinuousMultilinearMap.ext_iff, smul_apply]
+  push_neg
+  obtain ⟨n, hn⟩ := Function.ne_iff.1 h
+  refine ⟨n, fun _ ↦ 1, ?_⟩
+  simp only [mkPiAlgebraFin_apply, List.ofFn_const, List.prod_replicate, one_pow, ne_eq]
+  exact (smul_left_injective 𝕜 one_ne_zero).ne hn
+
+variable (c)
+
+@[simp]
+theorem ofScalars_series_eq_iff [Nontrivial E] (c' : ℕ → 𝕜) :
+    ofScalars E c = ofScalars E c' ↔ c = c' :=
+  ⟨fun e => ofScalars_series_injective 𝕜 E e, _root_.congrArg _⟩
+
+theorem ofScalars_apply_zero (n : ℕ) :
+    (ofScalars E c n fun _ => 0) = Pi.single (f := fun _ => E) 0 (c 0 • 1) n := by
+  rw [ofScalars]
+  cases n <;> simp
+
+theorem ofScalars_add (c' : ℕ → 𝕜) : ofScalars E (c + c') = ofScalars E c + ofScalars E c' := by
+  unfold ofScalars
+  simp_rw [Pi.add_apply, Pi.add_def _ _]
+  exact funext fun n ↦ Module.add_smul (c n) (c' n) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)
+
+theorem ofScalars_smul (x : 𝕜) : ofScalars E (x • c) = x • ofScalars E c := by
+  unfold ofScalars
+  simp [Pi.smul_def x _, smul_smul]
+
+variable (𝕜) in
+/-- The submodule generated by scalar series on `FormalMultilinearSeries 𝕜 E E`. -/
+def ofScalarsSubmodule : Submodule 𝕜 (FormalMultilinearSeries 𝕜 E E) where
+  carrier := {ofScalars E f | f}
+  add_mem' := fun ⟨c, hc⟩ ⟨c', hc'⟩ ↦ ⟨c + c', hc' ▸ hc ▸ ofScalars_add E c c'⟩
+  zero_mem' := ⟨0, ofScalars_series_eq_zero_of_scalar_zero 𝕜 E⟩
+  smul_mem' := fun x _ ⟨c, hc⟩ ↦ ⟨x • c, hc ▸ ofScalars_smul E c x⟩
+
+variable {E}
 
 theorem ofScalars_apply_eq (x : E) (n : ℕ) :
     ofScalars E c n (fun _ ↦ x) = c n • x ^ n := by
@@ -42,35 +109,39 @@ theorem ofScalars_apply_eq' (x : E) :
     (fun n ↦ ofScalars E c n (fun _ ↦ x)) = fun n ↦ c n • x ^ n := by
   simp [ofScalars]
 
+/-- The sum of the formal power series. Takes the value `0` outside the radius of convergence. -/
+noncomputable def ofScalarsSum := (ofScalars E c).sum
+
 theorem ofScalars_sum_eq (x : E) : ofScalarsSum c x =
     ∑' n, c n • x ^ n := tsum_congr fun n => ofScalars_apply_eq c x n
 
 theorem ofScalarsSum_eq_tsum : ofScalarsSum c =
     fun (x : E) => ∑' n : ℕ, c n • x ^ n := funext (ofScalars_sum_eq c)
 
 @[simp]
-theorem ofScalars_op [T2Space E] (x : E) :
+theorem ofScalarsSum_zero : ofScalarsSum c (0 : E) = c 0 • 1 := by
+  simp [ofScalarsSum_eq_tsum, ← ofScalars_apply_eq, ofScalars_apply_zero]
+
+@[simp]
+theorem ofScalarsSum_of_subsingleton [Subsingleton E] {x : E} : ofScalarsSum c x = 0 := by
+  simp [Subsingleton.eq_zero x, Subsingleton.eq_zero (1 : E)]
+
+@[simp]
+theorem ofScalarsSum_op [T2Space E] (x : E) :
     ofScalarsSum c (MulOpposite.op x) = MulOpposite.op (ofScalarsSum c x) := by
   simp [ofScalars, ofScalars_sum_eq, ← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]
 
 @[simp]
-theorem ofScalars_unop [T2Space E] (x : Eᵐᵒᵖ) :
+theorem ofScalarsSum_unop [T2Space E] (x : Eᵐᵒᵖ) :
     ofScalarsSum c (MulOpposite.unop x) = MulOpposite.unop (ofScalarsSum c x) := by
   simp [ofScalars, ofScalars_sum_eq, ← MulOpposite.unop_pow, ← MulOpposite.unop_smul, tsum_unop]
 
-@[simp]
-theorem ofScalars_eq_zero [Nontrivial E] (n : ℕ) : ofScalars E c n = 0 ↔ c n = 0 := by
-  rw [ofScalars, smul_eq_zero (c := c n) (x := ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]
-  refine or_iff_left (ContinuousMultilinearMap.ext_iff.1.mt <| not_forall_of_exists_not ?_)
-  use fun _ ↦ 1
-  simp
-
 end Field
 
 section Normed
 
-open Filter
-open scoped Topology
+open Filter ENNReal
+open scoped Topology NNReal
 
 variable {𝕜 : Type*} (E : Type*) [NontriviallyNormedField 𝕜] [NormedRing E]
     [NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) (n : ℕ)
@@ -88,44 +159,142 @@ theorem ofScalars_norm_le (hn : n > 0) : ‖ofScalars E c n‖ ≤ ‖c n‖ :=
 theorem ofScalars_norm [NormOneClass E] : ‖ofScalars E c n‖ = ‖c n‖ := by
   simp [ofScalars_norm_eq_mul]
 
-/-- The radius of convergence of a scalar series is the inverse of the ratio of the norms of the
-coefficients. -/
-theorem ofScalars_radius_eq_inv_of_tendsto [NormOneClass E] {r : NNReal} (hr : r ≠ 0)
+private theorem tendsto_succ_norm_div_norm {r r' : ℝ≥0} (hr' : r' ≠ 0)
+    (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r)) :
+      Tendsto (fun n ↦ ‖‖c (n + 1)‖ * r' ^ (n + 1)‖ /
+        ‖‖c n‖ * r' ^ n‖) atTop (𝓝 ↑(r' * r)) := by
+  simp_rw [norm_mul, norm_norm, mul_div_mul_comm, ← norm_div, pow_succ,
+    mul_div_right_comm, div_self (pow_ne_zero _ (NNReal.coe_ne_zero.mpr hr')
+    ), one_mul, norm_div, NNReal.norm_eq]
+  exact mul_comm r' r ▸ hc.mul tendsto_const_nhds
+
+theorem ofScalars_radius_ge_inv_of_tendsto {r : ℝ≥0} (hr : r ≠ 0)
     (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r)) :
-      (ofScalars E c).radius = ENNReal.ofNNReal r⁻¹ := by
-  have hc' {r' : NNReal} (hr' : (r' : ℝ) ≠ 0) :
-    Tendsto (fun n ↦ ‖‖ofScalars E c (n + 1)‖ * r' ^ (n + 1)‖ /
-      ‖‖ofScalars E c n‖ * r' ^ n‖) atTop (𝓝 ↑(r' * r)) := by
-    simp_rw [norm_mul, norm_norm, ofScalars_norm, mul_div_mul_comm, ← norm_div, pow_succ,
-      mul_div_right_comm, div_self (pow_ne_zero _ hr'), one_mul, norm_div, NNReal.norm_eq]
-    exact mul_comm r' r ▸ Filter.Tendsto.mul hc tendsto_const_nhds
-  apply le_antisymm <;> refine ENNReal.le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
-  · rw [ENNReal.coe_le_coe, NNReal.le_inv_iff_mul_le hr]
-    have := FormalMultilinearSeries.summable_norm_mul_pow _ hr'
-    contrapose! this
-    have hrz : (r' : ℝ) ≠ 0 := by aesop
-    apply not_summable_of_ratio_test_tendsto_gt_one this
-    exact hc' (by aesop)
-  · rw [ENNReal.coe_lt_coe, NNReal.lt_inv_iff_mul_lt hr] at hr'
-    by_cases hrz : r' = 0
-    · simp [hrz]
-    · apply FormalMultilinearSeries.le_radius_of_summable_norm
-      refine summable_of_ratio_test_tendsto_lt_one hr' ?_ <| hc' (NNReal.coe_ne_zero.2 hrz)
-      refine (Tendsto.eventually_ne hc (NNReal.coe_ne_zero.2 hr)).mp (Eventually.of_forall ?_)
-      simp_rw [div_ne_zero_iff, ofScalars_norm, mul_ne_zero_iff]
+      (ofScalars E c).radius ≥ ofNNReal r⁻¹ := by
+  refine le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
+  rw [coe_lt_coe, NNReal.lt_inv_iff_mul_lt hr] at hr'
+  by_cases hrz : r' = 0
+  · simp [hrz]
+  apply FormalMultilinearSeries.le_radius_of_summable_norm
+  refine Summable.of_norm_bounded_eventually (fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_
+  · refine summable_of_ratio_test_tendsto_lt_one hr' ?_ ?_
+    · refine (hc.eventually_ne (NNReal.coe_ne_zero.mpr hr)).mp (Eventually.of_forall ?_)
       aesop
+    · simp_rw [norm_norm]
+      exact tendsto_succ_norm_div_norm c hrz hc
+  · filter_upwards [eventually_cofinite_ne 0] with n hn
+    simp only [norm_mul, norm_norm, norm_pow, NNReal.norm_eq]
+    gcongr
+    exact ofScalars_norm_le E c n (Nat.pos_iff_ne_zero.mpr hn)
+
+/-- The radius of convergence of a scalar series is the inverse of the non-zero limit
+`fun n ↦ ‖c n.succ‖ / ‖c n‖`. -/
+theorem ofScalars_radius_eq_inv_of_tendsto [NormOneClass E] {r : ℝ≥0} (hr : r ≠ 0)
+    (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r)) :
+      (ofScalars E c).radius = ofNNReal r⁻¹ := by
+  refine le_antisymm ?_ (ofScalars_radius_ge_inv_of_tendsto E c hr hc)
+  refine le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
+  rw [coe_le_coe, NNReal.le_inv_iff_mul_le hr]
+  have := FormalMultilinearSeries.summable_norm_mul_pow _ hr'
+  contrapose! this
+  apply not_summable_of_ratio_test_tendsto_gt_one this
+  simp_rw [ofScalars_norm]
+  exact tendsto_succ_norm_div_norm c (by aesop) hc
 
 /-- A convenience lemma restating the result of `ofScalars_radius_eq_inv_of_tendsto` under
 the inverse ratio. -/
 theorem ofScalars_radius_eq_of_tendsto [NormOneClass E] {r : NNReal} (hr : r ≠ 0)
     (hc : Tendsto (fun n ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 r)) :
-      (ofScalars E c).radius = ENNReal.ofNNReal r := by
+      (ofScalars E c).radius = ofNNReal r := by
   suffices Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r⁻¹) by
     convert ofScalars_radius_eq_inv_of_tendsto E c (inv_ne_zero hr) this
     simp
-  convert (continuousAt_inv₀ <| NNReal.coe_ne_zero.mpr hr).tendsto.comp hc
+  convert hc.inv₀ (NNReal.coe_ne_zero.mpr hr) using 1
   simp
 
+/-- The ratio test stating that if `‖c n.succ‖ / ‖c n‖` tends to zero, the radius is unbounded.
+This requires that the coefficients are eventually non-zero as
+`‖c n.succ‖ / 0 = 0` by convention. -/
+theorem ofScalars_radius_eq_top_of_tendsto (hc : ∀ᶠ n in atTop, c n ≠ 0)
+    (hc' : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)) : (ofScalars E c).radius = ⊤ := by
+  refine radius_eq_top_of_summable_norm _ fun r' ↦ ?_
+  by_cases hrz : r' = 0
+  · apply Summable.comp_nat_add (k := 1)
+    simp [hrz]
+    exact (summable_const_iff 0).mpr rfl
+  · refine Summable.of_norm_bounded_eventually (fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_
+    · apply summable_of_ratio_test_tendsto_lt_one zero_lt_one (hc.mp (Eventually.of_forall ?_))
+      · simp only [norm_norm]
+        exact mul_zero (_ : ℝ) ▸ tendsto_succ_norm_div_norm _ hrz (NNReal.coe_zero ▸ hc')
+      · aesop
+    · filter_upwards [eventually_cofinite_ne 0] with n hn
+      simp only [norm_mul, norm_norm, norm_pow, NNReal.norm_eq]
+      gcongr
+      exact ofScalars_norm_le E c n (Nat.pos_iff_ne_zero.mpr hn)
+
+/-- If `‖c n.succ‖ / ‖c n‖` is unbounded, then the radius of convergence is zero. -/
+theorem ofScalars_radius_eq_zero_of_tendsto [NormOneClass E]
+    (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop) : (ofScalars E c).radius = 0 := by
+  suffices (ofScalars E c).radius ≤ 0 by aesop
+  refine le_of_forall_nnreal_lt (fun r hr ↦ ?_)
+  rw [← coe_zero, coe_le_coe]
+  have := FormalMultilinearSeries.summable_norm_mul_pow _ hr
+  contrapose! this
+  apply not_summable_of_ratio_norm_eventually_ge one_lt_two
+  · contrapose! hc
+    apply not_tendsto_atTop_of_tendsto_nhds (a:=0)
+    rw [not_frequently] at hc
+    apply Tendsto.congr' ?_ tendsto_const_nhds
+    filter_upwards [hc] with n hc'
+    rw [ofScalars_norm, norm_mul, norm_norm, not_ne_iff, mul_eq_zero] at hc'
+    cases hc' <;> aesop
+  · filter_upwards [hc.eventually_ge_atTop (2*r⁻¹), eventually_ne_atTop 0] with n hc hn
+    simp only [ofScalars_norm, norm_mul, norm_norm, norm_pow, NNReal.norm_eq]
+    rw [mul_comm ‖c n‖, ← mul_assoc, ← div_le_div_iff, mul_div_assoc]
+    · convert hc
+      rw [pow_succ, div_mul_cancel_left₀, NNReal.coe_inv]
+      aesop
+    · aesop
+    · refine Ne.lt_of_le (fun hr' ↦ Not.elim ?_ hc) (norm_nonneg _)
+      rw [← hr']
+      simp [this]
+
+/-- This theorem combines the results of the special cases above, using `ENNReal` division to remove
+the requirement that the ratio is eventually non-zero. -/
+theorem ofScalars_radius_eq_inv_of_tendsto_ENNReal [NormOneClass E] {r : ℝ≥0∞}
+    (hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)) :
+      (ofScalars E c).radius = r⁻¹ := by
+  rcases ENNReal.trichotomy r with (hr | hr | hr)
+  · simp_rw [hr, inv_zero] at hc' ⊢
+    by_cases h : (∀ᶠ (n : ℕ) in atTop, c n ≠ 0)
+    · apply ofScalars_radius_eq_top_of_tendsto E c h ?_
+      refine Tendsto.congr' ?_ <| (tendsto_toReal zero_ne_top).comp hc'
+      filter_upwards [h]
+      simp
+    · apply (ofScalars E c).radius_eq_top_of_eventually_eq_zero
+      simp only [eventually_atTop, not_exists, not_forall, Classical.not_imp, not_not] at h ⊢
+      obtain ⟨ti, hti⟩ := eventually_atTop.mp (hc'.eventually_ne zero_ne_top)
+      obtain ⟨zi, hzi, z⟩ := h ti
+      refine ⟨zi, Nat.le_induction (ofScalars_eq_zero_of_scalar_zero E z) fun n hmn a ↦ ?_⟩
+      nontriviality E
+      simp only [ofScalars_eq_zero] at a ⊢
+      contrapose! hti
+      exact ⟨n, hzi.trans hmn, ENNReal.div_eq_top.mpr (by simp [a, hti])⟩
+  · simp_rw [hr, inv_top] at hc' ⊢
+    apply ofScalars_radius_eq_zero_of_tendsto E c ((tendsto_add_atTop_iff_nat 1).mp ?_)
+    refine tendsto_ofReal_nhds_top.mp (Tendsto.congr' ?_ ((tendsto_add_atTop_iff_nat 1).mpr hc'))
+    filter_upwards [hc'.eventually_ne top_ne_zero] with n hn
+    apply (ofReal_div_of_pos (Ne.lt_of_le (Ne.symm ?_) (norm_nonneg _))).symm
+    aesop
+  · have hr' := toReal_ne_zero.mp hr.ne.symm
+    have hr'' := toNNReal_ne_zero.mpr hr' -- this result could go in ENNReal
+    convert ofScalars_radius_eq_inv_of_tendsto E c hr'' ?_
+    · simp [ENNReal.coe_inv hr'', ENNReal.coe_toNNReal (toReal_ne_zero.mp hr.ne.symm).2]
+    · simp_rw [ENNReal.coe_toNNReal_eq_toReal]
+      refine Tendsto.congr' ?_ <| (tendsto_toReal hr'.2).comp hc'
+      filter_upwards [hc'.eventually_ne hr'.1, hc'.eventually_ne hr'.2]
+      simp
+
 end Normed
 
 end FormalMultilinearSeries