Derive Gauss multiplication from the digamma multiplication identity

Proved

ErlerGross.gamma_multiplication_formula_of_digamma

by Eyal1990 · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

For each positive integer n, if the digamma multiplication identity holds at every complex z with positive real part, then there is a nonzero constant c such that the Gauss multiplication identity for Gamma holds for every complex z.

Preamble

import Mathlib

Formal statement

namespace ErlerGross
theorem gamma_multiplication_formula_of_digamma (n : Nat) (hn : 0 < n)
    (hpsi : forall z : Complex, 0 < z.re ->
      Finset.sum (Finset.range n) (fun k => Complex.digamma (z + (k : Complex) / n)) =
        n * Complex.digamma ((n : Complex) * z) - n * (Real.log n : Complex)) :
    Exists fun c : Complex => And (Not (c = 0)) (forall z : Complex,
      Finset.prod (Finset.range n) (fun k => Complex.Gamma (z + (k : Complex) / n)) =
        c * Complex.exp (-(n : Complex) * z * (Real.log n : Complex)) *
          Complex.Gamma ((n : Complex) * z)) := by
  sorry
end ErlerGross

Source

Reduction lemma for Gauss multiplication formula; compare NIST DLMF 5.5.6 and 5.5.9, https://dlmf.nist.gov/5.5.E6 and https://dlmf.nist.gov/5.5.E9

View graph