log_mul_add_isBigO_log

lemma log_mul_add_isBigO_log {a : ℝ} (ha : 0 < a) (b : ℝ) :    (fun x => Real.log (a * x + b)) =O[atTop] Real.log := by  apply IsBigO.of_bound (2 : ℕ)  have l2 : ∀ᶠ x : ℝ in atTop, 0 ≤ log x := tendsto_atTop.mp tendsto_log_atTop 0  have l3 : ∀ᶠ x : ℝ in atTop, 0 ≤ log (a * x + b) :=    tendsto_atTop.mp (tendsto_log_atTop.comp (tendsto_mul_add_atTop ha b)) 0  have l5 : ∀ᶠ x : ℝ in atTop, 1 ≤ a * x + b := tendsto_atTop.mp (tendsto_mul_add_atTop ha b) 1  have l1 : ∀ᶠ x : ℝ in atTop, a * x + b ≤ x ^ 2 := by    filter_upwards [(isLittleO_mul_add_sq a b).eventuallyLE, l5] with x r2 l5    simpa [abs_eq_self.mpr (zero_le_one.trans l5)] using r2  filter_upwards [l1, l2, l3, l5] with x l1 l2 l3 l5  simpa [abs_eq_self.mpr l2, abs_eq_self.mpr l3, Real.log_pow] using    Real.log_le_log (by linarith) l1