English
Let c: N → 𝕜 be a sequence of scalars and assume the ratio ‖c_{n+1}‖ / ‖c_n‖ converges to a nonzero r > 0. Then the radius of convergence of the scalar multilinear series associated to c is at least 1/r.
Русский
Пусть c: ℕ → 𝕜 — последовательность скаляров, и предположим, что отношение ‖c_{n+1}‖ / ‖c_n‖ стремится к не нулю r > 0. Тогда радиус сходования скалярной формальной многочленной серии, соответствующей c, не меньше 1/r.
LaTeX
$$$\operatorname{radius}(\operatorname{ofScalars} E c) \ge \operatorname{ofNNReal} \left(r^{-1}\right)$$$
Lean4
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 ≥ 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 (g := 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 ?_)
simp_all
· 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)
