ofScalars_radius_eq_of_tendsto — Mathlib

English

If the ratio tends to 0 after taking the inverse relation, the radius becomes infinite.

Русский

Если отношение ‖c_{n+1}‖ / ‖c_n‖ стремится к нулю, то радиус сходления бесконечен.

LaTeX

$$$(\operatorname{ofScalars} E c).radius = \top$$$

Lean4

/-- 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 = 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 hc.inv₀ (NNReal.coe_ne_zero.mpr hr) using 1
  simp

Похожие утверждения