apply IsBigO.const_mul_left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ ((C * (2 * π) ^ 2) • nnabla fun n => n⁻¹ * ((2 * π) ^ 2 + (n * x⁻¹).log ^ 2)⁻¹) =O[atTop] fun n =>
    (n.log ^ 2)⁻¹ * (n ^ 2)⁻¹
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (fun x_1 => nnabla (fun n => n⁻¹ * ((2 * π) ^ 2 + (n * x⁻¹).log ^ 2)⁻¹) x_1) =O[atTop] fun n =>
    (n.log ^ 2)⁻¹ * (n ^ 2)⁻¹