Revision #1202 → #1820 · back to history
addedIrrationality of γba27e042d7d2
addedTranscendence degree at least twoa9c22b922a53
modifiedShidlovsky: γ or Gompertz constant is irrationala26b73c58ba8
| Field | From #1202 | To #1820 |
|---|
| note | Mathlib has no Gompertz constant nor Shidlovsky's joint irrationality result. | Mathlib has no Gompertz constant nor Shidlovsky's joint irrationality result (loogle for `Gompertz` returns nothing). |
modifiedMurty–Saradha on Euler–Lehmer constantsdbd9bcdf8e50
| Field | From #1202 | To #1820 |
|---|
| anchors | [{"section":"Irrationality and transcendence","snippet":"M. Ram Murty and N. Saradha showed that at most one of the Euler-Lehmer constants"},{"type":"math_alttext","value":"{\\displaystyle \\gamma (a,q)=\\lim _{n\\rightarrow \\infty }\\left(\\sum _{k=0}^{n}{\\frac {1}{a+kq}}-{\\frac {\\log {(a+nq})}{q}}\\right)}"}] | — |
modifiedMurty–Zaytseva on generalized Euler constants3ad104d34f0f
| Field | From #1202 | To #1820 |
|---|
| anchors | [{"section":"Irrationality and transcendence","snippet":"M. Ram Murty and A. Zaytseva showed that the generalized Euler constants have the same property"},{"type":"math_alttext","value":"{\\displaystyle \\gamma (\\Omega )=\\lim _{x\\rightarrow \\infty }\\left(\\sum _{n=1}^{x}{\\frac {1_{\\Omega }(n)}{n}}-\\log x\\cdot \\lim _{x\\rightarrow \\infty }{\\frac {\\sum _{n=1}^{x}1_{\\Omega }(n)}{x}}\\right),}"}] | — |
addedKhinchin's constant for γ continued fraction090cac8f55b6
addedBeta-function limit for γ86eb2d1e4cfe
modifiedγ via reciprocals of non-trivial zeros32a7b43e98ce
| Field | From #1202 | To #1820 |
|---|
| anchors | [{"section":"Relation to the zeta function","snippet":"can also be expressed in terms of the sum of the reciprocals of non-trivial zeros"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\gamma &=\\sum _{m=2}^{\\infty }(-1)^{m}{\\frac {\\zeta (m)}{m}}\\\\&=\\log {\\frac {4}{\\pi }}+\\sum _{m=2}^{\\infty }(-1)^{m}{\\frac {\\zeta (m)}{2^{m-1}m}}.\\end{aligned}}}"}] | — |
addedDeTemple faster convergence at α=1/268e91d70318b
modifiedEuler's infinite series for γ3b9310354d68
| Field | From #1202 | To #1820 |
|---|
| anchors | [{"section":"Series expansions","snippet":"Euler showed that the following infinite series approaches γ"},{"type":"math_alttext","value":"{\\displaystyle \\gamma =\\sum _{k=1}^{\\infty }\\left({\\frac {1}{k}}-\\log \\left(1+{\\frac {1}{k}}\\right)\\right).}"}] | — |
| note | Euler's original series for γ involving ζ(k) is not formalized. | Euler's original series ∑(1/k - log(1+1/k)) = γ is not formalized. |
modifiede^γ as prime limit (Mertens)3c1984178b03
| Field | From #1202 | To #1820 |
|---|
| note | Mertens' third theorem expressing e^γ as a limit over primes is not in Mathlib. | Mertens' third theorem expressing e^γ as a limit over primes is not in Mathlib (loogle for `mertens` returns nothing). |
modifiedStieltjes constants710f75e93003
| Field | From #1202 | To #1820 |
|---|
| note | Stieltjes constants γ_n are not defined in Mathlib. | Stieltjes constants γ_n are not defined in Mathlib (only `StieltjesFunction`/measure theory hits exist). |