Library Coq.Reals.Cos_rel
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
SeqSeries
.
Require
Import
Rtrigo_def
.
Local
Open
Scope
R_scope
.
Definition
A1
(
x
:
R
) (
N
:
nat
) :
R
:=
sum_f_R0
(
fun
k
:
nat
=>
(
-1
)
^
k
/
INR
(
fact
(2
*
k
))
*
x
^
(
2
*
k
)
)
N
.
Definition
B1
(
x
:
R
) (
N
:
nat
) :
R
:=
sum_f_R0
(
fun
k
:
nat
=>
(
-1
)
^
k
/
INR
(
fact
(2
*
k
+
1))
*
x
^
(
2
*
k
+
1
)
)
N
.
Definition
C1
(
x
y
:
R
) (
N
:
nat
) :
R
:=
sum_f_R0
(
fun
k
:
nat
=>
(
-1
)
^
k
/
INR
(
fact
(2
*
k
))
*
(
x
+
y
)
^
(
2
*
k
)
)
N
.
Definition
Reste1
(
x
y
:
R
) (
N
:
nat
) :
R
:=
sum_f_R0
(
fun
k
:
nat
=>
sum_f_R0
(
fun
l
:
nat
=>
(
-1
)
^
S
(
l
+
k
)
/
INR
(
fact
(2
*
S
(
l
+
k
)))
*
x
^
(
2
*
S
(
l
+
k
)
)
*
(
(
-1
)
^
(
N
-
l
)
/
INR
(
fact
(2
*
(
N
-
l
)
))
)
*
y
^
(
2
*
(
N
-
l
)
)
) (
pred
(
N
-
k
))) (
pred
N
).
Definition
Reste2
(
x
y
:
R
) (
N
:
nat
) :
R
:=
sum_f_R0
(
fun
k
:
nat
=>
sum_f_R0
(
fun
l
:
nat
=>
(
-1
)
^
S
(
l
+
k
)
/
INR
(
fact
(2
*
S
(
l
+
k
)
+
1))
*
x
^
(
2
*
S
(
l
+
k
)
+
1
)
*
(
(
-1
)
^
(
N
-
l
)
/
INR
(
fact
(2
*
(
N
-
l
)
+
1))
)
*
y
^
(
2
*
(
N
-
l
)
+
1
)
) (
pred
(
N
-
k
))) (
pred
N
).
Definition
Reste
(
x
y
:
R
) (
N
:
nat
) :
R
:=
Reste2
x
y
N
-
Reste1
x
y
(
S
N
).
Theorem
cos_plus_form
:
forall
(
x
y
:
R
) (
n
:
nat
),
(0
<
n
)%
nat
->
A1
x
(
S
n
)
*
A1
y
(
S
n
)
-
B1
x
n
*
B1
y
n
+
Reste
x
y
n
=
C1
x
y
(
S
n
).
Lemma
pow_sqr
:
forall
(
x
:
R
) (
i
:
nat
),
x
^
(
2
*
i
)
=
(
x
*
x
)
^
i
.
Lemma
A1_cvg
:
forall
x
:
R
,
Un_cv
(
A1
x
) (
cos
x
).
Lemma
C1_cvg
:
forall
x
y
:
R
,
Un_cv
(
C1
x
y
) (
cos
(
x
+
y
)).
Lemma
B1_cvg
:
forall
x
:
R
,
Un_cv
(
B1
x
) (
sin
x
).