Derivative of Γ at positive integers

We prove the formula for the derivative of Real.Gamma at a positive integer:

deriv Real.Gamma (n + 1) = Nat.factorial n * (-Real.eulerMascheroniConstant + harmonic n)

theorem Real.deriv_Gamma_nat (n : ℕ) : deriv Gamma (↑n + 1) = ↑n.factorial * (-eulerMascheroniConstant + ↑(harmonic n))

Explicit formula for the derivative of the Gamma function at positive integers, in terms of harmonic numbers and the Euler-Mascheroni constant γ.

theorem Real.hasDerivAt_Gamma_nat (n : ℕ) : HasDerivAt Gamma (↑n.factorial * (-eulerMascheroniConstant + ↑(harmonic n))) (↑n + 1)

theorem Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1

theorem Real.hasDerivAt_Gamma_one : HasDerivAt Gamma (-eulerMascheroniConstant) 1

theorem Real.hasDerivAt_Gamma_one_half : HasDerivAt Gamma (-√Real.pi * (eulerMascheroniConstant + 2 * log 2)) (1 / 2)

theorem Complex.differentiable_at_Gamma_nat_add_one (n : ℕ) : DifferentiableAt ℂ Gamma (↑n + 1)

theorem Complex.hasDerivAt_Gamma_nat (n : ℕ) : HasDerivAt Gamma (↑n.factorial * (-↑Real.eulerMascheroniConstant + ↑(harmonic n))) (↑n + 1)

theorem Complex.deriv_Gamma_nat (n : ℕ) : deriv Gamma (↑n + 1) = ↑n.factorial * (-↑Real.eulerMascheroniConstant + ↑(harmonic n))

Explicit formula for the derivative of the complex Gamma function at positive integers, in terms of harmonic numbers and the Euler-Mascheroni constant γ.

theorem Complex.hasDerivAt_Gamma_one : HasDerivAt Gamma (-↑Real.eulerMascheroniConstant) 1

theorem Complex.hasDerivAt_Gamma_one_half : HasDerivAt Gamma (-↑√Real.pi * (↑Real.eulerMascheroniConstant + 2 * log 2)) (1 / 2)

theorem Complex.hasDerivAt_Gammaℂ_one : HasDerivAt Gammaℂ (-(↑Real.eulerMascheroniConstant + log (2 * ↑Real.pi)) / ↑Real.pi) 1

theorem Complex.hasDerivAt_Gammaℝ_one : HasDerivAt Gammaℝ (-(↑Real.eulerMascheroniConstant + log (4 * ↑Real.pi)) / 2) 1