𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < radius p
this :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
⊢ ∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < radius p
⊢ ∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x
have := (TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 1 4
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < radius p
this :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
⊢ ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < radius p
this :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
⊢ ∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x
rw [this]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
h : ∃ i i_1 i_2, ↑r < ↑i
⊢ ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < radius p
this :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
⊢ ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
simp only [radius, lt_iSup_iff] at h
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r < ↑t
⊢ ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
h : ∃ i i_1 i_2, ↑r < ↑i
⊢ ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
rcases h with ⟨t, C, hC, rt⟩
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r < ↑t
⊢ ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r < ↑t
⊢ ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at rt
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r < ↑t
this : 0 < ↑t
⊢ ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r < ↑t
⊢ ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
have : 0 < (t : ℝ) := r.coe_nonneg.trans_lt rt
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r / ↑t < 1
this : 0 < ↑t
⊢ ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r < ↑t
this : 0 < ↑t
⊢ ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
rw [← div_lt_one this] at rt
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r / ↑t < 1
this : 0 < ↑t
n : ℕ
⊢ abs (‖p n‖ * ↑r ^ n) ≤ C * (↑r / ↑t) ^ n
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r / ↑t < 1
this : 0 < ↑t
⊢ ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
refine' ⟨_, rt, C, Or.inr zero_lt_one, fun n => _⟩
no goals
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r / ↑t < 1
this : 0 < ↑t
n : ℕ
⊢ abs (‖p n‖ * ↑r ^ n) ≤ C * (↑r / ↑t) ^ n
calc
  |‖p n‖ * (r : ℝ) ^ n| = ‖p n‖ * (t : ℝ) ^ n * (r / t : ℝ) ^ n := by
    field_simp [mul_right_comm, abs_mul, this.ne']
  _ ≤ C * (r / t : ℝ) ^ n := by gcongr; apply hC
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r / ↑t < 1
this : 0 < ↑t
n : ℕ
⊢ abs (‖p n‖ * ↑r ^ n) = ‖p n‖ * ↑t ^ n * (↑r / ↑t) ^ n
field_simp [mul_right_comm, abs_mul, this.ne']
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r / ↑t < 1
this : 0 < ↑t
n : ℕ
⊢ ‖p n‖ * ↑t ^ n ≤ C
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r / ↑t < 1
this : 0 < ↑t
n : ℕ
⊢ ‖p n‖ * ↑t ^ n * (↑r / ↑t) ^ n ≤ C * (↑r / ↑t) ^ n
gcongr
no goals
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.114222
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a, a ∈ Ioo 0 1 ∧ (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a, a < 1 ∧ ∃ C x, ∀ (n : ℕ), abs (‖p n‖ * ↑r ^ n) ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r / ↑t < 1
this : 0 < ↑t
n : ℕ
⊢ ‖p n‖ * ↑t ^ n ≤ C
apply hC