le_radius_of_eventually_le

Mathlib.Analysis.Analytic.ConvergenceRadius

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

← MathLib Explorer

English

If ∀ r ≥ 0 the isBigO holds, then radius equals top.

Русский

Если для любого r ≥ 0 выполняется isBigO, тогда radius(p) = ∞.

LaTeX

$$le_radius_of_isBigO (p) (h) : ↑r ≤ p.radius$$

Lean4

theorem le_radius_of_eventually_le (C) (h : ∀ᶠ n in atTop, ‖p n‖ * (r : ℝ) ^ n ≤ C) : ↑r ≤ p.radius :=
  p.le_radius_of_isBigO <| IsBigO.of_bound C <| h.mono fun n hn => by simpa

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

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

Разделы

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

Аффилиация

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