ofScalars_radius_eq_zero_of_tendsto

English

If the ratio grows without bound (tends to infinity), the radius of convergence is zero.

Русский

Если отношение растет без границы (вероятно стремится к бесконечности), радиус схода равен нулю.

LaTeX

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

Lean4

/-- 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 simp_all
  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
    · simp_all
    · refine Ne.lt_of_le (fun hr' ↦ Not.elim ?_ hc) (norm_nonneg _)
      rw [← hr']
      simp [this]

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