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.digamma_apply_add_nat: The iterated recurrence digamma (s + n) = digamma s + ∑ k ∈ Finset.range n, (s + k)⁻¹.
• Complex.digamma_nat_add_one: The digamma function at positive integers, in terms of harmonic numbers: digamma (n + 1) = harmonic n - eulerMascheroniConstant.
• Complex.digamma_one_sub: Euler's reflection formula digamma (1 - s) = digamma s + π * cot (π * s).
• Complex.digamma_two_mul: The duplication formula digamma (2 * s) = (1 / 2) * (digamma s + digamma (s + 1 / 2)) + log 2.
• 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.

Equations

• Complex.digamma = logDeriv Complex.Gamma

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.digamma_apply_add_nat {s : ℂ} (hs : ∀ (m : ℕ), s ≠ -↑m) (n : ℕ) : (s + ↑n).digamma = s.digamma + ∑ k ∈ Finset.range n, (s + ↑k)⁻¹

The iterated digamma recurrence ψ(s + n) = ψ(s) + ∑_{k < n} 1 / (s + k), for s ∉ {0, -1, -2, …}. Proved by induction from digamma_apply_add_one.

theorem Complex.digamma_nat_add_one (n : ℕ) : (↑n + 1).digamma = ↑(harmonic n) - ↑Real.eulerMascheroniConstant

The digamma function at a positive integer, in terms of harmonic numbers.

theorem Complex.digamma_one_sub {s : ℂ} (hs : ∀ (n : ℤ), s ≠ ↑n) : (1 - s).digamma = s.digamma + ↑Real.pi * (↑Real.pi * s).cot

Euler's reflection formula for the digamma function: ψ (1 - s) = ψ s + π * cot (π * s) for s not an integer.

theorem Complex.meromorphic_digamma : Meromorphic digamma

theorem HasDerivAt.logDeriv_Gamma {g : ℂ → ℂ} {a s : ℂ} (hg : HasDerivAt g a s) (h : ∀ (m : ℕ), g s ≠ -↑m) : logDeriv (fun (z : ℂ) => Complex.Gamma (g z)) s = a * (g s).digamma

If g has derivative a at s, then the logarithmic derivative of Gamma ∘ g at s is a * digamma (g s).

theorem Complex.digamma_two_mul {s : ℂ} (hs : ∀ (m : ℕ), 2 * s ≠ -↑m) : (2 * s).digamma = 1 / 2 * (s.digamma + (s + 1 / 2).digamma) + log 2

The digamma duplication formula ψ(2s) = ½(ψ(s) + ψ(s + ½)) + log 2, for 2s ∉ {0, -1, -2, …}, which is equivalent to s and s + ½ both avoiding the poles of ψ. Proved from Legendre's doubling Complex.Gamma_mul_Gamma_add_half by taking logarithmic derivatives.