Library Coq.Reals.Ranalysis4
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
SeqSeries
.
Require
Import
Rtrigo
.
Require
Import
Ranalysis1
.
Require
Import
Ranalysis3
.
Require
Import
Exp_prop
.
Open
Local
Scope
R_scope
.
Lemma
derivable_pt_inv
:
forall
(
f
:R ->
R
) (
x
:R),
f
x
<> 0 ->
derivable_pt
f
x
->
derivable_pt
(/
f
)
x
.
Lemma
pr_nu_var
:
forall
(
f
g
:R ->
R
) (
x
:R) (
pr1
:derivable_pt
f
x
) (
pr2
:derivable_pt
g
x
),
f
=
g
->
derive_pt
f
x
pr1
=
derive_pt
g
x
pr2
.
Lemma
pr_nu_var2
:
forall
(
f
g
:R ->
R
) (
x
:R) (
pr1
:derivable_pt
f
x
) (
pr2
:derivable_pt
g
x
),
(
forall
h
:R,
f
h
=
g
h
) ->
derive_pt
f
x
pr1
=
derive_pt
g
x
pr2
.
Lemma
derivable_inv
:
forall
f
:R ->
R
, (
forall
x
:R,
f
x
<> 0) ->
derivable
f
->
derivable
(/
f
).
Lemma
derive_pt_inv
:
forall
(
f
:R ->
R
) (
x
:R) (
pr
:derivable_pt
f
x
) (
na
:f
x
<> 0),
derive_pt
(/
f
)
x
(
derivable_pt_inv
f
x
na
pr
) =
-
derive_pt
f
x
pr
/
Rsqr
(
f
x
).
Rabsolu
Lemma
Rabs_derive_1
:
forall
x
:R, 0 <
x
->
derivable_pt_lim
Rabs
x
1.
Lemma
Rabs_derive_2
:
forall
x
:R,
x
< 0 ->
derivable_pt_lim
Rabs
x
(-1).
Rabsolu is derivable for all x <> 0
Lemma
Rderivable_pt_abs
:
forall
x
:R,
x
<> 0 ->
derivable_pt
Rabs
x
.
Rabsolu is continuous for all x
Lemma
Rcontinuity_abs
:
continuity
Rabs
.
Finite sums : Sum a_k x^k
Lemma
continuity_finite_sum
:
forall
(
An
:nat ->
R
) (
N
:nat),
continuity
(
fun
y
:R =>
sum_f_R0
(
fun
k
:nat =>
An
k
*
y
^
k
)
N
).
Lemma
derivable_pt_lim_fs
:
forall
(
An
:nat ->
R
) (
x
:R) (
N
:nat),
(0 <
N
)%nat ->
derivable_pt_lim
(
fun
y
:R =>
sum_f_R0
(
fun
k
:nat =>
An
k
*
y
^
k
)
N
)
x
(
sum_f_R0
(
fun
k
:nat =>
INR
(
S
k
) *
An
(
S
k
) *
x
^
k
) (
pred
N
)).
Lemma
derivable_pt_lim_finite_sum
:
forall
(
An
:nat ->
R
) (
x
:R) (
N
:nat),
derivable_pt_lim
(
fun
y
:R =>
sum_f_R0
(
fun
k
:nat =>
An
k
*
y
^
k
)
N
)
x
match
N
with
|
O
=> 0
|
_
=>
sum_f_R0
(
fun
k
:nat =>
INR
(
S
k
) *
An
(
S
k
) *
x
^
k
) (
pred
N
)
end
.
Lemma
derivable_pt_finite_sum
:
forall
(
An
:nat ->
R
) (
N
:nat) (
x
:R),
derivable_pt
(
fun
y
:R =>
sum_f_R0
(
fun
k
:nat =>
An
k
*
y
^
k
)
N
)
x
.
Lemma
derivable_finite_sum
:
forall
(
An
:nat ->
R
) (
N
:nat),
derivable
(
fun
y
:R =>
sum_f_R0
(
fun
k
:nat =>
An
k
*
y
^
k
)
N
).
Regularity of hyperbolic functions
Lemma
derivable_pt_lim_cosh
:
forall
x
:R,
derivable_pt_lim
cosh
x
(
sinh
x
).
Lemma
derivable_pt_lim_sinh
:
forall
x
:R,
derivable_pt_lim
sinh
x
(
cosh
x
).
Lemma
derivable_pt_exp
:
forall
x
:R,
derivable_pt
exp
x
.
Lemma
derivable_pt_cosh
:
forall
x
:R,
derivable_pt
cosh
x
.
Lemma
derivable_pt_sinh
:
forall
x
:R,
derivable_pt
sinh
x
.
Lemma
derivable_exp
:
derivable
exp
.
Lemma
derivable_cosh
:
derivable
cosh
.
Lemma
derivable_sinh
:
derivable
sinh
.
Lemma
derive_pt_exp
:
forall
x
:R,
derive_pt
exp
x
(
derivable_pt_exp
x
) =
exp
x
.
Lemma
derive_pt_cosh
:
forall
x
:R,
derive_pt
cosh
x
(
derivable_pt_cosh
x
) =
sinh
x
.
Lemma
derive_pt_sinh
:
forall
x
:R,
derive_pt
sinh
x
(
derivable_pt_sinh
x
) =
cosh
x
.