Series and integrals for the digamma function

TheoremSeries for the derivative of \(\Gamma'(z+1)/\Gamma(z+1)\)#✓fully proved

Let \(\gamma\) be the Euler–Mascheroni constant and let \(\varphi(w) = \gamma + \Gamma'(w+1)/\Gamma(w+1)\) for complex \(w\). For every complex number \(z\) other than \(-1, -2, -3, \dots\), the function \(\varphi\) is complex differentiable at \(z\), and the series \(\sum_{k=1}^{\infty} \frac{1}{(z+k)^2}\) converges absolutely with sum \(\varphi'(z)\).

theorem ramanujan_part1_ch6_entry2_stirlingseries (z : ℂ)
    (hz : ∀ k : ℕ, z ≠ -((k + 1 : ℕ) : ℂ)) :
    DifferentiableAt ℂ chapter6HarmonicInterpolation z ∧
      HasSum (fun k : ℕ => 1 / (z + (k + 1 : ℕ)) ^ 2)
        (deriv chapter6HarmonicInterpolation z) ∧
      Summable (fun k : ℕ => ‖(1 / (z + (k + 1 : ℕ)) ^ 2 : ℂ)‖)

Sources

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

Uses 6

Proof usesAnalyticity of the Gamma function · Complex and real derivatives of Gamma agree on the positive reals · Absolute convergence of the trigamma series · Logarithmic derivative of the real Gamma function · Derivative of the digamma series · Digamma series on the positive reals

TheoremRamanujan's integral for \(\psi(1 - 1/x)\) (Chapter 8, Entry 10)#✓fully proved

Let \(x\) be a complex number with \(\operatorname{Re} x < 0\). For real \(u\) put \(u^x = e^{x \log |u|}\) when \(u \ne 0\), and define \(K_x(0) = 0\), \(K_x(1) = -1/x\) and \(K_x(u) = \frac{1 - u}{u\,(u^x - 1)}\) for every other real \(u\), the quotient being taken to be \(0\) at \(u = -1\), where its denominator vanishes. Then \(x \ne 0\) and \(\Gamma(1 - 1/x) \ne 0\); for every \(u \in (0, 1)\) the denominator \(u\,(u^x - 1)\) is nonzero and \(K_x(u) = \frac{1 - u}{u\,(u^x - 1)}\); \(K_x\) is integrable on \([0, 1]\); and

\[\psi\left(1 - \frac{1}{x}\right) + \gamma = -x \int_0^1 K_x(u)\,du,\]

where \(\psi\) is the digamma function and \(\gamma\) is the Euler–Mascheroni constant.

theorem ramanujan_part1_ch8_entry10_qgammalimit (x : ℂ) (hx : x.re < 0) :
    x ≠ 0 ∧
      Complex.Gamma (1 - 1 / x) ≠ 0 ∧
      chapter8Entry10Kernel x 0 = 0 ∧
      chapter8Entry10Kernel x 1 = -1 / x ∧
      (∀ u : ℝ, u ∈ Set.Ioo 0 1 →
        (u : ℂ) * (Entry9Qgamma.chapter8UnitPow x u - 1) ≠ 0 ∧
          chapter8Entry10Kernel x u =
            ((1 - u : ℝ) : ℂ) /
              ((u : ℂ) * (Entry9Qgamma.chapter8UnitPow x u - 1))) ∧
      IntervalIntegrable (chapter8Entry10Kernel x) volume 0 1 ∧
      Complex.digamma (1 - 1 / x) +
          (Real.eulerMascheroniConstant : ℂ) =
        -x * ∫ u in (0 : ℝ)..1, chapter8Entry10Kernel x u

Sources

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

Uses 4

Proof usesComplex digamma series · Terms of the complex digamma series · Series expansion of the complex digamma function · Summability of the Basel series

TheoremDigamma as the logarithmic derivative of Gamma (used for Chapter 8, Entry 11)#✓fully proved

For every complex number \(z\), \(\Gamma'(z)/\Gamma(z) = \psi(z)\), where \(\psi\) is the digamma function.

At the poles \(z = 0, -1, -2, \dots\) the conventions \(\Gamma(z) = 0\) and division by zero giving \(0\) make both sides \(0\), so the identity holds for every \(z\).

theorem chapter8Digamma_eq_digamma (z : ℂ) :
    chapter8Digamma z = Complex.digamma z

Used by 1

Used byRamanujan's identity for \(\Gamma'/\Gamma\) at \(1/x\) and \(1 - 1/x\) (Chapter 8, Entry 11)

TheoremThe Entry 11 and Entry 12 series terms agree#✓fully proved

For every complex number \(x\) and every natural number \(j\), with \(k = j + 1\), the term \(\frac{2}{(kx)^3 - kx}\) as defined for Entry 11 equals the term given by the same formula for Entry 12.

In both definitions a term with zero denominator is \(0\).

theorem chapter8PhiTerm_eq_entry12Qgammaintegers (x : ℂ) (j : ℕ) :
    chapter8PhiTerm x j =
      MathlibExt.Analysis.Ramanujan.Part1Ch8.Entry12Qgammaintegers.chapter8PhiTerm x j

Used by 1

Used byThe Entry 11 and Entry 12 definitions of \(\varphi\) agree

TheoremThe Entry 11 and Entry 12 definitions of \(\varphi\) agree#✓fully proved

For every complex number \(x\), the function \(\varphi(x) = 1 + \sum_{k \ge 1} \frac{2}{(kx)^3 - kx}\) as defined for Entry 11 equals the function given by the same formula for Entry 12.

In both definitions the sum is the unconditional sum, taken to be \(0\) when it does not converge, and a term with zero denominator is \(0\).

theorem chapter8Phi_eq_entry12Qgammaintegers (x : ℂ) :
    chapter8Phi x =
      MathlibExt.Analysis.Ramanujan.Part1Ch8.Entry12Qgammaintegers.chapter8Phi x

Uses 1

Proof usesThe Entry 11 and Entry 12 series terms agree

TheoremChapter 8, Entry 11 in terms of the digamma function#✓fully proved

Let \(x\) be a nonzero complex number with \(x \ne 1/k\) and \(x \ne -1/k\) for every positive integer \(k\), and put \(\varphi(x) = 1 + \sum_{k \ge 1} \frac{2}{(kx)^3 - kx}\). Then the series \(\sum_{k \ge 1} \frac{2}{(kx)^3 - kx}\) converges unconditionally, \(\Gamma(1/x) \ne 0\), \(\Gamma(1 - 1/x) \ne 0\), and

\[\psi(1/x) + \psi(1 - 1/x) = -2\gamma - x\,\varphi(x),\]

where \(\psi\) is the digamma function and \(\gamma\) is the Euler–Mascheroni constant.

theorem ramanujan_part1_ch8_entry11_qgammafunctional_digamma
    (x : ℂ) (hx0 : x ≠ 0)
    (hpoles : ∀ k : ℕ,
      x ≠ 1 / ((k + 1 : ℕ) : ℂ) ∧
        x ≠ -(1 / ((k + 1 : ℕ) : ℂ))) :
    Summable (chapter8PhiTerm x) ∧
      Complex.Gamma (1 / x) ≠ 0 ∧
      Complex.Gamma (1 - 1 / x) ≠ 0 ∧
      Complex.digamma (1 / x) + Complex.digamma (1 - 1 / x) =
        -2 * (Real.eulerMascheroniConstant : ℂ) - x * chapter8Phi x

Uses 4 · Used by 1

Proof usesAnalyticity of the digamma function · Complex and real derivatives of Gamma agree on the positive reals · Logarithmic derivative of the real Gamma function · Digamma series on the positive reals

Used byRamanujan's identity for \(\Gamma'/\Gamma\) at \(1/x\) and \(1 - 1/x\) (Chapter 8, Entry 11)

TheoremRamanujan's identity for \(\Gamma'/\Gamma\) at \(1/x\) and \(1 - 1/x\) (Chapter 8, Entry 11)#✓fully proved

Let \(x\) be a nonzero complex number with \(x \ne 1/k\) and \(x \ne -1/k\) for every positive integer \(k\), and put \(\varphi(x) = 1 + \sum_{k \ge 1} \frac{2}{(kx)^3 - kx}\). Then the series \(\sum_{k \ge 1} \frac{2}{(kx)^3 - kx}\) converges unconditionally, \(\Gamma(1/x) \ne 0\), \(\Gamma(1 - 1/x) \ne 0\), and

\[\frac{\Gamma'(1/x)}{\Gamma(1/x)} + \frac{\Gamma'(1 - 1/x)}{\Gamma(1 - 1/x)} = -2\gamma - x\,\varphi(x),\]

where \(\gamma\) is the Euler–Mascheroni constant.

theorem ramanujan_part1_ch8_entry11_qgammafunctional
    (x : ℂ) (hx0 : x ≠ 0)
    (hpoles : ∀ k : ℕ,
      x ≠ 1 / ((k + 1 : ℕ) : ℂ) ∧
        x ≠ -(1 / ((k + 1 : ℕ) : ℂ))) :
    Summable (chapter8PhiTerm x) ∧
      Complex.Gamma (1 / x) ≠ 0 ∧
      Complex.Gamma (1 - 1 / x) ≠ 0 ∧
      chapter8Digamma (1 / x) + chapter8Digamma (1 - 1 / x) =
        -2 * (Real.eulerMascheroniConstant : ℂ) - x * chapter8Phi x

Sources

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

Uses 2

Proof usesDigamma as the logarithmic derivative of Gamma (used for Chapter 8, Entry 11) · Chapter 8, Entry 11 in terms of the digamma function

TheoremExponential and principal powers agree for positive bases (Chapter 8, Entry 12)#✓fully proved

For a complex number \(x\) and a real number \(u\), let \(P_x(u) = 0\) if \(u = 0\) and \(P_x(u) = e^{x \log |u|}\) otherwise. Then for every complex \(x\) and every real \(u > 0\), \(P_x(u) = u^x\), where \(u^x\) is the principal complex power.

theorem chapter8UnitPow_eq_cpow (x : ℂ) (u : ℝ) (hu : 0 < u) :
    chapter8UnitPow x u = (u : ℂ) ^ x

Used by 2

Used byRamanujan's integral for \(\varphi(x) - 1\) with principal powers (Chapter 8, Entry 12) · Ramanujan's integral for \(\varphi(x) - 1\) (Chapter 8, Entry 12)

TheoremRamanujan's integral for \(\varphi(x) - 1\) with principal powers (Chapter 8, Entry 12)#✓fully proved

Let \(x\) be a complex number with \(\operatorname{Re} x > 1\). For real \(u\) and complex \(s\) put \(P_s(u) = 0\) if \(u = 0\) and \(P_s(u) = e^{s \log |u|}\) otherwise, and define \(K_x(0) = 0\), \(K_x(1) = 0\) and \(K_x(u) = \frac{P_{x-2}(u)\,(1 - u)^2}{1 - P_x(u)}\) for every other real \(u\), the quotient being taken to be \(0\) at \(u = -1\), where its denominator vanishes. Let \(\varphi(x) = 1 + \sum_{k \ge 1} \frac{2}{(kx)^3 - kx}\). Then \((kx)^3 - kx \ne 0\) for every positive integer \(k\); the series \(\sum_{k \ge 1} \frac{2}{(kx)^3 - kx}\) converges unconditionally; \(K_x(0) = 0\) and \(K_x(1) = 0\); for every \(u \in (0, 1)\), with \(u^x\) and \(u^{x-2}\) the principal complex powers, \(1 - u^x \ne 0\) and \(K_x(u) = \frac{u^{x-2}\,(1 - u)^2}{1 - u^x}\); \(K_x\) is integrable on \([0, 1]\); and

\[\int_0^1 K_x(u)\,du = \varphi(x) - 1.\]

For \(u > 0\) the powers \(P_s(u)\) and \(u^s\) agree, so this is the same statement as the version written with \(P_s\).

MathlibExt.Analysis.Ramanujan.Part1Ch8.Entry12Qgammaintegers.ramanujan_part1_ch8_entry12_qgammaintegers_cpow · 15 lines

theorem ramanujan_part1_ch8_entry12_qgammaintegers_cpow (x : ℂ) (hx : 1 < x.re) :
    (∀ j : ℕ,
      let k : ℂ := j + 1
      (k * x) ^ 3 - k * x ≠ 0) ∧
      Summable (chapter8PhiTerm x) ∧
      chapter8Entry12Kernel x 0 = 0 ∧
      chapter8Entry12Kernel x 1 = 0 ∧
      (∀ u : ℝ, u ∈ Set.Ioo 0 1 →
        1 - (u : ℂ) ^ x ≠ 0 ∧
          chapter8Entry12Kernel x u =
            (u : ℂ) ^ (x - 2) * ((1 - u : ℝ) : ℂ) ^ 2 /
              (1 - (u : ℂ) ^ x)) ∧
      IntervalIntegrable (chapter8Entry12Kernel x) volume 0 1 ∧
      (∫ u in (0 : ℝ)..1, chapter8Entry12Kernel x u) =
        chapter8Phi x - 1

Uses 1 · Used by 1

Proof usesExponential and principal powers agree for positive bases (Chapter 8, Entry 12)

Used byRamanujan's integral for \(\varphi(x) - 1\) (Chapter 8, Entry 12)

TheoremRamanujan's integral for \(\varphi(x) - 1\) (Chapter 8, Entry 12)#✓fully proved

Let \(x\) be a complex number with \(\operatorname{Re} x > 1\). For real \(u\) and complex \(s\) put \(P_s(u) = 0\) if \(u = 0\) and \(P_s(u) = e^{s \log |u|}\) otherwise, and define \(K_x(0) = 0\), \(K_x(1) = 0\) and \(K_x(u) = \frac{P_{x-2}(u)\,(1 - u)^2}{1 - P_x(u)}\) for every other real \(u\), the quotient being taken to be \(0\) at \(u = -1\), where its denominator vanishes. Let \(\varphi(x) = 1 + \sum_{k \ge 1} \frac{2}{(kx)^3 - kx}\). Then \((kx)^3 - kx \ne 0\) for every positive integer \(k\); the series \(\sum_{k \ge 1} \frac{2}{(kx)^3 - kx}\) converges unconditionally; \(K_x(0) = 0\) and \(K_x(1) = 0\); for every \(u \in (0, 1)\), \(1 - P_x(u) \ne 0\) and \(K_x(u) = \frac{P_{x-2}(u)\,(1 - u)^2}{1 - P_x(u)}\); \(K_x\) is integrable on \([0, 1]\); and

\[\int_0^1 K_x(u)\,du = \varphi(x) - 1.\]

MathlibExt.Analysis.Ramanujan.Part1Ch8.Entry12Qgammaintegers.ramanujan_part1_ch8_entry12_qgammaintegers · 15 lines

theorem ramanujan_part1_ch8_entry12_qgammaintegers (x : ℂ) (hx : 1 < x.re) :
    (∀ j : ℕ,
      let k : ℂ := j + 1
      (k * x) ^ 3 - k * x ≠ 0) ∧
      Summable (chapter8PhiTerm x) ∧
      chapter8Entry12Kernel x 0 = 0 ∧
      chapter8Entry12Kernel x 1 = 0 ∧
      (∀ u : ℝ, u ∈ Set.Ioo 0 1 →
        1 - chapter8UnitPow x u ≠ 0 ∧
          chapter8Entry12Kernel x u =
            chapter8UnitPow (x - 2) u * ((1 - u : ℝ) : ℂ) ^ 2 /
              (1 - chapter8UnitPow x u)) ∧
      IntervalIntegrable (chapter8Entry12Kernel x) volume 0 1 ∧
      (∫ u in (0 : ℝ)..1, chapter8Entry12Kernel x u) =
        chapter8Phi x - 1

Sources

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

Uses 2

Proof usesExponential and principal powers agree for positive bases (Chapter 8, Entry 12) · Ramanujan's integral for \(\varphi(x) - 1\) with principal powers (Chapter 8, Entry 12)

TheoremDigamma as the logarithmic derivative of Gamma (used for Chapter 8, Entry 8)#✓fully proved

For every complex number \(z\), \(\Gamma'(z)/\Gamma(z) = \psi(z)\), where \(\psi\) is the digamma function.

At the poles \(z = 0, -1, -2, \dots\) the conventions \(\Gamma(z) = 0\) and division by zero giving \(0\) make both sides \(0\), so the identity holds for every \(z\).

theorem chapter8Digamma_eq_Complex_digamma (z : ℂ) :
    chapter8Digamma z = Complex.digamma z

Used by 1

Used byRamanujan's alternating digamma series (Chapter 8, Entry 8)

TheoremAlternating series \(\sum_{k \ge 1} (-1)^{k-1}/(a + kb)\) via the digamma function#✓fully proved

Let \(a\) and \(b\) be complex numbers with \(b \ne 0\) and \(a + kb \ne 0\) for every integer \(k \ge 1\), and let \(\psi\) be the digamma function, the logarithmic derivative of \(\Gamma\). Then the partial sums of \(\sum_{k=1}^{\infty} \frac{(-1)^{k-1}}{a + kb}\) converge to

\[\frac{1}{2b} \left(\psi\left(\frac{a+2b}{2b}\right) - \psi\left(\frac{a+b}{2b}\right)\right).\]

theorem ramanujan_part1_ch8_entry8_digammaseries_complex_digamma
    (a b : ℂ) (hb : b ≠ 0)
    (hdenom : ∀ j : ℕ, a + b * ((j + 1 : ℕ) : ℂ) ≠ 0) :
    HasSum (chapter8Entry8Term a b)
      ((Complex.digamma ((a + 2 * b) / (2 * b)) -
          Complex.digamma ((a + b) / (2 * b))) /
        (2 * b))
      (SummationFilter.conditional ℕ)

Uses 1 · Used by 1

Proof usesAnalyticity of the digamma function

Used byRamanujan's alternating digamma series (Chapter 8, Entry 8)

TheoremRamanujan's alternating digamma series (Chapter 8, Entry 8)#✓fully proved

Let \(a\) and \(b\) be complex numbers with \(b \ne 0\) and \(a + kb \ne 0\) for every integer \(k \ge 1\), suppose that \(\Gamma\left(\frac{a+2b}{2b}\right) \ne 0\) and \(\Gamma\left(\frac{a+b}{2b}\right) \ne 0\), and let \(\psi(z) = \Gamma'(z)/\Gamma(z)\). Then the partial sums of \(\sum_{k=1}^{\infty} \frac{(-1)^{k-1}}{a + kb}\) converge to

\[\frac{1}{2b} \left(\psi\left(\frac{a+2b}{2b}\right) - \psi\left(\frac{a+b}{2b}\right)\right).\]

Here \(\Gamma\) takes the value \(0\) at its poles \(0, -1, -2, \dots\), so the two conditions on \(\Gamma\) say that these arguments are not poles; they already follow from the condition on \(a + kb\).

theorem ramanujan_part1_ch8_entry8_digammaseries
    (a b : ℂ) (hb : b ≠ 0)
    (hleft : Complex.Gamma ((a + 2 * b) / (2 * b)) ≠ 0)
    (hright : Complex.Gamma ((a + b) / (2 * b)) ≠ 0)
    (hdenom : ∀ j : ℕ, a + b * ((j + 1 : ℕ) : ℂ) ≠ 0) :
    HasSum (chapter8Entry8Term a b)
      ((chapter8Digamma ((a + 2 * b) / (2 * b)) -
          chapter8Digamma ((a + b) / (2 * b))) /
        (2 * b))
      (SummationFilter.conditional ℕ)

Sources

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

Uses 2

Proof usesDigamma as the logarithmic derivative of Gamma (used for Chapter 8, Entry 8) · Alternating series \(\sum_{k \ge 1} (-1)^{k-1}/(a + kb)\) via the digamma function

TheoremDigamma as the logarithmic derivative of Gamma (Chapter 8, Entry 9)#✓fully proved

For every complex number \(z\), \(\Gamma'(z)/\Gamma(z) = \psi(z)\), where \(\Gamma'\) is the complex derivative of the Gamma function and \(\psi\) is the digamma function. At the poles of \(\Gamma\) both sides are \(0\) by convention.

theorem chapter8Digamma_eq_digamma (z : ℂ) :
    chapter8Digamma z = Complex.digamma z

Used by 1

Used byRamanujan's integral for \(\Gamma'/\Gamma\) (Chapter 8, Entry 9)

TheoremThe Entry 9 power function on positive reals (Chapter 8)#✓fully proved

For a complex number \(x\) and a real number \(u\), let \(p_x(u) = e^{x \log\lvert u\rvert}\) if \(u \ne 0\) and \(p_x(0) = 0\). If \(u > 0\), then \(p_x(u) = u^x\), the principal complex power of \(u\).

theorem chapter8UnitPow_eq_cpow (x : ℂ) (u : ℝ) (hu : 0 < u) :
    chapter8UnitPow x u = (u : ℂ) ^ x

TheoremRamanujan's integral for the digamma function (Chapter 8, Entry 9)#✓fully proved

Let \(x\) be a complex number with \(\operatorname{Re} x > 0\), and for real \(u\) write \(u^x = e^{x \log u}\) if \(u > 0\) and \(0^x = 0\). Let \(\psi\) be the digamma function. Then \(x \ne 0\); the function \(u \mapsto u^x/(1 + u^x)\) is integrable on \([0, 1]\); \(1 + u^x \ne 0\) for every \(u \in [0, 1]\); \(\Gamma(1/(2x) + 1) \ne 0\) and \(\Gamma(1/x + 1) \ne 0\); and

\[ \psi\Bigl(\frac{1}{2x} + 1\Bigr) = \psi\Bigl(\frac{1}{x} + 1\Bigr) - \log 2 + x \int_0^1 \frac{u^x}{1 + u^x}\,du. \]

theorem ramanujan_part1_ch8_entry9_qgamma_digamma (x : ℂ) (hx : 0 < x.re) :
    x ≠ 0 ∧
      IntervalIntegrable (chapter8UnitPowRatio x) volume 0 1 ∧
      (∀ u : ℝ, u ∈ Set.Icc 0 1 →
        1 + chapter8UnitPow x u ≠ 0) ∧
      Complex.Gamma (1 / (2 * x) + 1) ≠ 0 ∧
      Complex.Gamma (1 / x + 1) ≠ 0 ∧
      Complex.digamma (1 / (2 * x) + 1) =
        Complex.digamma (1 / x + 1) - (Real.log 2 : ℂ) +
          x * ∫ u in (0 : ℝ)..1, chapter8UnitPowRatio x u

Sources

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

Used by 1

Used byRamanujan's integral for \(\Gamma'/\Gamma\) (Chapter 8, Entry 9)

TheoremRamanujan's integral for \(\Gamma'/\Gamma\) (Chapter 8, Entry 9)#✓fully proved

Let \(x\) be a complex number with \(\operatorname{Re} x > 0\), and for real \(u\) write \(u^x = e^{x \log u}\) if \(u > 0\) and \(0^x = 0\). Write \(\Gamma'\) for the complex derivative of the Gamma function. Then \(x \ne 0\); the function \(u \mapsto u^x/(1 + u^x)\) is integrable on \([0, 1]\); \(1 + u^x \ne 0\) for every \(u \in [0, 1]\); \(\Gamma(1/(2x) + 1) \ne 0\) and \(\Gamma(1/x + 1) \ne 0\); and

\[ \frac{\Gamma'}{\Gamma}\Bigl(\frac{1}{2x} + 1\Bigr) = \frac{\Gamma'}{\Gamma}\Bigl(\frac{1}{x} + 1\Bigr) - \log 2 + x \int_0^1 \frac{u^x}{1 + u^x}\,du. \]

theorem ramanujan_part1_ch8_entry9_qgamma (x : ℂ) (hx : 0 < x.re) :
    x ≠ 0 ∧
      IntervalIntegrable (chapter8UnitPowRatio x) volume 0 1 ∧
      (∀ u : ℝ, u ∈ Set.Icc 0 1 →
        1 + chapter8UnitPow x u ≠ 0) ∧
      Complex.Gamma (1 / (2 * x) + 1) ≠ 0 ∧
      Complex.Gamma (1 / x + 1) ≠ 0 ∧
      chapter8Digamma (1 / (2 * x) + 1) =
        chapter8Digamma (1 / x + 1) - (Real.log 2 : ℂ) +
          x * ∫ u in (0 : ℝ)..1, chapter8UnitPowRatio x u

Sources

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

Uses 2

Proof usesDigamma as the logarithmic derivative of Gamma (Chapter 8, Entry 9) · Ramanujan's integral for the digamma function (Chapter 8, Entry 9)

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.