rw [Asymptotics.isBigO_iff] at this ⊢
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
this : (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | ε * σ₁ ≤ s.re ∧ s.re ≤ ε * σ₂}] fun s => 1 / ‖s‖
⊢ (fun s => ‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / (ε * ‖s‖ ^ 2)
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
this : ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | ε * σ₁ ≤ s.re ∧ s.re ≤ ε * σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ c * ‖1 / ‖x‖‖
⊢ ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖