use f a * 2 ^ σ₂ * (3 / 2)
case intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
⊢ ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ c * ‖1 / ‖x‖‖
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
⊢ ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ f a * 2 ^ σ₂ * (3 / 2) * ‖1 / ‖x‖‖