Library Coq.Reals.Rtrigo_alt
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
SeqSeries
.
Require
Import
Rtrigo_def
.
Open
Local
Scope
R_scope
.
Using series definitions of cos and sin
Definition
sin_term
(
a
:R) (
i
:nat) :
R
:=
(-1) ^
i
* (
a
^ (2 *
i
+ 1) /
INR
(
fact
(2 *
i
+ 1))).
Definition
cos_term
(
a
:R) (
i
:nat) :
R
:=
(-1) ^
i
* (
a
^ (2 *
i
) /
INR
(
fact
(2 *
i
))).
Definition
sin_approx
(
a
:R) (
n
:nat) :
R
:=
sum_f_R0
(
sin_term
a
)
n
.
Definition
cos_approx
(
a
:R) (
n
:nat) :
R
:=
sum_f_R0
(
cos_term
a
)
n
.
Lemma
PI_4
:
PI
<= 4.
Theorem
sin_bound
:
forall
(
a
:R) (
n
:nat),
0 <=
a
->
a
<=
PI
->
sin_approx
a
(2 *
n
+ 1) <=
sin
a
<=
sin_approx
a
(2 * (
n
+ 1)).
Lemma
cos_bound
:
forall
(
a
:R) (
n
:nat),
-
PI
/ 2 <=
a
->
a
<=
PI
/ 2 ->
cos_approx
a
(2 *
n
+ 1) <=
cos
a
<=
cos_approx
a
(2 * (
n
+ 1)).