Library Coq.Reals.Rtrigo_reg
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
SeqSeries
.
Require
Import
Rtrigo
.
Require
Import
Ranalysis1
.
Require
Import
PSeries_reg
.
Open
Local
Scope
nat_scope
.
Open
Local
Scope
R_scope
.
Lemma
CVN_R_cos
:
forall
fn
:nat ->
R
->
R
,
fn
= (
fun
(
N
:nat) (
x
:R) => (-1) ^
N
/
INR
(
fact
(2 *
N
)) *
x
^ (2 *
N
)) ->
CVN_R
fn
.
Lemma
continuity_cos
:
continuity
cos
.
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
.