English
If the same ratio tends to a positive real r, then the radius of convergence is exactly 1/r.
Русский
Если предел отношения ‖c_{n+1}‖ / ‖c_n‖ существует и равен положительному числу r, то радиус сходления равен 1/r.
LaTeX
$$$\operatorname{radius}(\operatorname{ofScalars} E c) = \operatorname{ofNNReal} \left(r^{-1}\right)$$$
Lean4
/-- 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
