rw [Complex.norm_eq_abs, abs_cpow_eq_rpow_re_of_pos (by linarith [mem_Icc.mp hx])]
𝕂 : 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
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
⊢ ‖↑x ^ s‖ ≤ 2 ^ σ₂
𝕂 : 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
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
⊢ x ^ s.re ≤ 2 ^ σ₂