Documentation

Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Derivative of the Gamma function #

This file shows that the (complex) Γ function is complex-differentiable at all s : ℂ with s ∉ {-n : n ∈ ℕ}, as well as the real counterpart.

Main results #

Tags #

Gamma

Now check that the Γ function is differentiable, wherever this makes sense.

Rewrite the Gamma integral as an example of a Mellin transform.

The derivative of the Γ integral, at any s ∈ ℂ with 1 < re s, is given by the Mellin transform of log t * exp (-t).

theorem Complex.differentiableAt_GammaAux (s : ) (n : ) (h1 : 1 - s.re < n) (h2 : ∀ (m : ), s -m) :

At s = 0, the Gamma function has a simple pole with residue 1.

theorem Real.differentiableAt_Gamma {s : } (hs : ∀ (m : ), s -m) :