Assumptions:
TeX:
\left|P_{n}\!\left(x\right)\right| \le 1
n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; -1 \le x \le 1Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Abs | Absolute value | |
| LegendrePolynomial | Legendre polynomial | |
| ZZGreaterEqual | Integers greater than or equal to n |
Source code for this entry:
Entry(ID("1ba9a5"),
Formula(LessEqual(Abs(LegendrePolynomial(n, x)), 1)),
Variables(n, x),
Assumptions(And(Element(n, ZZGreaterEqual(0)), LessEqual(-1, x, 1))))