change (fun x_1 ↦ nnabla (fun n ↦ 1 / d n) x_1) =O[atTop] _
n : ℕ
A a b c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
d : ℝ → ℝ := fun n => n * ((2 * π) ^ 2 + (n / x).log ^ 2)
⊢ (nnabla fun n => 1 / (n * ((2 * π) ^ 2 + (n / x).log ^ 2))) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
n : ℕ
A a b c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
d : ℝ → ℝ := fun n => n * ((2 * π) ^ 2 + (n / x).log ^ 2)
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)