case pos
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n

case neg
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : ¬r₁ = 0
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
by_cases h0 : r₁ = 0
case neg
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
case neg
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : ¬r₁ = 0
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
rw [← Ne.def, ← norm_pos_iff] at h0
case neg
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
case neg
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
have A : (fun n ↦ (n : R) ^ k : ℕ → R) =o[atTop] fun n ↦ (r₂ / ‖r₁‖) ^ n :=
  isLittleO_pow_const_const_pow_of_one_lt k ((one_lt_div h0).2 h)
case neg
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
⊢ (fun n => r₁ ^ n) =O[atTop] fun n => ‖r₁‖ ^ n
case neg
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
suffices (fun n ↦ r₁ ^ n) =O[atTop] fun n ↦ ‖r₁‖ ^ n by
  simpa [div_mul_cancel _ (pow_pos h0 _).ne'] using A.mul_isBigO this
no goals
case neg
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
⊢ (fun n => r₁ ^ n) =O[atTop] fun n => ‖r₁‖ ^ n
exact IsBigO.of_bound 1 (by simpa using eventually_norm_pow_le r₁)
case pos
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
n : ℕ
hn : n ≥ 1
⊢ n ∈ {x | (fun x => (fun _x => 0) x = (fun n => ↑n ^ k * r₁ ^ n) x) x}
case pos
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
refine' (isLittleO_zero _ _).congr' (mem_atTop_sets.2 <| ⟨1, fun n hn ↦ _⟩) EventuallyEq.rfl
no goals
case pos
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
n : ℕ
hn : n ≥ 1
⊢ n ∈ {x | (fun x => (fun _x => 0) x = (fun n => ↑n ^ k * r₁ ^ n) x) x}
simp [zero_pow (zero_lt_one.trans_le hn), h0]
no goals
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
this : (fun n => r₁ ^ n) =O[atTop] fun n => ‖r₁‖ ^ n
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
simpa [div_mul_cancel _ (pow_pos h0 _).ne'] using A.mul_isBigO this
no goals
α : Type ?u.98739
β : Type ?u.98742
ι : Type ?u.98745
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
⊢ ∀ᶠ (x : ℕ) in atTop, ‖r₁ ^ x‖ ≤ 1 * ‖‖r₁‖ ^ x‖
simpa using eventually_norm_pow_le r₁