theorem digamma_gauss_theorem (x : ℚ) (h1 : x > 0) (h2 : x < 1) : (↑x).digamma = -↑Real.eulerMascheroniConstant - ↑(Real.log (2 * ↑x.den)) - ↑Real.pi / 2 * ↑(↑x * Real.pi).cot + 2 * ↑(∑ n ∈ Finset.Icc 1 (⌈↑x.den / 2⌉ - 1), Real.cos (2 * Real.pi * ↑x.num * ↑n / ↑x.den) * Real.log (Real.sin (Real.pi * ↑n / ↑x.den)))

theorem digamma_one_fourth : (1 / 4).digamma = -↑Real.eulerMascheroniConstant - 3 * ↑(Real.log 2) - ↑Real.pi / 2