have l4 : (fun x => Real.log ((x + 1) / b) + Real.log (x / b)) =O[atTop] Real.log := by
  simpa using (log_add_div_isBigO_log _ hb).add (log_add_div_isBigO_log 0 hb)
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)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
⊢ (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)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
l4 : (fun x => ((x + 1) / b).log + (x / b).log) =O[atTop] Real.log
⊢ (nabla fun x => x * (a + (x / b).log ^ 2)) =O[atTop] fun x => x.log ^ 2