Theorem: nabla_log (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
⊢ (nabla fun x => (x / b).log) =O[atTop] fun x => 1 / x
Tactic:
refine EventuallyEq.trans_isBigO ?_ nabla_log_main
State after:
n : ℕ
A a b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
⊢ (nabla fun x => (x / b).log) =ᶠ[atTop] nabla Real.log

State before:
n : ℕ
A a b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
⊢ (nabla fun x => (x / b).log) =ᶠ[atTop] nabla Real.log
Tactic:
filter_upwards [eventually_gt_atTop 0] with x l2
State after:
case h
n : ℕ
A a b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
x : ℝ
l2 : 0 < x
⊢ nabla (fun x => (x / b).log) x = nabla Real.log x

State before:
case h
n : ℕ
A a b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
x : ℝ
l2 : 0 < x
⊢ nabla (fun x => (x / b).log) x = nabla Real.log x
Tactic:
rw [nabla, log_div (by linarith) (by linarith), log_div l2.ne.symm (by linarith), nabla]
State after:
case h
n : ℕ
A a b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
x : ℝ
l2 : 0 < x
⊢ (x + 1).log - b.log - (x.log - b.log) = (x + 1).log - x.log

State before:
case h
n : ℕ
A a b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
x : ℝ
l2 : 0 < x
⊢ (x + 1).log - b.log - (x.log - b.log) = (x + 1).log - x.log
Tactic:
ring
State after:
no goals

State before:
n : ℕ
A a b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
x : ℝ
l2 : 0 < x
⊢ x + 1 ≠ 0
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
b : ℝ
hb : 0 < b
x : ℝ
l2 : 0 < x
⊢ b ≠ 0
Tactic:
linarith
State after:
no goals