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

theorem Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1

theorem Real.eulerMascheroniConstant_eq_neg_integral_log : eulerMascheroniConstant = -∫ (t : ℝ) in Set.Ioi 0, log t * exp (-t)

The Euler–Mascheroni constant as an integral: γ = -∫₀^∞ log t · e^{-t} dt.

theorem Real.eulerMascheroniConstant_eq_neg_integral_log_log {s : ℝ} (hs : 1 < s) : eulerMascheroniConstant = -log (s - 1) + -((s - 1) * ∫ (t : ℝ) in Set.Ioi 1, log (log t) * t ^ (-s))

An integral representation of the Euler–Mascheroni constant, valid for any s > 1.

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

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

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

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

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

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

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

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