radius_neg

Mathlib.Analysis.Analytic.ConvergenceRadius

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

English

If for all r the weighted norms are summable, then the radius is infinite.

Русский

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

LaTeX

$$$\\text{AllSummable}(\\|p_n\\| \\cdot r^n) \\Rightarrow p.radius = \\infty.$$$

Lean4

@[simp]
theorem radius_neg (p : FormalMultilinearSeries 𝕜 E F) : (-p).radius = p.radius := by
  simp only [radius, neg_apply, norm_neg]

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

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

Разделы

Аффилиация

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