# 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) = ↑(Nat.factorial n) * (-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 (↑(Nat.factorial n) * (-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 Complex.differentiable_at_Gamma_nat_add_one (n : ℕ) : DifferentiableAt ℂ Complex.Gamma (↑n + 1)

theorem Complex.deriv_Gamma_nat (n : ℕ) : deriv Complex.Gamma (↑n + 1) = ↑(Nat.factorial n) * (-↑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_nat (n : ℕ) : HasDerivAt Complex.Gamma (↑(Nat.factorial n) * (-↑Real.eulerMascheroniConstant + ↑(harmonic n))) (↑n + 1)

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