Assumptions:
TeX:
{2 n \choose n} \lt \frac{{4}^{n}}{\sqrt{\pi n}}
n \in \mathbb{Z}_{\ge 1}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Binomial | Binomial coefficient | |
| Pow | Power | |
| Sqrt | Principal square root | |
| ConstPi | The constant pi (3.14...) | |
| ZZGreaterEqual | Integers greater than or equal to n |
Source code for this entry:
Entry(ID("433d8b"),
Formula(Less(Binomial(Mul(2, n), n), Div(Pow(4, n), Sqrt(Mul(ConstPi, n))))),
Variables(n),
Assumptions(Element(n, ZZGreaterEqual(1))))