norm_mul_pow_le_mul_pow_of_lt_radius

English

If there exists a real a with -1<a<1 such that ‖p_n‖ r^n = O(a^n), then r < p.radius.

Русский

Если найдётся a ∈ (-1,1) так, что ‖p_n‖ r^n = O(a^n), то r < p.radius.

LaTeX

$$$\\exists a\\in(-1,1):\\; (\\|p_n\\| r^n) =O_{n\\to\\infty}(a^n) \\Rightarrow r < p.radius.$$$

Lean4

/-- For `r` strictly smaller than the radius of `p`, then `‖pₙ‖ rⁿ` tends to zero exponentially:
for some `0 < a < 1` and `C > 0`, `‖p n‖ * r ^ n ≤ C * a ^ n`. -/
theorem norm_mul_pow_le_mul_pow_of_lt_radius (h : ↑r < p.radius) :
    ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ n, ‖p n‖ * (r : ℝ) ^ n ≤ C * a ^ n :=
  by
  have := ((TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 1 5).mp (p.isLittleO_of_lt_radius h)
  rcases this with ⟨a, ha, C, hC, H⟩
  exact ⟨a, ha, C, hC, fun n => (le_abs_self _).trans (H n)⟩

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