Library Coq.Reals.Rtrigo_reg
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
SeqSeries
.
Require
Import
Rtrigo1
.
Require
Import
Ranalysis1
.
Require
Import
PSeries_reg
.
Local
Open
Scope
nat_scope
.
Local
Open
Scope
R_scope
.
Lemma
continuity_sin
:
continuity
sin
.
Lemma
CVN_R_sin
:
forall
fn
:
nat
->
R
->
R
,
fn
=
(
fun
(
N
:
nat
) (
x
:
R
) =>
(
-1
)
^
N
/
INR
(
fact
(2
*
N
+
1))
*
x
^
(
2
*
N
)
)
->
CVN_R
fn
.
(sin h)/h -> 1 when h -> 0
Lemma
derivable_pt_lim_sin_0
:
derivable_pt_lim
sin
0 1.
((cos h)-1)/h -> 0 when h -> 0
Lemma
derivable_pt_lim_cos_0
:
derivable_pt_lim
cos
0 0.
Theorem
derivable_pt_lim_sin
:
forall
x
:
R
,
derivable_pt_lim
sin
x
(
cos
x
).
Lemma
derivable_pt_lim_cos
:
forall
x
:
R
,
derivable_pt_lim
cos
x
(
-
sin
x
).
Lemma
derivable_pt_sin
:
forall
x
:
R
,
derivable_pt
sin
x
.
Lemma
derivable_pt_cos
:
forall
x
:
R
,
derivable_pt
cos
x
.
Lemma
derivable_sin
:
derivable
sin
.
Lemma
derivable_cos
:
derivable
cos
.
Lemma
derive_pt_sin
:
forall
x
:
R
,
derive_pt
sin
x
(
derivable_pt_sin
_
)
=
cos
x
.
Lemma
derive_pt_cos
:
forall
x
:
R
,
derive_pt
cos
x
(
derivable_pt_cos
_
)
=
-
sin
x
.