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 Lia Lra.
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 (Nat.div2 (pred N))))).

Lemma div2_double : forall N:nat, Nat.div2 (2 * N) = N.

Lemma div2_S_double : forall N:nat, Nat.div2 (S (2 * N)) = N.

Lemma div2_not_R0 : forall N:nat, (1 < N)%nat -> (0 < Nat.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).

Require Import Div2 Even Max.