le_radius_of_summable_nnnorm

Mathlib.Analysis.Analytic.ConvergenceRadius

URI: https://scilib.ai/kg/mathlib#FormalMultilinearSeries.le_radius_of_summable_nnnorm

← MathLib Explorer

English

If ∑ ‖p_n‖₊ r^n converges, then radius ≥ r.

Русский

Если ∑ ‖p_n‖₊ r^n сходится, то радиус ≥ r.

LaTeX

$$le_radius_of_summable_nnnorm (p) (r) (h) : (r : ENNReal) ≤ radius(p)$$

Lean4

theorem le_radius_of_summable_nnnorm (h : Summable fun n => ‖p n‖₊ * r ^ n) : ↑r ≤ p.radius :=
  p.le_radius_of_bound_nnreal (∑' n, ‖p n‖₊ * r ^ n) fun _ => h.le_tsum' _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru