ZetaAbelFractKernel.kernel_deriv_norm_bound_on_ball

theorem kernel_deriv_norm_bound_on_ball (ε : ℝ) (u : ℝ) (hu : 1 < u) (x : ℂ) (hx : ε ≤ x.re) :    ‖-((Real.log u) : ℂ) * zetaAbelFractKernel x u‖ ≤ Real.log u * u ^ (-1 - ε) := by  have hu1 : (1 : ℝ) ≤ u := le_of_lt hu  have hinner : ‖zetaAbelFractKernel x u‖ ≤ u ^ (-1 - ε) :=    (norm_zetaAbelFractKernel_le u hu1 x).trans (Real.rpow_le_rpow_of_exponent_le hu1 (by linarith))  have hlognorm : ‖-((Real.log u) : ℂ)‖ = Real.log u := by    have hnonneg : 0 ≤ Real.log u := le_of_lt (Real.log_pos hu)    simp [norm_neg, Complex.norm_real, abs_of_nonneg hnonneg]  calc    ‖-((Real.log u) : ℂ) * zetaAbelFractKernel x u‖        = Real.log u * ‖zetaAbelFractKernel x u‖ := by rw [norm_mul, hlognorm]    _ ≤ Real.log u * u ^ (-1 - ε) := mul_le_mul_of_nonneg_left hinner (le_of_lt (Real.log_pos hu))