Theorem: nabla_log_main (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ nabla Real.log =O[atTop] fun x => 1 / x
Tactic:
apply IsBigO.of_bound 1
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ∀ᶠ (x : ℝ) in atTop, ‖nabla Real.log x‖ ≤ 1 * ‖1 / x‖

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ∀ᶠ (x : ℝ) in atTop, ‖nabla Real.log x‖ ≤ 1 * ‖1 / x‖
Tactic:
filter_upwards [eventually_gt_atTop 0] with x l1
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
l1 : 0 < x
⊢ ‖nabla Real.log x‖ ≤ 1 * ‖1 / x‖

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
l1 : 0 < x
⊢ ‖nabla Real.log x‖ ≤ 1 * ‖1 / x‖
Tactic:
have l2 : log x ≤ log (x + 1) := log_le_log l1 (by linarith)
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
l1 : 0 < x
l2 : x.log ≤ (x + 1).log
⊢ ‖nabla Real.log x‖ ≤ 1 * ‖1 / x‖

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
l1 : 0 < x
l2 : x.log ≤ (x + 1).log
⊢ ‖nabla Real.log x‖ ≤ 1 * ‖1 / x‖
Tactic:
simpa [nabla, abs_eq_self.mpr l1.le, abs_eq_self.mpr (sub_nonneg.mpr l2)] using log_add_one_sub_log_le l1
State after:
no goals

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