The digamma function

This file defines the digamma function as the logarithmic derivative of the Gamma function and proves some basic properties.

Main definitions

• Complex.digamma: The digamma function of a complex variable.

Main statements

• Complex.digamma_apply_add_one: The digamma function satisfies the functional equation digamma (s + 1) = digamma s + s⁻¹.
• Complex.meromorphic_digamma: The digamma function is meromorphic.

TODO

• Prove Gauss' integral representation of the digamma function.

noncomputable def Complex.digamma : ℂ → ℂ

The digamma function, defined as the logarithmic derivative of the Gamma function.

theorem Complex.digamma_def : digamma = logDeriv Gamma

@[simp]

theorem Complex.digamma_zero : digamma 0 = 0

theorem Complex.digamma_one : digamma 1 = -↑Real.eulerMascheroniConstant

theorem Complex.digamma_one_half : (1 / 2).digamma = -2 * log 2 - ↑Real.eulerMascheroniConstant

theorem Complex.digamma_apply_add_one (s : ℂ) (hs : ∀ (m : ℕ), s ≠ -↑m) : (s + 1).digamma = s.digamma + s⁻¹

theorem Complex.meromorphic_digamma : Meromorphic digamma