English
There exist a∈(0,1) and C>0 such that for all n, ‖p_n‖ r^n ≤ C a^n when r is below the radius.
Русский
Существуют a∈(0,1) и C>0 такие, что для всех n выполняется ‖p_n‖ r^n ≤ C a^n, если r ниже радиуса.
LaTeX
$$$\\exists a\\in(0,1),\\exists C>0:\\forall n,\\|p_n\\| r^n \\le C a^n.$$$
Lean4
/-- If `r ≠ 0` and `‖pₙ‖ rⁿ = O(aⁿ)` for some `-1 < a < 1`, then `r < p.radius`. -/
theorem lt_radius_of_isBigO (h₀ : r ≠ 0) {a : ℝ} (ha : a ∈ Ioo (-1 : ℝ) 1)
(hp : (fun n => ‖p n‖ * (r : ℝ) ^ n) =O[atTop] (a ^ ·)) : ↑r < p.radius :=
by
have := ((TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 2 5)
rcases this.mp ⟨a, ha, hp⟩ with ⟨a, ha, C, hC, hp⟩
rw [← pos_iff_ne_zero, ← NNReal.coe_pos] at h₀
lift a to ℝ≥0 using ha.1.le
have : (r : ℝ) < r / a := by simpa only [div_one] using (div_lt_div_iff_of_pos_left h₀ zero_lt_one ha.1).2 ha.2
norm_cast at this
rw [← ENNReal.coe_lt_coe] at this
refine this.trans_le (p.le_radius_of_bound C fun n => ?_)
rw [NNReal.coe_div, div_pow, ← mul_div_assoc, div_le_iff₀ (pow_pos ha.1 n)]
exact (le_abs_self _).trans (hp n)
