Library Coq.Reals.Rtrigo_alt
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
SeqSeries
.
Require
Import
Rtrigo_def
.
Local
Open
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
.
Theorem
pre_sin_bound
:
forall
(
a
:
R
) (
n
:
nat
),
0
<=
a
->
a
<=
4 ->
sin_approx
a
(2
*
n
+
1)
<=
sin
a
<=
sin_approx
a
(2
*
(
n
+
1
)
).
Lemma
pre_cos_bound
:
forall
(
a
:
R
) (
n
:
nat
),
- 2
<=
a
->
a
<=
2 ->
cos_approx
a
(2
*
n
+
1)
<=
cos
a
<=
cos_approx
a
(2
*
(
n
+
1
)
).