Library Coq.Reals.Cos_rel
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
SeqSeries
.
Require
Import
Rtrigo_def
.
Open
Local
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
).