TeX:
\left(\operatorname{RH}\right) \iff \left(\sigma_{1}\!\left(n\right) < {e}^{\gamma} n \log\!\left(\log(n)\right) \;\text{ for all } n \in \mathbb{Z}_{\ge 5041}\right)Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| RiemannHypothesis | Riemann hypothesis | |
| DivisorSigma | Sum of divisors function | |
| Exp | Exponential function | |
| ConstGamma | The constant gamma (0.577...) | |
| Log | Natural logarithm | |
| ZZGreaterEqual | Integers greater than or equal to n |
Source code for this entry:
Entry(ID("3142ec"),
Formula(Equivalent(RiemannHypothesis, All(Less(DivisorSigma(1, n), Mul(Mul(Exp(ConstGamma), n), Log(Log(n)))), ForElement(n, ZZGreaterEqual(5041))))))