apply Real.isLittleO_const_log_atTop.isBigO.add ((isBigO_refl ..).const_mul_left ..) |>.pow
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => (1 + 1 / 2 * x.log) ^ 3) =O[atTop] fun x => x.log ^ 3
no goals