Complex.exists_norm_digamma_div_two_le_log

theorem exists_norm_digamma_div_two_le_log {a b : ℝ} (ha : 0 < a) :    ∃ C : ℝ, 0 < C ∧ ∀ w : ℂ, a ≤ w.re → w.re ≤ b →      ‖digamma (w / 2)‖ ≤ C * Real.log (|w.im| + 2) := by  obtain ⟨C, hC, hbound⟩ := exists_norm_digamma_le_log (a := a / 2) (b := b / 2) (by linarith)  refine ⟨C, hC, fun w hwa hwb => ?_⟩  have h2 : (2 : ℂ) = ((2 : ℝ) : ℂ) := by norm_num  have hre2 : (w / 2).re = w.re / 2 := by rw [h2, div_ofReal_re]  have him2 : (w / 2).im = w.im / 2 := by rw [h2, div_ofReal_im]  have h := hbound (w / 2) (by rw [hre2]; linarith) (by rw [hre2]; linarith)  refine le_trans h ?_  have him_le : |(w / 2).im| + 2 ≤ |w.im| + 2 := by    rw [him2, abs_div]    have h4 : (0 : ℝ) ≤ |w.im| := abs_nonneg _    have h5 : |(2 : ℝ)| = 2 := by norm_num    rw [h5]    linarith  exact mul_le_mul_of_nonneg_left (Real.log_le_log (by positivity) him_le) hC.le