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

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

theorem Complex.differentiableAt_Gamma_one : DifferentiableAt ℂ Gamma 1

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

theorem Complex.continuousAt_Gamma_one : ContinuousAt Gamma 1

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

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

theorem Complex.not_continuousAt_Gamma_zero : ¬ContinuousAt Gamma 0

theorem Complex.not_differentiableAt_Gamma_zero : ¬DifferentiableAt ℂ Gamma 0

theorem Complex.not_continuousAt_Gamma_neg_nat (n : ℕ) : ¬ContinuousAt Gamma (-↑n)

theorem Complex.not_differentiableAt_Gamma_neg_nat (n : ℕ) : ¬DifferentiableAt ℂ Gamma (-↑n)

theorem Complex.deriv_Gamma_add_one (s : ℂ) (hs : s ≠ 0) : deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s

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

theorem Real.differentiableOn_Gamma_Ioi : DifferentiableOn ℝ Gamma (Set.Ioi 0)