Kadiri.kadiri_thm_3_1_q1_gamma_symmetrization

@[blueprint  "kadiri-thm-3-1-q1-gamma-symmetrization"  (title := "$\\Gamma'/\\Gamma$ symmetrization on the critical line")  (statement := /-- For every $s \in \mathbb{C}$ with $\Re s = 1/2$,  $$ \frac{1}{2}\!\left\{       \frac{\Gamma'}{\Gamma}\!\Big(\frac{s}{2}\Big)     + \frac{\Gamma'}{\Gamma}\!\Big(\frac{1-s}{2}\Big)       \right\}     \;=\; \Re\!\left[\frac{\Gamma'}{\Gamma}\!\Big(\frac{s}{2}\Big)\right]. $$  Used to identify the integrand of $I_3$ after shifting to the critical line  (\cite[p.~13]{Kadiri2005}, displayed equation between (14) and (15)). -/)  (proof := /-- On $\Re s = 1/2$, $1 - s = \bar s$, hence $(1 - s)/2 = \overline{s/2}$.  Since $\Gamma'/\Gamma$ has real Taylor coefficients away from its poles, it commutes  with complex conjugation: $\Gamma'/\Gamma((1-s)/2) = \overline{\Gamma'/\Gamma(s/2)}$.  Then $\tfrac{1}{2}(z + \bar z) = \Re z$ with $z = \Gamma'/\Gamma(s/2)$. To be  formalised. -/)  (latexEnv := "sublemma")  (discussion := 1544)]theorem kadiri_thm_3_1_q1_gamma_symmetrization {s : ℂ} (_hs : s.re = 1 / 2) :    (1 / 2 : ℂ) * (digamma (s / 2) + digamma ((1 - s) / 2)) =      ((digamma (s / 2)).re : ℂ) := by  have h1s : 1 - s = (starRingEnd ℂ) s := by    apply Complex.ext    · rw [Complex.sub_re, Complex.one_re, Complex.conj_re, _hs]      norm_num    · rw [Complex.sub_im, Complex.one_im, Complex.conj_im]      ring  have hconj : (1 - s) / 2 = (starRingEnd ℂ) (s / 2) := by    rw [map_div₀, map_ofNat, h1s]  rw [hconj, digamma_conj, Complex.add_conj]  push_cast  ring