Polynomial bounds for trigonometric functions #
Main statements #
This file contains upper and lower bounds for real trigonometric functions in terms
of polynomials. See
trigonometric.basic for more elementary inequalities, establishing
the ranges of these functions, and their monotonicity in suitable intervals.
Here we prove the following:
x > 0we have
sin x < x.
0 < x ≤ 1we have
x - x ^ 3 / 4 < sin x.
0 < x < π/2we have
x < tan x.
-3 * π / 2 ≤ x ≤ 3 * π / 2, we have
cos x ≤ 1 / sqrt (x ^ 2 + 1), with strict inequality if
x ≠ 0. (This bound is not quite optimal, but not far off)
sin, cos, tan, angle
For 0 < x ≤ 1 we have x - x ^ 3 / 4 < sin x.
This is also true for x > 1, but it's nontrivial for x just above 1. This inequality is not tight; the tighter inequality is sin x > x - x ^ 3 / 6 for all x > 0, but this inequality has a simpler proof.