isLittleO_one_of_lt_radius — Mathlib

English

If r is strictly smaller than the radius of p, then the sequence of coefficients satisfies ‖p_n‖ r^n = o(1); in particular it tends to 0 when scaled by r^n.

Русский

Если r меньше радиуса p, то ‖p_n‖ r^n = o(1); следовательно, ‖p_n‖ r^n → 0.

LaTeX

$$$\\text{If } r>0 \\text{ and } r < p.radius,\\quad \\bigl( n \\mapsto \\|p\\,n\\| \\; r^n \\bigr) = o_{n\\to\\infty}(1).$$$

Lean4

/-- For `r` strictly smaller than the radius of `p`, then `‖pₙ‖ rⁿ = o(1)`. -/
theorem isLittleO_one_of_lt_radius (h : ↑r < p.radius) :
    (fun n => ‖p n‖ * (r : ℝ) ^ n) =o[atTop] (fun _ => 1 : ℕ → ℝ) :=
  let ⟨_, ha, hp⟩ := p.isLittleO_of_lt_radius h
  hp.trans <| (isLittleO_pow_pow_of_lt_left ha.1.le ha.2).congr (fun _ => rfl) one_pow

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