20.3. Special values and identities🔗

open Real
variable {x : ℝ}

Many basic facts about the trigonometric functions are also known, including special values such as:

example :
    sin (π / 4) = √2 / 2 :=
  sin_pi_div_four

example :
    cos (π / 3) = 1 / 2 :=
  cos_pi_div_three

example :
    cos (π / 5) = (1 + √5) / 4 :=
  cos_pi_div_five

example :
    cos (π / 8) = √(2 + √2) / 2 :=
  cos_pi_div_eight

example :
    tan (π / 4) = 1 :=
  tan_pi_div_four

example :
    tan (π / 6) = 1 / √3 :=
  tan_pi_div_six

and identities such as:

example :
    cos (2 * x) = 2 * cos x ^ 2 - 1 :=
  cos_two_mul x

example :
    sin (2 * x) = 2 * sin x * cos x :=
  sin_two_mul x

example :
    cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x :=
  cosh_three_mul x

and bounds such as:

example (hx : |x| ≤ 1) :
    |cos x - (1 - x ^ 2 / 2)| ≤ |x| ^ 4 * (5 / 96) :=
  cos_bound hx

example (hx : |x| ≤ 1) :
    |sin x - (x - x ^ 3 / 6)| ≤ |x| ^ 4 * (5 / 96) :=
  sin_bound hx