nnabla_mul_log_sq

lemma nnabla_mul_log_sq (a : ℝ) {b : ℝ} (hb : 0 < b) :    nabla (fun x => x * (a + Real.log (x / b) ^ 2)) =O[atTop] (fun x => Real.log x ^ 2) := by   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  have l2 := (isLittleO_const_of_tendsto_atTop a    ((tendsto_pow_atTop two_ne_zero).comp tendsto_log_atTop)).isBigO  have l3 := (log_add_div_isBigO_log 1 hb).sq  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)  have e2 : (fun x : ℝ => x * (Real.log x * (1 / x))) =ᶠ[atTop] Real.log := by    filter_upwards [eventually_ge_atTop 1] with x hx using by field_simp  have l5 : (fun n ↦ n * (Real.log n * (1 / n))) =O[atTop] (fun n ↦ (Real.log n) ^ 2) :=    e2.trans_isBigO      (by simpa using! (isLittleO_mul_add_sq 1 0).isBigO.comp_tendsto Real.tendsto_log_atTop)   simp_rw [l1, _root_.sq_sub_sq]  exact ((l2.add l3).add (isBigO_refl (·) atTop |>.mul (l4.mul (nabla_log hb)) |>.trans l5))