Library Coq.Reals.Exp_prop
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Rtrigo.
Require Import Ranalysis1.
Require Import PSeries_reg.
Require Import Div2.
Require Import Even.
Require Import Max.
Open Local Scope nat_scope.
Open Local Scope R_scope.
Definition E1 (
x:R) (
N:nat) :
R :=
sum_f_R0 (
fun k:nat => /
INR (
fact k) *
x ^
k)
N.
Lemma E1_cvg :
forall x:R,
Un_cv (
E1 x) (
exp x).
Definition Reste_E (
x y:R) (
N:nat) :
R :=
sum_f_R0
(
fun k:nat =>
sum_f_R0
(
fun l:nat =>
/
INR (
fact (
S (
l +
k))) *
x ^
S (
l +
k) *
(/
INR (
fact (
N -
l)) *
y ^ (
N -
l))) (
pred (
N -
k))) (
pred N).
Lemma exp_form :
forall (
x y:R) (
n:nat),
(0 <
n)%nat ->
E1 x n *
E1 y n -
Reste_E x y n =
E1 (
x +
y)
n.
Definition maj_Reste_E (
x y:R) (
N:nat) :
R :=
4 *
(
Rmax 1 (
Rmax (
Rabs x) (
Rabs y)) ^ (2 *
N) /
Rsqr (
INR (
fact (
div2 (
pred N))))).
Lemma Rle_Rinv :
forall x y:R, 0 <
x -> 0 <
y ->
x <=
y -> /
y <= /
x.
Lemma div2_double :
forall N:nat,
div2 (2 *
N) =
N.
Lemma div2_S_double :
forall N:nat,
div2 (
S (2 *
N)) =
N.
Lemma div2_not_R0 :
forall N:nat, (1 <
N)%nat -> (0 <
div2 N)%nat.
Lemma Reste_E_maj :
forall (
x y:R) (
N:nat),
(0 <
N)%nat ->
Rabs (
Reste_E x y N) <=
maj_Reste_E x y N.
Lemma maj_Reste_cv_R0 :
forall x y:R,
Un_cv (
maj_Reste_E x y) 0.
Lemma Reste_E_cv :
forall x y:R,
Un_cv (
Reste_E x y) 0.
Lemma exp_plus :
forall x y:R,
exp (
x +
y) =
exp x *
exp y.
Lemma exp_pos_pos :
forall x:R, 0 <
x -> 0 <
exp x.
Lemma exp_pos :
forall x:R, 0 <
exp x.
Lemma derivable_pt_lim_exp_0 :
derivable_pt_lim exp 0 1.
Lemma derivable_pt_lim_exp :
forall x:R,
derivable_pt_lim exp x (
exp x).