Assumptions:
TeX:
\left|J_{n}\!\left(z\right)\right| \le \exp\!\left(\left|\operatorname{Im}\!\left(z\right)\right|\right)
n \in \mathbb{Z} \,\mathbin{\operatorname{and}}\, z \in \mathbb{C}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Abs | Absolute value | |
| BesselJ | Bessel function of the first kind | |
| Exp | Exponential function | |
| Im | Imaginary part | |
| ZZ | Integers | |
| CC | Complex numbers |
Source code for this entry:
Entry(ID("0836b4"),
Formula(LessEqual(Abs(BesselJ(n, z)), Exp(Abs(Im(z))))),
Variables(n, z),
Assumptions(And(Element(n, ZZ), Element(z, CC))))