le_radius_of_bound — Mathlib

English

If ∑ ‖p_n‖ r^n is summable in NNReal, then the radius is at least r.

Русский

Если сумма ‖p_n‖ r^n по NNReal сходится, тогда радиус не меньше r.

LaTeX

$$le_radius_of_summable_nnreal (p) (C) (h) : (r : ℝ≥0∞) ≤ radius(p)$$

Lean4

/-- If `‖pₙ‖ rⁿ` is bounded in `n`, then the radius of `p` is at least `r`. -/
theorem le_radius_of_bound (C : ℝ) {r : ℝ≥0} (h : ∀ n : ℕ, ‖p n‖ * (r : ℝ) ^ n ≤ C) : (r : ℝ≥0∞) ≤ p.radius :=
  le_iSup_of_le r <| le_iSup_of_le C <| le_iSup (fun _ => (r : ℝ≥0∞)) h

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