LogDerivZetaHolcSmallT

@[blueprint  (title := "LogDerivZetaHolcSmallT")  (statement := /--  There is a $\sigma_2 < 1$ so that the function  $$  \frac {\zeta'}{\zeta}(s)  $$  is holomorphic on $\{ \sigma_2 \le \Re s \le 2, |\Im s| \le 3 \} \setminus \{1\}$.  -/)  (proof := /--  The derivative of $\zeta$ is holomorphic away from $s=1$; the denominator $\zeta(s)$ is nonzero  in this range by Lemma \ref{ZetaNoZerosInBox}.  -/)  (latexEnv := "lemma")]theorem LogDerivZetaHolcSmallT :    ∃ (σ₂ : ℝ) (_ : σ₂ < 1), HolomorphicOn (fun (s : ℂ) ↦ ζ' s / (ζ s))      (( [[ σ₂, 2 ]] ×ℂ [[ -3, 3 ]]) \ {1}) := by  obtain ⟨σ₂, hσ₂_lt_one, hζ_ne_zero⟩ := ZetaNoZerosInBox 3  refine ⟨σ₂, hσ₂_lt_one, ?_⟩  let U := ([[σ₂, 2]] ×ℂ [[-3, 3]]) \ {1}  have s_in_U_im_le3 : ∀ s ∈ U, |s.im| ≤ 3 := by    intro s hs    rw [Set.mem_sdiff_singleton] at hs    rcases hs with ⟨hbox, _hne⟩    rcases hbox with ⟨hre, him⟩    simp only [Set.mem_preimage] at him    obtain ⟨him_lower, him_upper⟩ := him    apply abs_le.2    simp only [neg_le_self_iff, Nat.ofNat_nonneg, inf_of_le_left] at him_lower    simp only [neg_le_self_iff, Nat.ofNat_nonneg, sup_of_le_right] at him_upper    exact ⟨him_lower, him_upper⟩   have s_in_U_re_ges2 : ∀ s ∈ U, σ₂ ≤ s.re := by    intro s hs    rw [Set.mem_sdiff_singleton] at hs    rcases hs with ⟨hbox, _hne⟩    rcases hbox with ⟨hre, _him⟩    simp only [Set.mem_preimage] at hre    obtain ⟨hre_lower, hre_upper⟩ := hre    have : min σ₂ 2 = σ₂ := by      apply min_eq_left      linarith [hσ₂_lt_one]    rwa [← this]   apply LogDerivZetaHoloOn  · exact Set.notMem_sdiff_of_mem rfl  · intro s hs    rw[← re_add_im s]    apply hζ_ne_zero    · apply s_in_U_im_le3 _ hs    · apply s_in_U_re_ges2 _ hs