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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x ^ r * x.log ^ k) =O[atTop] fun x => x ^ r * x ^ ((1 - r) / 2)
Tactic:
apply IsBigO.mul (isBigO_refl ..)
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x.log ^ k) =O[atTop] fun x => x ^ ((1 - r) / 2)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x.log ^ k) =O[atTop] fun x => x ^ ((1 - r) / 2)
Tactic:
apply (isLittleO_log_rpow_rpow_atTop k (by linarith) ..).isBigO
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ 0 < (1 - r) / 2
Tactic:
linarith
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x ^ r * x ^ ((1 - r) / 2)) =ᶠ[atTop] fun N => N * (N ^ ((1 - r) / 2))⁻¹
Tactic:
filter_upwards [Filter.eventually_gt_atTop 0]
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ (a : ℝ), 0 < a → a ^ r * a ^ ((1 - r) / 2) = a * (a ^ ((1 - r) / 2))⁻¹

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ (a : ℝ), 0 < a → a ^ r * a ^ ((1 - r) / 2) = a * (a ^ ((1 - r) / 2))⁻¹
Tactic:
intro N hN
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ r * N ^ ((1 - r) / 2) = N * (N ^ ((1 - r) / 2))⁻¹

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ r * N ^ ((1 - r) / 2) = N * (N ^ ((1 - r) / 2))⁻¹
Tactic:
trans (N ^ (1 : ℝ) * (N ^ ((1-r)/2 : ℝ))⁻¹)
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ r * N ^ ((1 - r) / 2) = N ^ 1 * (N ^ ((1 - r) / 2))⁻¹

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ 1 * (N ^ ((1 - r) / 2))⁻¹ = N * (N ^ ((1 - r) / 2))⁻¹

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ r * N ^ ((1 - r) / 2) = N ^ 1 * (N ^ ((1 - r) / 2))⁻¹
Tactic:
rw [← Real.rpow_add hN, ← Real.rpow_neg hN.le, ← Real.rpow_add hN]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ (r + (1 - r) / 2) = N ^ (1 + -((1 - r) / 2))

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ (r + (1 - r) / 2) = N ^ (1 + -((1 - r) / 2))
Tactic:
ring_nf
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ 1 * (N ^ ((1 - r) / 2))⁻¹ = N * (N ^ ((1 - r) / 2))⁻¹
Tactic:
rw [← Nat.cast_one, Real.rpow_natCast, pow_one]
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun N => N * (N ^ ((1 - r) / 2))⁻¹) =O[atTop] fun N => N * N.log⁻¹
Tactic:
apply IsBigO.mul (isBigO_refl ..)
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => (x ^ ((1 - r) / 2))⁻¹) =O[atTop] fun x => x.log⁻¹

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => (x ^ ((1 - r) / 2))⁻¹) =O[atTop] fun x => x.log⁻¹
Tactic:
apply IsBigO.inv_rev
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x.log) =O[atTop] fun x => x ^ ((1 - r) / 2)

case h₀
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ᶠ (x : ℝ) in atTop, x.log = 0 → x ^ ((1 - r) / 2) = 0

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x.log) =O[atTop] fun x => x ^ ((1 - r) / 2)

case h₀
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ᶠ (x : ℝ) in atTop, x.log = 0 → x ^ ((1 - r) / 2) = 0
Tactic:
apply (isLittleO_log_rpow_atTop (by linarith) ..).isBigO
State after:
case h₀
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ᶠ (x : ℝ) in atTop, x.log = 0 → x ^ ((1 - r) / 2) = 0

State before:
case h₀
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ᶠ (x : ℝ) in atTop, x.log = 0 → x ^ ((1 - r) / 2) = 0
Tactic:
filter_upwards [Filter.eventually_gt_atTop 1]
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ (a : ℝ), 1 < a → a.log = 0 → a ^ ((1 - r) / 2) = 0

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ (a : ℝ), 1 < a → a.log = 0 → a ^ ((1 - r) / 2) = 0
Tactic:
intro N hN hcontra
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 1 < N
hcontra : N.log = 0
⊢ N ^ ((1 - r) / 2) = 0

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 1 < N
hcontra : N.log = 0
⊢ N ^ ((1 - r) / 2) = 0
Tactic:
linarith [Real.log_pos hN]
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun N => N * N.log⁻¹) = fun N => N / N.log
Tactic:
simp_rw [div_eq_mul_inv]
State after:
no goals