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:

• sin_lt: for x > 0 we have sin x < x.
• sin_gt_sub_cube: For 0 < x ≤ 1 we have x - x ^ 3 / 4 < sin x.
• lt_tan: for 0 < x < π/2 we have x < tan x.
• cos_le_one_div_sqrt_sq_add_one and cos_lt_one_div_sqrt_sq_add_one: for -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)

Tags

sin, cos, tan, angle

theorem Real.sin_lt {x : ℝ} (h : 0 < x) : sin x < x

For 0 < x, we have sin x < x.

theorem Real.sin_le {x : ℝ} (hx : 0 ≤ x) : sin x ≤ x

theorem Real.lt_sin {x : ℝ} (hx : x < 0) : x < sin x

theorem Real.le_sin {x : ℝ} (hx : x ≤ 0) : x ≤ sin x

theorem Real.lt_sin_mul {x : ℝ} (hx : 0 < x) (hx' : x < 1) : x < sin (Real.pi / 2 * x)

theorem Real.le_sin_mul {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 1) : x ≤ sin (Real.pi / 2 * x)

theorem Real.mul_lt_sin {x : ℝ} (hx : 0 < x) (hx' : x < Real.pi / 2) : 2 / Real.pi * x < sin x

theorem Real.mul_le_sin {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ Real.pi / 2) : 2 / Real.pi * x ≤ sin x

One half of Jordan's inequality.

In the range [0, π / 2], we have a linear lower bound on sin. The other half is given by Real.sin_le.

theorem Real.sin_le_mul {x : ℝ} (hx : -(Real.pi / 2) ≤ x) (hx₀ : x ≤ 0) : sin x ≤ 2 / Real.pi * x

Half of Jordan's inequality for negative values.

theorem Real.mul_abs_le_abs_sin {x : ℝ} (hx : |x| ≤ Real.pi / 2) : 2 / Real.pi * |x| ≤ |sin x|

Half of Jordan's inequality for absolute values.

theorem Real.sin_sq_lt_sq {x : ℝ} (hx : x ≠ 0) : sin x ^ 2 < x ^ 2

theorem Real.sin_sq_le_sq {x : ℝ} : sin x ^ 2 ≤ x ^ 2

theorem Real.abs_sin_lt_abs {x : ℝ} (hx : x ≠ 0) : |sin x| < |x|

theorem Real.abs_sin_le_abs {x : ℝ} : |sin x| ≤ |x|

theorem Real.one_sub_sq_div_two_lt_cos {x : ℝ} (hx : x ≠ 0) : 1 - x ^ 2 / 2 < cos x

theorem Real.one_sub_sq_div_two_le_cos {x : ℝ} : 1 - x ^ 2 / 2 ≤ cos x

theorem Real.one_sub_mul_le_cos {x : ℝ} (hx₀ : 0 ≤ x) (hx : x ≤ Real.pi / 2) : 1 - 2 / Real.pi * x ≤ cos x

Half of Jordan's inequality for cos.

theorem Real.one_add_mul_le_cos {x : ℝ} (hx₀ : -(Real.pi / 2) ≤ x) (hx : x ≤ 0) : 1 + 2 / Real.pi * x ≤ cos x

Half of Jordan's inequality for cos and negative values.

theorem Real.cos_le_one_sub_mul_cos_sq {x : ℝ} (hx : |x| ≤ Real.pi) : cos x ≤ 1 - 2 / Real.pi ^ 2 * x ^ 2

theorem Real.sin_gt_sub_cube {x : ℝ} (h : 0 < x) (h' : x ≤ 1) : x - x ^ 3 / 4 < sin x

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.

theorem Real.deriv_tan_sub_id (x : ℝ) (h : cos x ≠ 0) : deriv (fun (y : ℝ) => tan y - y) x = 1 / cos x ^ 2 - 1

The derivative of tan x - x is 1/(cos x)^2 - 1 away from the zeroes of cos.

theorem Real.lt_tan {x : ℝ} (h1 : 0 < x) (h2 : x < Real.pi / 2) : x < tan x

For all 0 < x < π/2 we have x < tan x.

This is proved by checking that the function tan x - x vanishes at zero and has non-negative derivative.

theorem Real.le_tan {x : ℝ} (h1 : 0 ≤ x) (h2 : x < Real.pi / 2) : x ≤ tan x

theorem Real.cos_lt_one_div_sqrt_sq_add_one {x : ℝ} (hx1 : -(3 * Real.pi / 2) ≤ x) (hx2 : x ≤ 3 * Real.pi / 2) (hx3 : x ≠ 0) : cos x < 1 / √(x ^ 2 + 1)

theorem Real.cos_le_one_div_sqrt_sq_add_one {x : ℝ} (hx1 : -(3 * Real.pi / 2) ≤ x) (hx2 : x ≤ 3 * Real.pi / 2) : cos x ≤ 1 / √(x ^ 2 + 1)

theorem Real.lipschitzWith_sin : LipschitzWith 1 sin

theorem Real.lipschitzWith_cos : LipschitzWith 1 cos

theorem Real.abs_sin_sub_sin_le (x y : ℝ) : |sin x - sin y| ≤ |x - y|

theorem Real.abs_cos_sub_cos_le (x y : ℝ) : |cos x - cos y| ≤ |x - y|

theorem Real.norm_exp_I_mul_ofReal_sub_one_le {x : ℝ} : ‖Complex.exp (Complex.I * ↑x) - 1‖ ≤ ‖x‖

theorem Real.enorm_exp_I_mul_ofReal_sub_one_le {x : ℝ} : ‖Complex.exp (Complex.I * ↑x) - 1‖ₑ ≤ ‖x‖ₑ

theorem Real.nnnorm_exp_I_mul_ofReal_sub_one_le {x : ℝ} : ‖Complex.exp (Complex.I * ↑x) - 1‖₊ ≤ ‖x‖₊