have l1 : nabla (fun n => n * (a + Real.log (n / b) ^ 2)) = fun n =>
    a + Real.log ((n + 1) / b) ^ 2 + (n * (Real.log ((n + 1) / b) ^ 2 - Real.log (n / b) ^ 2)) := by
  ext n ; simp [nabla] ; ring
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2