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 : Nat) : Eq (deriv Gamma (HAdd.hAdd n.cast 1)) (HMul.hMul n.factorial.cast (HAdd.hAdd (Neg.neg eulerMascheroniConstant) (harmonic n).cast))

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 : Nat) : HasDerivAt Gamma (HMul.hMul n.factorial.cast (HAdd.hAdd (Neg.neg eulerMascheroniConstant) (harmonic n).cast)) (HAdd.hAdd n.cast 1)

theorem Real.eulerMascheroniConstant_eq_neg_deriv : Eq eulerMascheroniConstant (Neg.neg (deriv Gamma 1))

theorem Real.hasDerivAt_Gamma_one : HasDerivAt Gamma (Neg.neg eulerMascheroniConstant) 1

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)

theorem Complex.differentiable_at_Gamma_nat_add_one (n : Nat) : DifferentiableAt Complex Gamma (HAdd.hAdd n.cast 1)

theorem Complex.hasDerivAt_Gamma_nat (n : Nat) : HasDerivAt Gamma (HMul.hMul n.factorial.cast (HAdd.hAdd (Neg.neg (ofReal Real.eulerMascheroniConstant)) (harmonic n).cast)) (HAdd.hAdd n.cast 1)

theorem Complex.deriv_Gamma_nat (n : Nat) : Eq (deriv Gamma (HAdd.hAdd n.cast 1)) (HMul.hMul n.factorial.cast (HAdd.hAdd (Neg.neg (ofReal Real.eulerMascheroniConstant)) (harmonic n).cast))

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 (Neg.neg (ofReal Real.eulerMascheroniConstant)) 1

theorem Complex.hasDerivAt_Gamma_one_half : HasDerivAt Gamma (HMul.hMul (Neg.neg (ofReal Real.pi.sqrt)) (HAdd.hAdd (ofReal Real.eulerMascheroniConstant) (HMul.hMul 2 (log 2)))) (1 / 2)

theorem Complex.hasDerivAt_Gammaℂ_one : HasDerivAt Gammaℂ (HDiv.hDiv (Neg.neg (HAdd.hAdd (ofReal Real.eulerMascheroniConstant) (log (HMul.hMul 2 (ofReal Real.pi))))) (ofReal Real.pi)) 1

theorem Complex.hasDerivAt_Gammaℝ_one : HasDerivAt Gammaℝ (HDiv.hDiv (Neg.neg (HAdd.hAdd (ofReal Real.eulerMascheroniConstant) (log (HMul.hMul 4 (ofReal Real.pi))))) 2) 1