Fungrim entry: 351d87

\left|\operatorname{sinc}(x)\right| < \frac{\sqrt{2}}{x} \tanh\!\left(\frac{x}{\sqrt{2}}\right)

Assumptions:

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; x \ne 0

TeX:

\left|\operatorname{sinc}(x)\right| < \frac{\sqrt{2}}{x} \tanh\!\left(\frac{x}{\sqrt{2}}\right)

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; x \ne 0

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Sinc`	$\operatorname{sinc}(z)$	Sinc function
`Sqrt`	$\sqrt{z}$	Principal square root
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("351d87"),
    Formula(Less(Abs(Sinc(x)), Mul(Div(Sqrt(2), x), Tanh(Div(x, Sqrt(2)))))),
    Variables(x),
    Assumptions(And(Element(x, RR), NotEqual(x, 0))))

Topics using this entry

Sinc 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