Fungrim entry: 809bc0

\left|\zeta\!\left(s\right)\right| \le \zeta\!\left(\operatorname{Re}\!\left(s\right)\right)

Assumptions:

s \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \operatorname{Re}\!\left(s\right) \gt 1

TeX:

\left|\zeta\!\left(s\right)\right| \le \zeta\!\left(\operatorname{Re}\!\left(s\right)\right)

s \in \mathbb{C} \,\mathbin{\operatorname{and}}\, \operatorname{Re}\!\left(s\right) \gt 1

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`RiemannZeta`	$\zeta\!\left(s\right)$	Riemann zeta function
`Re`	$\operatorname{Re}\!\left(z\right)$	Real part
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("809bc0"),
    Formula(LessEqual(Abs(RiemannZeta(s)), RiemannZeta(Re(s)))),
    Variables(s),
    Assumptions(And(Element(s, CC), Greater(Re(s), 1))))

Topics using this entry

Riemann zeta function

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

2019-06-18 07:49:59.356594 UTC