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