Digamma and trigamma functions
Digamma and trigamma series on the reals
TheoremSummability of the Basel series#✓fully proved
The series of real numbers \(\sum_{j \ge 0} \frac{1}{(j+1)^2}\) is summable.
theorem summable_one_div_add_nat_succ_sq : Summable (fun j : ℕ => 1 / ((j : ℝ) + 1) ^ 2)TheoremDigamma series on the positive reals#✓fully proved
For every real \(x > 0\), the series \(\sum_{j=0}^{\infty} \left(\frac{1}{j+1} - \frac{1}{x+j+1}\right)\) has sum \(\psi(x+1) + \gamma\), where \(\psi = (\log \Gamma)'\) with \(\Gamma\) the real Gamma function, and \(\gamma\) is the Euler–Mascheroni constant.
theorem hasSum_digamma_series (x : ℝ) (hx : 0 < x) :
HasSum (fun j : ℕ => 1 / ((j : ℝ) + 1) - 1 / (x + (j : ℝ) + 1))
(deriv (fun t => Real.log (Real.Gamma t)) (x + 1)
+ Real.eulerMascheroniConstant)TheoremDerivative of the digamma series#✓fully proved
For every real \(y > 0\), the real function \(z \mapsto \sum_{j=0}^{\infty} \left(\frac{1}{j+1} - \frac{1}{z+j+1}\right)\) is differentiable at \(y\) with derivative \(\sum_{j=0}^{\infty} \frac{1}{(y+j+1)^2}\).
theorem hasDerivAt_tsum_digamma_series (y : ℝ) (hy : 0 < y) :
HasDerivAt (fun z => ∑' j : ℕ, (1 / ((j : ℝ) + 1) - 1 / (z + (j : ℝ) + 1)))
(∑' j : ℕ, 1 / (y + (j : ℝ) + 1) ^ 2) yUses 1 · Used by 2
TheoremTrigamma series#✓fully proved
For every real \(y > 0\), the second derivative of \(\log \Gamma\) at \(y + 1\) equals \(\sum_{j=0}^{\infty} \frac{1}{(y + j + 1)^2}\), where \(\Gamma\) is the real Gamma function.
theorem deriv_deriv_log_Gamma_add_one (y : ℝ) (hy : 0 < y) :
deriv (deriv (fun t => Real.log (Real.Gamma t))) (y + 1)
= ∑' j : ℕ, 1 / (y + (j : ℝ) + 1) ^ 2Uses 2
TheoremLogarithmic derivative of the real Gamma function#✓fully proved
For every real \(u > 0\), the derivative of \(\log \Gamma\) at \(u\) equals \(\Gamma'(u) / \Gamma(u)\), where \(\Gamma\) is the real Gamma function.
theorem deriv_log_Gamma (u : ℝ) (hu : 0 < u) :
deriv (fun t => Real.log (Real.Gamma t)) u
= deriv Real.Gamma u / Real.Gamma uAnalyticity and the complex digamma series
TheoremAnalyticity of the Gamma function#✓fully proved
The complex Gamma function is analytic at every \(w \in \mathbb{C}\) that is not a nonpositive integer.
theorem analyticAt_Gamma (w : ℂ) (hw : ∀ m : ℕ, w ≠ -((m : ℕ) : ℂ)) :
AnalyticAt ℂ Complex.Gamma wTheoremAnalyticity of the digamma function#✓fully proved
The digamma function \(\psi = \Gamma'/\Gamma\), where \(\Gamma\) is the complex Gamma function, is complex analytic at every \(w \in \mathbb{C}\) that is not a nonpositive integer.
theorem analyticAt_digamma (w : ℂ) (hw : ∀ m : ℕ, w ≠ -((m : ℕ) : ℂ)) :
AnalyticAt ℂ Complex.digamma wTheoremComplex and real derivatives of Gamma agree on the positive reals#✓fully proved
For every real \(t > 0\), the derivative of the complex Gamma function at \(t\) equals the derivative of the real Gamma function at \(t\).
theorem deriv_Gamma_ofReal (t : ℝ) (ht : 0 < t) :
deriv Complex.Gamma (↑t) = ↑(deriv Real.Gamma t)TheoremAbsolute convergence of the trigamma series#✓fully proved
For every complex number \(z\), the series \(\sum_{k \ge 0} \frac{1}{(z + k + 1)^2}\) converges absolutely, that is, the series of absolute values \(\sum_{k \ge 0} \left|\frac{1}{(z + k + 1)^2}\right|\) is summable, where a term whose denominator vanishes is read as \(0\).
Because of this convention no hypothesis excluding the poles \(z = -(k + 1)\) is needed.
theorem summable_norm_one_div_add_nat_succ_sq (z : ℂ) :
Summable (fun k : ℕ => ‖(1 / (z + (k + 1 : ℕ)) ^ 2 : ℂ)‖)Used by 1
DefinitionTerms of the complex digamma series#✓fully proved
For \(j \in \mathbb{N}\) and \(s \in \mathbb{C}\), the \(j\)-th term of the complex digamma series at \(s\) is \(\frac{1}{j+1} - \frac{1}{j+s}\), where \(1/0\) is read as \(0\).
def digammaSeriesTerm (j : ℕ) (s : ℂ) : ℂ :=
1 / ((j : ℂ) + 1) - 1 / ((j : ℂ) + s)DefinitionComplex digamma series#✓fully proved
For \(s \in \mathbb{C}\), the digamma series function at \(s\) is \(\sum_{j=0}^{\infty} \left(\frac{1}{j+1} - \frac{1}{j+s}\right)\), the sum of the terms of the complex digamma series at \(s\).
The value is taken to be \(0\) when the series is not summable, and a term with \(j + s = 0\) uses \(1/0 = 0\).
def digammaSeriesFun (s : ℂ) : ℂ := ∑' j : ℕ, digammaSeriesTerm j sdef digammaSeriesTerm (j : ℕ) (s : ℂ) : ℂ :=
1 / ((j : ℂ) + 1) - 1 / ((j : ℂ) + s)MathlibExt/Analysis/SpecialFunctions/Gamma/Digamma.lean:738
Uses 1 · Used by 2
TheoremSummability of the digamma series terms#✓fully proved
For every complex number \(s\) with \(\operatorname{Re} s > 1\), the sequence of digamma series terms \(\frac{1}{j+1} - \frac{1}{j+s}\), for \(j = 0, 1, 2, \dots\), is summable.
theorem summable_digammaSeriesTerm (s : ℂ) (hs : 1 < s.re) :
Summable (fun j : ℕ => digammaSeriesTerm j s)def digammaSeriesTerm (j : ℕ) (s : ℂ) : ℂ :=
1 / ((j : ℂ) + 1) - 1 / ((j : ℂ) + s)MathlibExt/Analysis/SpecialFunctions/Gamma/Digamma.lean:738
Uses 2 · Used by 1
TheoremSeries expansion of the complex digamma function#✓fully proved
For every complex number \(s\) with \(\operatorname{Re} s > 1\), the series \(\sum_{j=0}^{\infty} \left(\frac{1}{j+1} - \frac{1}{j+s}\right)\) of the terms of the complex digamma series at \(s\) has sum \(\psi(s) + \gamma\), where \(\psi = \Gamma'/\Gamma\) is the complex digamma function, the logarithmic derivative of the complex Gamma function, and \(\gamma\) is the Euler–Mascheroni constant.
theorem hasSum_digamma_series (s : ℂ) (hs : 1 < s.re) :
HasSum (fun j : ℕ => digammaSeriesTerm j s)
(Complex.digamma s + (Real.eulerMascheroniConstant : ℂ))def digammaSeriesTerm (j : ℕ) (s : ℂ) : ℂ :=
1 / ((j : ℂ) + 1) - 1 / ((j : ℂ) + s)MathlibExt/Analysis/SpecialFunctions/Gamma/Digamma.lean:738
Uses 8 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.