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

• Complex.differentiableAt_Gamma: Γ is complex-differentiable at all s : ℂ with s ∉ {-n : n ∈ ℕ}.
• Real.differentiableAt_Gamma: Γ is real-differentiable at all s : ℝ with s ∉ {-n : n ∈ ℕ}.

Tags

Gamma

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

theorem Complex.GammaIntegral_eq_mellin : Complex.GammaIntegral = mellin fun (x : ℝ) => ↑(Real.exp (-x))

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

theorem Complex.hasDerivAt_GammaIntegral {s : ℂ} (hs : 0 < s.re) : HasDerivAt Complex.GammaIntegral (∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (s - 1) * (↑(Real.log t) * ↑(Real.exp (-t)))) s

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) : DifferentiableAt ℂ (Complex.GammaAux n) s

theorem Complex.differentiableAt_Gamma (s : ℂ) (hs : ∀ (m : ℕ), s ≠ -↑m) : DifferentiableAt ℂ Complex.Gamma s

theorem Complex.tendsto_self_mul_Gamma_nhds_zero : Filter.Tendsto (fun (z : ℂ) => z * Complex.Gamma z) (nhdsWithin 0 {0}ᶜ) (nhds 1)

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

theorem Real.differentiableAt_Gamma {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -↑m) : DifferentiableAt ℝ Real.Gamma s