Theorem: isBigO_log_mul_add (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 : ℝ
⊢ Real.log =O[atTop] fun x => (a * x + b).log
Tactic:
convert (log_mul_add_isBigO_log (b := -b / a) (inv_pos.mpr ha)).comp_tendsto (tendsto_mul_add_atTop (b := b) ha) using 1
State after:
case h.e'_7
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
⊢ Real.log = (fun x => (a⁻¹ * x + -b / a).log) ∘ fun x => a * x + b

State before:
case h.e'_7
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
⊢ Real.log = (fun x => (a⁻¹ * x + -b / a).log) ∘ fun x => a * x + b
Tactic:
ext x
State after:
case h.e'_7.h
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b x : ℝ
⊢ x.log = ((fun x => (a⁻¹ * x + -b / a).log) ∘ fun x => a * x + b) x

State before:
case h.e'_7.h
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b x : ℝ
⊢ x.log = ((fun x => (a⁻¹ * x + -b / a).log) ∘ fun x => a * x + b) x
Tactic:
field_simp [ha.ne.symm]
State after:
no goals