Library Coq.Reals.Rtrigo_def
Require
Import
Rbase
Rfunctions
SeqSeries
Rtrigo_fun
Max
.
Local
Open
Scope
R_scope
.
Definition of exponential
Definition
exp_in
(
x
l
:
R
) :
Prop
:=
infinite_sum
(
fun
i
:
nat
=>
/
INR
(
fact
i
)
*
x
^
i
)
l
.
Lemma
exp_cof_no_R0
:
forall
n
:
nat
,
/
INR
(
fact
n
)
<>
0.
Lemma
exist_exp
:
forall
x
:
R
,
{
l
:
R
|
exp_in
x
l
}
.
Definition
exp
(
x
:
R
) :
R
:=
proj1_sig
(
exist_exp
x
).
Lemma
pow_i
:
forall
i
:
nat
, (0
<
i
)%
nat
-> 0
^
i
=
0.
Lemma
exist_exp0
:
{
l
:
R
|
exp_in
0
l
}
.
Lemma
exp_0
:
exp
0
=
1.
Definition of hyperbolic functions
Definition
cosh
(
x
:
R
) :
R
:=
(
exp
x
+
exp
(
-
x
)
)
/
2.
Definition
sinh
(
x
:
R
) :
R
:=
(
exp
x
-
exp
(
-
x
)
)
/
2.
Definition
tanh
(
x
:
R
) :
R
:=
sinh
x
/
cosh
x
.
Lemma
cosh_0
:
cosh
0
=
1.
Lemma
sinh_0
:
sinh
0
=
0.
Definition
cos_n
(
n
:
nat
) :
R
:=
(
-1
)
^
n
/
INR
(
fact
(2
*
n
)).
Lemma
simpl_cos_n
:
forall
n
:
nat
,
cos_n
(
S
n
)
/
cos_n
n
=
-
/
INR
(2
*
S
n
*
(
2
*
n
+
1
)
).
Lemma
archimed_cor1
:
forall
eps
:
R
, 0
<
eps
->
exists
N
:
nat
,
/
INR
N
<
eps
/\
(0
<
N
)%
nat
.
Lemma
Alembert_cos
:
Un_cv
(
fun
n
:
nat
=>
Rabs
(
cos_n
(
S
n
)
/
cos_n
n
)) 0.
Lemma
cosn_no_R0
:
forall
n
:
nat
,
cos_n
n
<>
0.
Definition
cos_in
(
x
l
:
R
) :
Prop
:=
infinite_sum
(
fun
i
:
nat
=>
cos_n
i
*
x
^
i
)
l
.
Lemma
exist_cos
:
forall
x
:
R
,
{
l
:
R
|
cos_in
x
l
}
.
Definition of cosinus
Definition
cos
(
x
:
R
) :
R
:=
let
(
a
,
_
) :=
exist_cos
(
Rsqr
x
)
in
a
.
Definition
sin_n
(
n
:
nat
) :
R
:=
(
-1
)
^
n
/
INR
(
fact
(2
*
n
+
1)).
Lemma
simpl_sin_n
:
forall
n
:
nat
,
sin_n
(
S
n
)
/
sin_n
n
=
-
/
INR
(
(
2
*
S
n
+
1
)
*
(
2
*
S
n
)
).
Lemma
Alembert_sin
:
Un_cv
(
fun
n
:
nat
=>
Rabs
(
sin_n
(
S
n
)
/
sin_n
n
)) 0.
Lemma
sin_no_R0
:
forall
n
:
nat
,
sin_n
n
<>
0.
Definition
sin_in
(
x
l
:
R
) :
Prop
:=
infinite_sum
(
fun
i
:
nat
=>
sin_n
i
*
x
^
i
)
l
.
Lemma
exist_sin
:
forall
x
:
R
,
{
l
:
R
|
sin_in
x
l
}
.
Definition
sin
(
x
:
R
) :
R
:=
let
(
a
,
_
) :=
exist_sin
(
Rsqr
x
)
in
x
*
a
.
Properties
Lemma
cos_sym
:
forall
x
:
R
,
cos
x
=
cos
(
-
x
).
Lemma
sin_antisym
:
forall
x
:
R
,
sin
(
-
x
)
=
-
sin
x
.
Lemma
sin_0
:
sin
0
=
0.
Lemma
exist_cos0
:
{
l
:
R
|
cos_in
0
l
}
.
Lemma
cos_0
:
cos
0
=
1.