# 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 Real.Gamma (↑n + 1) = ↑n.factorial * (-Real.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 Real.Gamma (↑n.factorial * (-Real.eulerMascheroniConstant + ↑(harmonic n))) (↑n + 1)

theorem Real.eulerMascheroniConstant_eq_neg_deriv : Real.eulerMascheroniConstant = -deriv Real.Gamma 1

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

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

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

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

theorem Complex.deriv_Gamma_nat (n : ℕ) : deriv Complex.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 Complex.Gamma (-↑Real.eulerMascheroniConstant) 1

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

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

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