Fungrim entry: 65fa9f

\left(\operatorname{RH}\right) \iff \left(\log\!\left(g(n)\right) < \sqrt{f(n)} \;\text{ for all } n \in \mathbb{Z}_{\ge 1}\; \text{ where } f(y) = \mathop{\operatorname{solution*}\,}\limits_{x \in \left(1, \infty\right)} \left[\operatorname{li}(x) = y\right]\right)

References:

Marc Deleglise, Jean-Louis Nicolas, The Landau function and the Riemann Hypothesis, https://arxiv.org/abs/1907.07664

TeX:

\left(\operatorname{RH}\right) \iff \left(\log\!\left(g(n)\right) < \sqrt{f(n)} \;\text{ for all } n \in \mathbb{Z}_{\ge 1}\; \text{ where } f(y) = \mathop{\operatorname{solution*}\,}\limits_{x \in \left(1, \infty\right)} \left[\operatorname{li}(x) = y\right]\right)

Definitions:

Fungrim symbol	Notation	Short description
`RiemannHypothesis`	$\operatorname{RH}$	Riemann hypothesis
`Log`	$\log(z)$	Natural logarithm
`LandauG`	$g(n)$	Landau's function
`Sqrt`	$\sqrt{z}$	Principal square root
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`UniqueSolution`	$\mathop{\operatorname{solution*}\,}\limits_{x \in S} Q(x)$	Unique solution
`LogIntegral`	$\operatorname{li}(z)$	Logarithmic integral
`OpenInterval`	$\left(a, b\right)$	Open interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("65fa9f"),
    Formula(Equivalent(RiemannHypothesis, Where(All(Less(Log(LandauG(n)), Sqrt(f(n))), ForElement(n, ZZGreaterEqual(1))), Equal(f(y), UniqueSolution(Brackets(Equal(LogIntegral(x), y)), ForElement(x, OpenInterval(1, Infinity))))))),
    References("Marc Deleglise, Jean-Louis Nicolas, The Landau function and the Riemann Hypothesis, https://arxiv.org/abs/1907.07664"))

Fungrim entry: 65fa9f

Topics using this entry