Library Coq.Reals.Exp_prop
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Rtrigo1.
Require Import Ranalysis1.
Require Import PSeries_reg.
Require Import Div2.
Require Import Even.
Require Import Max.
Local Open Scope nat_scope.
Local Open 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 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).