Fungrim entry: 809bc0

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

Assumptions:

s \in \mathbb{C} \;\mathbin{\operatorname{and}}\; \operatorname{Re}(s) > 1

TeX:

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

s \in \mathbb{C} \;\mathbin{\operatorname{and}}\; \operatorname{Re}(s) > 1

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`RiemannZeta`	$\zeta\!\left(s\right)$	Riemann zeta function
`Re`	$\operatorname{Re}(z)$	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.

2021-03-15 19:12:00.328586 UTC