radius_eq_top_of_forall_nnreal_isBigO

English

If for every NNReal r, the IsBigO condition holds, then radius equals top (∞).

Русский

Если для каждого NNReal r выполняется IsBigO, radius(p) = ∞.

LaTeX

$$radius_eq_top_of_forall_nnreal_isBigO (p) (h)$$

Lean4

theorem radius_eq_top_of_forall_nnreal_isBigO
    (h : ∀ r : ℝ≥0, (fun n => ‖p n‖ * (r : ℝ) ^ n) =O[atTop] fun _ => (1 : ℝ)) : p.radius = ∞ :=
  ENNReal.eq_top_of_forall_nnreal_le fun r => p.le_radius_of_isBigO (h r)

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