Gamma and digamma functions

The gamma, digamma and trigamma functions: series and integral representations, factorial series, growth bounds against exponentials, and Ramanujan's digamma identities.

• Digamma and trigamma functions
• Iterated factorials and power towers
• Series and integrals for the digamma function

TheoremRamanujan's asymptotic expansion of \(((x + 1/2)/e^{\psi(x+1)})^{4n}\)#✓fully proved

For real \(x\) let \(\psi(x) = \Gamma'(x)/\Gamma(x)\) and \(a(x) = e^{\psi(x+1)}\). Then \(a(x) \to \infty\) as \(x \to \infty\), and for every complex number \(n\),

\[\left(\frac{x + 1/2}{a(x)}\right)^{4n} = 1 - \frac{n}{6 a(x)^2} + \frac{10 n^2 + 11 n}{720 a(x)^4} - \frac{70 n^3 + 231 n^2 + 891 n}{90720 a(x)^6} + O\left(\frac{1}{a(x)^8}\right)\]

as \(x \to \infty\) through the real numbers, where the power is the principal complex power.

Proof: Convexity of log Γ gives crude digamma bounds. A telescoped centered expansion and Taylor's formula for the complex exponential then give the stated coefficients and remainder.

theorem ramanujan_part1_ch8_entry15_doublegamma (n : ℂ) :
    Tendsto chapter8Entry15A atTop atTop ∧
      IsBigO atTop
        (fun x : ℝ => chapter8Entry15Power n x - chapter8Entry15Approx n x)
        (fun x : ℝ => (1 : ℂ) / (chapter8Entry15A x : ℂ) ^ 8)

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 8.

Uses 1

Proof usesComplex and real derivatives of Gamma agree on the positive reals

TheoremRamanujan's multiplication formula for the series \(\sum_k (\log k/k - \log(k+x)/(k+x))\)#✓fully proved

For real \(x\) let

\[\varphi(x) = \sum_{k=1}^{\infty} \left(\frac{\log k}{k} - \frac{\log(k+x)}{k+x}\right),\]

and let \(\psi(x) = \Gamma'(x)/\Gamma(x)\). Let \(x > -1\) be real and let \(n \ge 1\) be an integer. Then \(k + x > 0\) and \(k + (x - j)/n > 0\) for all integers \(k \ge 1\) and \(0 \le j < n\); the series defining \(\varphi(x)\) and \(\varphi((x - j)/n)\) for \(0 \le j < n\) converge absolutely; \(\Gamma(x + 1) > 0\); and

\[n \varphi(x) - \sum_{j=0}^{n-1} \varphi\left(\frac{x - j}{n}\right) = n \log n \, \psi(x + 1) - \frac{n (\log n)^2}{2}.\]

theorem ramanujan_part1_ch8_entry17_loggammaintegral (x : ℝ) (n : ℕ)
    (hx : -1 < x) (hn : 0 < n) :
    (∀ j : ℕ, 0 < (j + 1 : ℝ) + x) ∧
      (∀ k ∈ range n, ∀ j : ℕ,
        0 < (j + 1 : ℝ) + (x - k) / n) ∧
      Summable (chapter8Entry17Term x) ∧
      (∀ k ∈ range n,
        Summable (chapter8Entry17Term ((x - k) / n))) ∧
      0 < Real.Gamma (x + 1) ∧
      (n : ℝ) * chapter8Entry17Phi x -
          ∑ k ∈ range n, chapter8Entry17Phi ((x - k) / n) =
        (n : ℝ) * Real.log n * chapter8RealDigamma (x + 1) -
          (n : ℝ) * Real.log n ^ 2 / 2

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 8.

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.