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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => N ^ (1 / 2) * (1 + N.log / Real.log 2)) =O[atTop] fun N => N ^ (1 / 2) * N.log
Tactic:
apply IsBigO.mul
State after:
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x ^ (1 / 2)) =O[atTop] fun x => x ^ (1 / 2)

case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => 1 + x.log / Real.log 2) =O[atTop] fun x => x.log

State before:
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => 1 + x.log / Real.log 2) =O[atTop] fun x => x.log
Tactic:
apply one_add_log_div_log_two_isBigO
State after:
no goals

State before:
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => x ^ (1 / 2)) =O[atTop] fun x => x ^ (1 / 2)
Tactic:
apply isBigO_refl
State after:
no goals

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

State before:
case h.e'_7
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N => N ^ (1 / 2) * N.log) = fun x => x ^ (1 / 2) * x.log ^ 1
Tactic:
simp
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 1 / 2 < 1
Tactic:
norm_num
State after:
no goals