have l3 : ∀ᶠ x : ℝ in atTop, 0 ≤ log (a * x + b) :=
  tendsto_atTop.mp (tendsto_log_atTop.comp (tendsto_mul_add_atTop ha b)) 0
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‖
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‖