Theorem: log_mul_add_isBigO_log (PrimeNumberTheoremAnd/Wiener.lean)

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

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Tactic:
have l2 : ∀ᶠ x : ℝ in atTop, 0 ≤ log x := tendsto_atTop.mp tendsto_log_atTop 0
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Tactic:
have l3 : ∀ᶠ x : ℝ in atTop, 0 ≤ log (a * x + b) :=
  tendsto_atTop.mp (tendsto_log_atTop.comp (tendsto_mul_add_atTop ha b)) 0
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Tactic:
have l5 : ∀ᶠ x : ℝ in atTop, 1 ≤ a * x + b := tendsto_atTop.mp (tendsto_mul_add_atTop ha b) 1
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5 : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5 : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Tactic:
have l1 : ∀ᶠ x : ℝ in atTop, a * x + b ≤ x ^ 2 := by
  filter_upwards [(isLittleO_mul_add_sq a b).eventuallyLE, l5] with x r2 l5
  simpa [abs_eq_self.mpr (zero_le_one.trans l5)] using r2
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5 : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
l1 : ∀ᶠ (x : ℝ) in atTop, a * x + b ≤ x ^ 2
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖

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

State before:
case h
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5✝ : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
l1✝ : ∀ᶠ (x : ℝ) in atTop, a * x + b ≤ x ^ 2
x : ℝ
l1 : a * x + b ≤ x ^ 2
l2 : 0 ≤ x.log
l3 : 0 ≤ (a * x + b).log
l5 : 1 ≤ a * x + b
⊢ ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Tactic:
simpa [abs_eq_self.mpr l2, abs_eq_self.mpr l3, Real.log_pow] using Real.log_le_log (by linarith) l1
State after:
no goals

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5 : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
⊢ ∀ᶠ (x : ℝ) in atTop, a * x + b ≤ x ^ 2
Tactic:
filter_upwards [(isLittleO_mul_add_sq a b).eventuallyLE, l5] with x r2 l5
State after:
case h
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5✝ : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
x : ℝ
r2 : ‖a * x + b‖ ≤ ‖x ^ 2‖
l5 : 1 ≤ a * x + b
⊢ a * x + b ≤ x ^ 2

State before:
case h
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5✝ : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
x : ℝ
r2 : ‖a * x + b‖ ≤ ‖x ^ 2‖
l5 : 1 ≤ a * x + b
⊢ a * x + b ≤ x ^ 2
Tactic:
simpa [abs_eq_self.mpr (zero_le_one.trans l5)] using r2
State after:
no goals

State before:
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5✝ : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
l1✝ : ∀ᶠ (x : ℝ) in atTop, a * x + b ≤ x ^ 2
x : ℝ
l1 : a * x + b ≤ x ^ 2
l2 : 0 ≤ x.log
l3 : 0 ≤ (a * x + b).log
l5 : 1 ≤ a * x + b
⊢ 0 < a * x + b
Tactic:
linarith
State after:
no goals