English
If r is strictly less than the radius of p, then the sequence n ↦ ‖p_n‖ r^n is bounded by a geometric rate; in fact it can be dominated by C a^n with some a in (0,1) and C>0.
Русский
Если r меньше радиуса p, то последовательность n ↦ ‖p_n‖ r^n растет не быстрее геометрической прогрессии; существует a в (0,1) и C>0 с ∀n, ‖p_n‖ r^n ≤ C a^n.
LaTeX
$$$\text{If } \uparrow r < p.radius,\ \exists a\in(0,1),\exists C>0,\forall n:\; \|p_n\|\, r^n \le C a^n$$$
Lean4
/-- For `r` strictly smaller than the radius of `p`, then `‖pₙ‖ rⁿ` tends to zero exponentially:
for some `0 < a < 1`, `‖p n‖ rⁿ = o(aⁿ)`. -/
theorem isLittleO_of_lt_radius (h : ↑r < p.radius) :
∃ a ∈ Ioo (0 : ℝ) 1, (fun n => ‖p n‖ * (r : ℝ) ^ n) =o[atTop] (a ^ ·) :=
by
have := (TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 1 4
rw [this]
-- Porting note: was
-- rw [(TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 1 4]
simp only [radius, lt_iSup_iff] at h
rcases h with ⟨t, C, hC, rt⟩
rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at rt
have : 0 < (t : ℝ) := r.coe_nonneg.trans_lt rt
rw [← div_lt_one this] at rt
refine ⟨_, rt, C, Or.inr zero_lt_one, fun n => ?_⟩
calc
|‖p n‖ * (r : ℝ) ^ n| = ‖p n‖ * (t : ℝ) ^ n * (r / t : ℝ) ^ n := by simp [field, abs_mul, div_pow]
_ ≤ C * (r / t : ℝ) ^ n := by gcongr; apply hC
