LogDerivZetaBoundForI1

lemma LogDerivZetaBoundForI1 : ∃ C > 0, ∀ {X T : ℝ} (_Xgt3 : 3 < X) (_Tgt3 : 3 < T)    (t : ℝ) (_ht : t ≤ -T),    let σ := 1 + (Real.log X)⁻¹    ‖deriv riemannZeta (σ + t * I) / riemannZeta (σ + t * I)‖ ≤ C * (Real.log (-t))^2 := by  obtain ⟨C, hC⟩ := LogDerivZetaUniformLogSquaredBound  field_simp  use C + 1  refine ⟨by grind, fun {X T} hX hT t ht ↦ (hC.2 _ _ ?_ ?_).trans ?_⟩  · cases abs_cases t <;> grind  · apply Set.mem_Ici.mpr    have hX' : 0 ≤ 1 / Real.log X := one_div_nonneg.mpr (Real.log_nonneg (by grind))    have ht' : 0 ≤ F / Real.log |t| := by      apply div_nonneg (Fequ ▸ div_nonneg (le_of_lt EinIoo.1) zero_le_three)      exact Real.log_nonneg (by cases abs_cases t <;> grind)    grind  · simp only [abs_of_nonpos (by grind : t ≤ 0)]    nlinarith [hC.1, sq_nonneg (Real.log (-t))]