Fungrim home page

Fungrim entry: 3a5eb6

ζ ⁣(s)<31+s1s1+s2π(1+ηRe(s))/2ζ ⁣(1+η)\left|\zeta\!\left(s\right)\right| < 3 \left|\frac{1 + s}{1 - s}\right| {\left|\frac{1 + s}{2 \pi}\right|}^{\left( 1 + \eta - \operatorname{Re}(s) \right) / 2} \zeta\!\left(1 + \eta\right)
Assumptions:sC  and  ηR  and  s1  and  η(0,12]  and  ηRe(s)1+ηs \in \mathbb{C} \;\mathbin{\operatorname{and}}\; \eta \in \mathbb{R} \;\mathbin{\operatorname{and}}\; s \ne 1 \;\mathbin{\operatorname{and}}\; \eta \in \left(0, \frac{1}{2}\right] \;\mathbin{\operatorname{and}}\; -\eta \le \operatorname{Re}(s) \le 1 + \eta
  • H. Rademacher, Topics in analytic number theory, Springer, 1973. Equation 43.3.
\left|\zeta\!\left(s\right)\right| < 3 \left|\frac{1 + s}{1 - s}\right| {\left|\frac{1 + s}{2 \pi}\right|}^{\left( 1 + \eta - \operatorname{Re}(s) \right) / 2} \zeta\!\left(1 + \eta\right)

s \in \mathbb{C} \;\mathbin{\operatorname{and}}\; \eta \in \mathbb{R} \;\mathbin{\operatorname{and}}\; s \ne 1 \;\mathbin{\operatorname{and}}\; \eta \in \left(0, \frac{1}{2}\right] \;\mathbin{\operatorname{and}}\; -\eta \le \operatorname{Re}(s) \le 1 + \eta
Fungrim symbol Notation Short description
Absz\left|z\right| Absolute value
RiemannZetaζ ⁣(s)\zeta\!\left(s\right) Riemann zeta function
Powab{a}^{b} Power
Piπ\pi The constant pi (3.14...)
ReRe(z)\operatorname{Re}(z) Real part
CCC\mathbb{C} Complex numbers
RRR\mathbb{R} Real numbers
OpenClosedInterval(a,b]\left(a, b\right] Open-closed interval
Source code for this entry:
    Formula(Less(Abs(RiemannZeta(s)), Mul(Mul(Mul(3, Abs(Div(Add(1, s), Sub(1, s)))), Pow(Abs(Div(Add(1, s), Mul(2, Pi))), Div(Sub(Add(1, eta), Re(s)), 2))), RiemannZeta(Add(1, eta))))),
    Variables(s, eta),
    Assumptions(And(Element(s, CC), Element(eta, RR), NotEqual(s, 1), Element(eta, OpenClosedInterval(0, Div(1, 2))), LessEqual(Neg(eta), Re(s), Add(1, eta)))),
    References("H. Rademacher, Topics in analytic number theory, Springer, 1973. Equation 43.3."))

Topics using this entry

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2021-03-15 19:12:00.328586 UTC