α : Type ?u.72372
β : Type ?u.72375
ι : Type ?u.72378
r₁ r₂ : ℝ
h : abs r₁ < abs r₂
⊢ (fun x => ‖r₁ ^ x‖) =o[atTop] fun x => ‖r₂ ^ x‖
α : Type ?u.72372
β : Type ?u.72375
ι : Type ?u.72378
r₁ r₂ : ℝ
h : abs r₁ < abs r₂
⊢ (fun n => r₁ ^ n) =o[atTop] fun n => r₂ ^ n
refine' (IsLittleO.of_norm_left _).of_norm_right
no goals
α : Type ?u.72372
β : Type ?u.72375
ι : Type ?u.72378
r₁ r₂ : ℝ
h : abs r₁ < abs r₂
⊢ (fun x => ‖r₁ ^ x‖) =o[atTop] fun x => ‖r₂ ^ x‖
exact (isLittleO_pow_pow_of_lt_left (abs_nonneg r₁) h).congr (pow_abs r₁) (pow_abs r₂)