Library Stdlib.Reals.Rtrigo_facts


From Stdlib Require Import Rbase.
From Stdlib Require Import Rtrigo1.
From Stdlib Require Import Rfunctions.

From Stdlib Require Import Lra.
From Stdlib Require Import Ranalysis_reg.

Local Open Scope R_scope.

Bounds of expressions with trigonometric functions


Lemma sin2_bound : forall x,
  0 <= (sin x)² <= 1.

Lemma cos2_bound : forall x,
  0 <= (cos x)² <= 1.

Express trigonometric functions with each other

Express sin and cos with each other


Lemma cos_sin : forall x, cos x >=0 ->
  cos x = sqrt(1 - (sin x)²).

Lemma cos_sin_opp : forall x, cos x <=0 ->
  cos x = - sqrt(1 - (sin x)²).

Lemma cos_sin_Rabs : forall x,
  Rabs (cos x) = sqrt(1 - (sin x)²).

Lemma sin_cos : forall x, sin x >=0 ->
  sin x = sqrt(1 - (cos x)²).

Lemma sin_cos_opp : forall x, sin x <=0 ->
  sin x = - sqrt(1 - (cos x)²).

Lemma sin_cos_Rabs : forall x,
  Rabs (sin x) = sqrt(1 - (cos x)²).

Express tan with sin and cos


Lemma tan_sin : forall x, 0 <= cos x ->
  tan x = sin x / sqrt (1 - (sin x)²).

Lemma tan_sin_opp : forall x, 0 > cos x ->
  tan x = - (sin x / sqrt (1 - (sin x)²)).

Note: tan_sin_Rabs wouldn't make a lot of sense, because one would need Rabs on both sides

Lemma tan_cos : forall x, 0 <= sin x ->
  tan x = sqrt (1 - (cos x)²) / cos x.

Lemma tan_cos_opp : forall x, 0 >= sin x ->
  tan x = - sqrt (1 - (cos x)²) / cos x.

Express sin and cos with tan


Lemma sin_tan : forall x, 0 < cos x ->
  sin x = tan x / sqrt (1 + (tan x)²).

Lemma cos_tan : forall x, 0 < cos x ->
  cos x = 1 / sqrt (1 + (tan x)²).

Additional shift lemmas for sin, cos, tan


Lemma sin_pi_minus : forall x,
  sin (PI - x) = sin x.

Lemma sin_pi_plus : forall x,
  sin (PI + x) = - sin x.

Lemma cos_pi_minus : forall x,
  cos (PI - x) = - cos x.

Lemma cos_pi_plus : forall x,
  cos (PI + x) = - cos x.

Lemma tan_pi_minus : forall x, cos x <> 0 ->
  tan (PI - x) = - tan x.

Lemma tan_pi_plus : forall x, cos x <> 0 ->
  tan (PI + x) = tan x.