Library Stdlib.Reals.Exp_prop

From Stdlib Require Import Rbase.
From Stdlib Require Import Rfunctions.
From Stdlib Require Import SeqSeries.
From Stdlib Require Import Rtrigo1.
From Stdlib Require Import Ranalysis1.
From Stdlib Require Import PSeries_reg.
From Stdlib Require Import Lia Lra.
From Stdlib Require Import Arith.Factorial.
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).