α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
have : Tendsto (fun x : ℝ ↦ x ^ k) (𝓝[>] 1) (𝓝 1) :=
  ((continuous_id.pow k).tendsto' (1 : ℝ) 1 (one_pow _)).mono_left inf_le_left
case intro.intro
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
obtain ⟨r' : ℝ, hr' : r' ^ k < r, h1 : 1 < r'⟩ :=
  ((this.eventually (gt_mem_nhds hr)).and self_mem_nhdsWithin).exists
case intro.intro
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
case intro.intro
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
have h0 : 0 ≤ r' := zero_le_one.trans h1.le
case intro.intro
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this✝ : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
this : (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ k) ^ n
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n

case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ k) ^ n
case intro.intro
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
suffices : (fun n ↦ (n : R) ^ k : ℕ → R) =O[atTop] fun n : ℕ ↦ (r' ^ k) ^ n
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ k) ^ n
case intro.intro
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this✝ : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
this : (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ k) ^ n
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n

case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ k) ^ n
exact this.trans_isLittleO (isLittleO_pow_pow_of_lt_left (pow_nonneg h0 _) hr')
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ n) ^ k
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ k) ^ n
conv in (r' ^ _) ^ _ => rw [← pow_mul, mul_comm, pow_mul]
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this✝ : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
this : ∀ (n : ℕ), ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
⊢ (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ n) ^ k

case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ ∀ (n : ℕ), ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ n) ^ k
suffices : ∀ n : ℕ, ‖(n : R)‖ ≤ (r' - 1)⁻¹ * ‖(1 : R)‖ * ‖r' ^ n‖
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ ∀ (n : ℕ), ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this✝ : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
this : ∀ (n : ℕ), ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
⊢ (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ n) ^ k

case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ ∀ (n : ℕ), ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
exact (isBigO_of_le' _ this).pow _
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ ∀ (n : ℕ), ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
intro n
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖r' ^ n‖ * ‖1‖
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
rw [mul_right_comm]
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ ↑n ≤ (r' - 1)⁻¹ * ‖r' ^ n‖
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖r' ^ n‖ * ‖1‖
refine' n.norm_cast_le.trans (mul_le_mul_of_nonneg_right _ (norm_nonneg _))
no goals
case this
α : Type ?u.86654
β : Type ?u.86657
ι : Type ?u.86660
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ ↑n ≤ (r' - 1)⁻¹ * ‖r' ^ n‖
simpa [_root_.div_eq_inv_mul, Real.norm_eq_abs, abs_of_nonneg h0] using n.cast_le_pow_div_sub h1