English
In ENNReal terms, if the ratio tends to 0, the radius of convergence is infinite.
Русский
В терминах ENNReal, если отношение стремится к нулю, радиус схода бесконечен.
LaTeX
$$$\operatorname{radius}(\operatorname{ofScalars} E c) = \top$$$
Lean4
/-- 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)
simpa [hrz] using (summable_const_iff 0).mpr rfl
· refine Summable.of_norm_bounded_eventually (g := 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')
· simp_all
· 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)
