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)
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_one_half :
HasDerivAt Gamma (HMul.hMul (Neg.neg Real.pi.sqrt) (HAdd.hAdd eulerMascheroniConstant (HMul.hMul 2 (log 2)))) (1 / 2)
Explicit formula for the derivative of the complex Gamma function at positive integers, in
terms of harmonic numbers and the Euler-Mascheroni constant γ
.