simp only [Real.norm_eq_abs, Complex.norm_eq_abs, abs_ofReal, map_mul] at this ⊢
case h.h₂.calc_3.refine_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
this : ‖∫ (x : ℝ) in 1 / 2 ..2, (fun x => f x * ‖↑x ^ s‖) x‖ ≤ f a * 2 ^ σ₂ * |2 - 1 / 2|
⊢ ‖∫ (x : ℝ) in Icc (1 / 2) 2, ‖↑(deriv Ψ x) * ↑x ^ s‖‖ ≤ ‖deriv Ψ a‖ * 2 ^ σ₂ * (3 / 2)
case h.h₂.calc_3.refine_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
this : |∫ (x : ℝ) in 1 / 2 ..2, f x * Complex.abs (↑x ^ s)| ≤ f a * 2 ^ σ₂ * |2 - 1 / 2|
⊢ |∫ (x : ℝ) in Icc (1 / 2) 2, |deriv Ψ x| * Complex.abs (↑x ^ s)| ≤ |deriv Ψ a| * 2 ^ σ₂ * (3 / 2)