Documentation

Mathlib.NumberTheory.Harmonic.GammaDeriv

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 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 γ.