Documentation Verification Report

Digamma

📁 Source: Mathlib/Analysis/SpecialFunctions/Gamma/Digamma.lean

Statistics

Metric	Count
Definitions `digamma`	1
Theorems `digamma_apply_add_one`, `digamma_def`, `digamma_one`, `digamma_one_half`, `digamma_zero`, `meromorphic_digamma`	6
Total	7

Complex

Definitions

Name	Category	Theorems
`digamma` 📖	CompOp	6 math math: `meromorphic_digamma`, `digamma_apply_add_one`, `digamma_one_half`, `digamma_zero`, `digamma_def`, `digamma_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`digamma_apply_add_one` 📖	mathematical	—	`digamma` `Complex` `instAdd` `instOne` `instInv`	—	`CharP.cast_eq_zero` `CharP.ofCharZero` `instCharZero` `neg_zero` `digamma_def` `logDeriv_apply` `deriv_Gamma_add_one` `Gamma_add_one` `add_div` `div_mul_cancel_right₀` `Gamma_ne_zero` `mul_div_mul_left` `add_comm`
`digamma_def` 📖	mathematical	—	`digamma` `logDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `NormedAlgebra.id` `NontriviallyNormedField.toNormedField` `Gamma`	—	—
`digamma_one` 📖	mathematical	—	`digamma` `Complex` `instOne` `instNeg` `ofReal` `Real.eulerMascheroniConstant`	—	`digamma_def` `logDeriv_apply` `HasDerivAt.deriv` `hasDerivAt_Gamma_one` `Gamma_one` `div_one`
`digamma_one_half` 📖	mathematical	—	`digamma` `Complex` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `instSub` `instMul` `instNeg` `log` `ofReal` `Real.eulerMascheroniConstant`	—	`Nat.instAtLeastTwoHAddOfNat` `digamma_def` `logDeriv_apply` `HasDerivAt.deriv` `hasDerivAt_Gamma_one_half` `add_comm` `Gamma_one_half_eq` `neg_mul` `mul_neg` `neg_add'` `Real.sqrt_eq_rpow` `ofReal_cpow` `Real.pi_nonneg` `one_div` `ofReal_inv` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `instCharZero`
`digamma_zero` 📖	mathematical	—	`digamma` `Complex` `instZero`	—	`logDeriv_eq_zero_of_not_differentiableAt` `not_differentiableAt_Gamma_zero`
`meromorphic_digamma` 📖	mathematical	—	`Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `digamma`	—	`Meromorphic.logDeriv` `instCompleteSpace` `Meromorphic.Gamma`

---

← Back to Index