Theorem: BrunTitchmarsh.err_isBigO (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x ^ (1 / 2) * (1 + 1 / 2 * x.log) ^ 3) =O[atTop] fun x => x / x.log
Tactic:
calc
  _ =O[atTop] (fun x ↦ x ^ (1/2:ℝ) * (Real.log x) ^ 3) := by
    apply IsBigO.mul (isBigO_refl ..)
    apply Real.isLittleO_const_log_atTop.isBigO.add ((isBigO_refl ..).const_mul_left ..) |>.pow
  _ =O[atTop] _ := by
    convert rpow_mul_rpow_log_isBigO_id_div_log 3 (?_) <;> norm_num
    rw [← Real.rpow_natCast]
    norm_cast
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x ^ (1 / 2) * (1 + 1 / 2 * x.log) ^ 3) =O[atTop] fun x => x ^ (1 / 2) * x.log ^ 3
Tactic:
apply IsBigO.mul (isBigO_refl ..)
State after:
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

State before:
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
Tactic:
apply Real.isLittleO_const_log_atTop.isBigO.add ((isBigO_refl ..).const_mul_left ..) |>.pow
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x ^ (1 / 2) * x.log ^ 3) =O[atTop] fun x => x / x.log
Tactic:
convert rpow_mul_rpow_log_isBigO_id_div_log 3 (?_) <;> norm_num
State after:
case h.e'_7.h.h.e'_6
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
x✝ : ℝ
⊢ x✝.log ^ 3 = x✝.log ^ 3

State before:
case h.e'_7.h.h.e'_6
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
x✝ : ℝ
⊢ x✝.log ^ 3 = x✝.log ^ 3
Tactic:
rw [← Real.rpow_natCast]
State after:
case h.e'_7.h.h.e'_6
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
x✝ : ℝ
⊢ x✝.log ^ ↑3 = x✝.log ^ 3

State before:
case h.e'_7.h.h.e'_6
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
x✝ : ℝ
⊢ x✝.log ^ ↑3 = x✝.log ^ 3
Tactic:
norm_cast
State after:
no goals