Revision #1538 → #1846 · back to history
modifiedNontrivial zeros of zeta82057fbbc8c5
| Field | From #1538 | To #1846 |
|---|
| note | The exclusion condition for non-trivial zeros appears inline in `RiemannHypothesis` but is not separately named; `riemannZetaZeros` defines all zeros, not just non-trivial ones. | The exclusion condition for non-trivial zeros appears inline in `RiemannHypothesis` but is not separately named. |
modifiedRecovering primes via Möbius inversion69566f63a68d
| Field | From #1538 | To #1846 |
|---|
| mathlib.decl | Nat.ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq | ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq |
modifiedMertens function41d2575d1ccc
| Field | From #1538 | To #1846 |
|---|
| note | No `Mertens` function exists in Mathlib (`mertens` matches only an unrelated file). | No `Mertens` function exists in Mathlib. |
modifiedLindelöf hypothesis7ed665a4cd6b
| Field | From #1538 | To #1846 |
|---|
| note | The Lindelöf hypothesis is not stated in Mathlib (only unrelated `Lindelöf` topology hits). | The Lindelöf hypothesis is not stated in Mathlib. |
modifiedHardy–Littlewood (1917) on Chebyshev's bias under GRH6305ac95d9ed
| Field | From #1538 | To #1846 |
|---|
| anchors | [{"section":"Consequences of the generalized Riemann hypothesis","snippet":"In 1917, Hardy and Littlewood showed that the generalized Riemann hypothesis implies a conjecture of Chebyshev"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{x\\to 1^{-}}\\sum _{p>2}(-1)^{(p+1)/2}x^{p}=+\\infty ,}"}] | — |
modifiedNicolas inequality on Euler's totienta28ea310d424
| Field | From #1538 | To #1846 |
|---|
| anchors | [{"section":"Growth of Euler's totient","snippet":"In 1983 J. L. Nicolas proved that"},{"type":"math_alttext","value":"{\\displaystyle \\varphi (n)<e^{-\\gamma }{\\frac {n}{\\log \\log n}}}"}] | — |
modifiedKeating–Snaith moments conjectureff1c1243a4e5
| Field | From #1538 | To #1846 |
|---|
| anchors | [{"section":"Random matrix theory and quantum chaos","snippet":"Jonathan Keating and Nina Snaith used averages over random unitary matrices"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {1}{T}}\\int _{0}^{T}|\\zeta (1/2+it)|^{2k}\\,dt}"}] | — |
addedGeneralized Riemann hypothesis (Dirichlet L-functions)13debb4666ce
addedExtended Riemann hypothesis (Dedekind zeta)795f406a1f74
addedGrand Riemann hypothesisa3bdf144888d
addedHilbert–Pólya conjecture94de9c72bcc3
addedLee–Yang theoremf79b421e7b81
addedLiouville function9fbe65612f8a
addedTurán's conditional RH criterion via finite Dirichlet sumsea6df7abb658
addedHaselgrove: T(x) is negative infinitely often (Pólya conjecture disproof)2ae53b4e6848
addedde Branges Hilbert-space positivity approachfca628ce807e
addedQuasicrystal property of zeta zeros under RH5501645e18b8
addedConnes' Selberg-trace-formula approach to RH247cb25ad94f
addedSkewes' number8aa9a98b4856
addedOdlyzko: zeros of zeta match GUE eigenvalue statisticsa2d1e73554e8