le_radius_of_bound_nnreal — Mathlib

English

If ‖p_n‖ ≤ C r^n for all n with C a NNReal, then radius(p) ≥ r.

Русский

Если ‖p_n‖ ≤ C r^n для всех n, где C ∈ NNReal, тогда radius(p) ≥ r.

LaTeX

$$le_radius_of_bound_nnreal (p) (C) {r} (h) : (r : ENNReal) ≤ p.radius$$

Lean4

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

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