diff options
Diffstat (limited to 'theories/Reals/Exp_prop.v')
| -rw-r--r-- | theories/Reals/Exp_prop.v | 1842 |
1 files changed, 913 insertions, 929 deletions
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 90ea93ef..5dafec83 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -5,8 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - -(*i $Id: Exp_prop.v 8670 2006-03-28 22:16:14Z herbelin $ i*) + +(*i $Id: Exp_prop.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -24,988 +24,972 @@ 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). -intro; unfold exp in |- *; unfold projT1 in |- *. -case (exist_exp x); intro. -unfold exp_in, Un_cv in |- *; unfold infinit_sum, E1 in |- *; trivial. +Proof. + intro; unfold exp in |- *; unfold projT1 in |- *. + case (exist_exp x); intro. + unfold exp_in, Un_cv in |- *; unfold infinit_sum, E1 in |- *; trivial. Qed. 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). + (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. -intros; unfold E1 in |- *. -rewrite cauchy_finite. -unfold Reste_E in |- *; unfold Rminus in |- *; rewrite Rplus_assoc; - rewrite Rplus_opp_r; rewrite Rplus_0_r; apply sum_eq; - intros. -rewrite binomial. -rewrite scal_sum; apply sum_eq; intros. -unfold C in |- *; unfold Rdiv in |- *; repeat rewrite Rmult_assoc; - rewrite (Rmult_comm (INR (fact i))); repeat rewrite Rmult_assoc; - rewrite <- Rinv_l_sym. -rewrite Rmult_1_r; rewrite Rinv_mult_distr. -ring. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -apply H. + forall (x y:R) (n:nat), + (0 < n)%nat -> E1 x n * E1 y n - Reste_E x y n = E1 (x + y) n. +Proof. + intros; unfold E1 in |- *. + rewrite cauchy_finite. + unfold Reste_E in |- *; unfold Rminus in |- *; rewrite Rplus_assoc; + rewrite Rplus_opp_r; rewrite Rplus_0_r; apply sum_eq; + intros. + rewrite binomial. + rewrite scal_sum; apply sum_eq; intros. + unfold C in |- *; unfold Rdiv in |- *; repeat rewrite Rmult_assoc; + rewrite (Rmult_comm (INR (fact i))); repeat rewrite Rmult_assoc; + rewrite <- Rinv_l_sym. + rewrite Rmult_1_r; rewrite Rinv_mult_distr. + ring. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + apply H. Qed. 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))))). + Rsqr (INR (fact (div2 (pred N))))). Lemma Rle_Rinv : forall x y:R, 0 < x -> 0 < y -> x <= y -> / y <= / x. -intros; apply Rmult_le_reg_l with x. -apply H. -rewrite <- Rinv_r_sym. -apply Rmult_le_reg_l with y. -apply H0. -rewrite Rmult_1_r; rewrite Rmult_comm; rewrite Rmult_assoc; - rewrite <- Rinv_l_sym. -rewrite Rmult_1_r; apply H1. -red in |- *; intro; rewrite H2 in H0; elim (Rlt_irrefl _ H0). -red in |- *; intro; rewrite H2 in H; elim (Rlt_irrefl _ H). +Proof. + intros; apply Rmult_le_reg_l with x. + apply H. + rewrite <- Rinv_r_sym. + apply Rmult_le_reg_l with y. + apply H0. + rewrite Rmult_1_r; rewrite Rmult_comm; rewrite Rmult_assoc; + rewrite <- Rinv_l_sym. + rewrite Rmult_1_r; apply H1. + red in |- *; intro; rewrite H2 in H0; elim (Rlt_irrefl _ H0). + red in |- *; intro; rewrite H2 in H; elim (Rlt_irrefl _ H). Qed. (**********) Lemma div2_double : forall N:nat, div2 (2 * N) = N. -intro; induction N as [| N HrecN]. -reflexivity. -replace (2 * S N)%nat with (S (S (2 * N))). -simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity. -apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; - ring. +Proof. + intro; induction N as [| N HrecN]. + reflexivity. + replace (2 * S N)%nat with (S (S (2 * N))). + simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity. + ring_nat. Qed. Lemma div2_S_double : forall N:nat, div2 (S (2 * N)) = N. -intro; induction N as [| N HrecN]. -reflexivity. -replace (2 * S N)%nat with (S (S (2 * N))). -simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity. -apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; - ring. +Proof. + intro; induction N as [| N HrecN]. + reflexivity. + replace (2 * S N)%nat with (S (S (2 * N))). + simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity. + ring_nat. Qed. Lemma div2_not_R0 : forall N:nat, (1 < N)%nat -> (0 < div2 N)%nat. -intros; induction N as [| N HrecN]. -elim (lt_n_O _ H). -cut ((1 < N)%nat \/ N = 1%nat). -intro; elim H0; intro. -assert (H2 := even_odd_dec N). -elim H2; intro. -rewrite <- (even_div2 _ a); apply HrecN; assumption. -rewrite <- (odd_div2 _ b); apply lt_O_Sn. -rewrite H1; simpl in |- *; apply lt_O_Sn. -inversion H. -right; reflexivity. -left; apply lt_le_trans with 2%nat; [ apply lt_n_Sn | apply H1 ]. +Proof. + intros; induction N as [| N HrecN]. + elim (lt_n_O _ H). + cut ((1 < N)%nat \/ N = 1%nat). + intro; elim H0; intro. + assert (H2 := even_odd_dec N). + elim H2; intro. + rewrite <- (even_div2 _ a); apply HrecN; assumption. + rewrite <- (odd_div2 _ b); apply lt_O_Sn. + rewrite H1; simpl in |- *; apply lt_O_Sn. + inversion H. + right; reflexivity. + left; apply lt_le_trans with 2%nat; [ apply lt_n_Sn | apply H1 ]. Qed. 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. -intros; set (M := Rmax 1 (Rmax (Rabs x) (Rabs y))). -apply Rle_trans with - (M ^ (2 * N) * - sum_f_R0 - (fun k:nat => - sum_f_R0 (fun l:nat => / Rsqr (INR (fact (div2 (S N))))) - (pred (N - k))) (pred N)). -unfold Reste_E in |- *. -apply Rle_trans with - (sum_f_R0 - (fun k:nat => - Rabs - (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)). -apply - (Rsum_abs - (fun k:nat => - sum_f_R0 - (fun l:nat => + forall (x y:R) (N:nat), + (0 < N)%nat -> Rabs (Reste_E x y N) <= maj_Reste_E x y N. +Proof. + intros; set (M := Rmax 1 (Rmax (Rabs x) (Rabs y))). + apply Rle_trans with + (M ^ (2 * N) * + sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => / Rsqr (INR (fact (div2 (S N))))) + (pred (N - k))) (pred N)). + unfold Reste_E in |- *. + apply Rle_trans with + (sum_f_R0 + (fun k:nat => + Rabs + (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)). -apply Rle_trans with - (sum_f_R0 - (fun k:nat => - sum_f_R0 - (fun l:nat => - Rabs - (/ INR (fact (S (l + k))) * x ^ S (l + k) * - (/ INR (fact (N - l)) * y ^ (N - l)))) ( - pred (N - k))) (pred N)). -apply sum_Rle; intros. -apply - (Rsum_abs - (fun l:nat => - / INR (fact (S (l + n))) * x ^ S (l + n) * - (/ INR (fact (N - l)) * y ^ (N - l)))). -apply Rle_trans with - (sum_f_R0 - (fun k:nat => - sum_f_R0 - (fun l:nat => - M ^ (2 * N) * / INR (fact (S l)) * / INR (fact (N - l))) - (pred (N - k))) (pred N)). -apply sum_Rle; intros. -apply sum_Rle; intros. -repeat rewrite Rabs_mult. -do 2 rewrite <- RPow_abs. -rewrite (Rabs_right (/ INR (fact (S (n0 + n))))). -rewrite (Rabs_right (/ INR (fact (N - n0)))). -replace - (/ INR (fact (S (n0 + n))) * Rabs x ^ S (n0 + n) * - (/ INR (fact (N - n0)) * Rabs y ^ (N - n0))) with - (/ INR (fact (N - n0)) * / INR (fact (S (n0 + n))) * Rabs x ^ S (n0 + n) * - Rabs y ^ (N - n0)); [ idtac | ring ]. -rewrite <- (Rmult_comm (/ INR (fact (N - n0)))). -repeat rewrite Rmult_assoc. -apply Rmult_le_compat_l. -left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. -apply Rle_trans with - (/ INR (fact (S n0)) * Rabs x ^ S (n0 + n) * Rabs y ^ (N - n0)). -rewrite (Rmult_comm (/ INR (fact (S (n0 + n))))); - rewrite (Rmult_comm (/ INR (fact (S n0)))); repeat rewrite Rmult_assoc; - apply Rmult_le_compat_l. -apply pow_le; apply Rabs_pos. -rewrite (Rmult_comm (/ INR (fact (S n0)))); apply Rmult_le_compat_l. -apply pow_le; apply Rabs_pos. -apply Rle_Rinv. -apply INR_fact_lt_0. -apply INR_fact_lt_0. -apply le_INR; apply fact_le; apply le_n_S. -apply le_plus_l. -rewrite (Rmult_comm (M ^ (2 * N))); rewrite Rmult_assoc; - apply Rmult_le_compat_l. -left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. -apply Rle_trans with (M ^ S (n0 + n) * Rabs y ^ (N - n0)). -do 2 rewrite <- (Rmult_comm (Rabs y ^ (N - n0))). -apply Rmult_le_compat_l. -apply pow_le; apply Rabs_pos. -apply pow_incr; split. -apply Rabs_pos. -apply Rle_trans with (Rmax (Rabs x) (Rabs y)). -apply RmaxLess1. -unfold M in |- *; apply RmaxLess2. -apply Rle_trans with (M ^ S (n0 + n) * M ^ (N - n0)). -apply Rmult_le_compat_l. -apply pow_le; apply Rle_trans with 1. -left; apply Rlt_0_1. -unfold M in |- *; apply RmaxLess1. -apply pow_incr; split. -apply Rabs_pos. -apply Rle_trans with (Rmax (Rabs x) (Rabs y)). -apply RmaxLess2. -unfold M in |- *; apply RmaxLess2. -rewrite <- pow_add; replace (S (n0 + n) + (N - n0))%nat with (N + S n)%nat. -apply Rle_pow. -unfold M in |- *; apply RmaxLess1. -replace (2 * N)%nat with (N + N)%nat; [ idtac | ring ]. -apply plus_le_compat_l. -replace N with (S (pred N)). -apply le_n_S; apply H0. -symmetry in |- *; apply S_pred with 0%nat; apply H. -apply INR_eq; do 2 rewrite plus_INR; do 2 rewrite S_INR; rewrite plus_INR; - rewrite minus_INR. -ring. -apply le_trans with (pred (N - n)). -apply H1. -apply le_S_n. -replace (S (pred (N - n))) with (N - n)%nat. -apply le_trans with N. -apply (fun p n m:nat => plus_le_reg_l n m p) with n. -rewrite <- le_plus_minus. -apply le_plus_r. -apply le_trans with (pred N). -apply H0. -apply le_pred_n. -apply le_n_Sn. -apply S_pred with 0%nat. -apply plus_lt_reg_l with n. -rewrite <- le_plus_minus. -replace (n + 0)%nat with n; [ idtac | ring ]. -apply le_lt_trans with (pred N). -apply H0. -apply lt_pred_n_n. -apply H. -apply le_trans with (pred N). -apply H0. -apply le_pred_n. -apply Rle_ge; left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. -apply Rle_ge; left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. -rewrite scal_sum. -apply sum_Rle; intros. -rewrite <- Rmult_comm. -rewrite scal_sum. -apply sum_Rle; intros. -rewrite (Rmult_comm (/ Rsqr (INR (fact (div2 (S N)))))). -rewrite Rmult_assoc; apply Rmult_le_compat_l. -apply pow_le. -apply Rle_trans with 1. -left; apply Rlt_0_1. -unfold M in |- *; apply RmaxLess1. -assert (H2 := even_odd_cor N). -elim H2; intros N0 H3. -elim H3; intro. -apply Rle_trans with (/ INR (fact n0) * / INR (fact (N - n0))). -do 2 rewrite <- (Rmult_comm (/ INR (fact (N - n0)))). -apply Rmult_le_compat_l. -left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. -apply Rle_Rinv. -apply INR_fact_lt_0. -apply INR_fact_lt_0. -apply le_INR. -apply fact_le. -apply le_n_Sn. -replace (/ INR (fact n0) * / INR (fact (N - n0))) with - (C N n0 / INR (fact N)). -pattern N at 1 in |- *; rewrite H4. -apply Rle_trans with (C N N0 / INR (fact N)). -unfold Rdiv in |- *; do 2 rewrite <- (Rmult_comm (/ INR (fact N))). -apply Rmult_le_compat_l. -left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. -rewrite H4. -apply C_maj. -rewrite <- H4; apply le_trans with (pred (N - n)). -apply H1. -apply le_S_n. -replace (S (pred (N - n))) with (N - n)%nat. -apply le_trans with N. -apply (fun p n m:nat => plus_le_reg_l n m p) with n. -rewrite <- le_plus_minus. -apply le_plus_r. -apply le_trans with (pred N). -apply H0. -apply le_pred_n. -apply le_n_Sn. -apply S_pred with 0%nat. -apply plus_lt_reg_l with n. -rewrite <- le_plus_minus. -replace (n + 0)%nat with n; [ idtac | ring ]. -apply le_lt_trans with (pred N). -apply H0. -apply lt_pred_n_n. -apply H. -apply le_trans with (pred N). -apply H0. -apply le_pred_n. -replace (C N N0 / INR (fact N)) with (/ Rsqr (INR (fact N0))). -rewrite H4; rewrite div2_S_double; right; reflexivity. -unfold Rsqr, C, Rdiv in |- *. -repeat rewrite Rinv_mult_distr. -rewrite (Rmult_comm (INR (fact N))). -repeat rewrite Rmult_assoc. -rewrite <- Rinv_r_sym. -rewrite Rmult_1_r; replace (N - N0)%nat with N0. -ring. -replace N with (N0 + N0)%nat. -symmetry in |- *; apply minus_plus. -rewrite H4. -apply INR_eq; rewrite plus_INR; rewrite mult_INR; do 2 rewrite S_INR; ring. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -unfold C, Rdiv in |- *. -rewrite (Rmult_comm (INR (fact N))). -repeat rewrite Rmult_assoc. -rewrite <- Rinv_r_sym. -rewrite Rinv_mult_distr. -rewrite Rmult_1_r; ring. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -replace (/ INR (fact (S n0)) * / INR (fact (N - n0))) with - (C (S N) (S n0) / INR (fact (S N))). -apply Rle_trans with (C (S N) (S N0) / INR (fact (S N))). -unfold Rdiv in |- *; do 2 rewrite <- (Rmult_comm (/ INR (fact (S N)))). -apply Rmult_le_compat_l. -left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. -cut (S N = (2 * S N0)%nat). -intro; rewrite H5; apply C_maj. -rewrite <- H5; apply le_n_S. -apply le_trans with (pred (N - n)). -apply H1. -apply le_S_n. -replace (S (pred (N - n))) with (N - n)%nat. -apply le_trans with N. -apply (fun p n m:nat => plus_le_reg_l n m p) with n. -rewrite <- le_plus_minus. -apply le_plus_r. -apply le_trans with (pred N). -apply H0. -apply le_pred_n. -apply le_n_Sn. -apply S_pred with 0%nat. -apply plus_lt_reg_l with n. -rewrite <- le_plus_minus. -replace (n + 0)%nat with n; [ idtac | ring ]. -apply le_lt_trans with (pred N). -apply H0. -apply lt_pred_n_n. -apply H. -apply le_trans with (pred N). -apply H0. -apply le_pred_n. -apply INR_eq; rewrite H4. -do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; ring. -cut (S N = (2 * S N0)%nat). -intro. -replace (C (S N) (S N0) / INR (fact (S N))) with (/ Rsqr (INR (fact (S N0)))). -rewrite H5; rewrite div2_double. -right; reflexivity. -unfold Rsqr, C, Rdiv in |- *. -repeat rewrite Rinv_mult_distr. -replace (S N - S N0)%nat with (S N0). -rewrite (Rmult_comm (INR (fact (S N)))). -repeat rewrite Rmult_assoc. -rewrite <- Rinv_r_sym. -rewrite Rmult_1_r; reflexivity. -apply INR_fact_neq_0. -replace (S N) with (S N0 + S N0)%nat. -symmetry in |- *; apply minus_plus. -rewrite H5; ring. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -apply INR_eq; rewrite H4; do 2 rewrite S_INR; do 2 rewrite mult_INR; - repeat rewrite S_INR; ring. -unfold C, Rdiv in |- *. -rewrite (Rmult_comm (INR (fact (S N)))). -rewrite Rmult_assoc; rewrite <- Rinv_r_sym. -rewrite Rmult_1_r; rewrite Rinv_mult_distr. -reflexivity. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -unfold maj_Reste_E in |- *. -unfold Rdiv in |- *; rewrite (Rmult_comm 4). -rewrite Rmult_assoc. -apply Rmult_le_compat_l. -apply pow_le. -apply Rle_trans with 1. -left; apply Rlt_0_1. -apply RmaxLess1. -apply Rle_trans with - (sum_f_R0 (fun k:nat => INR (N - k) * / Rsqr (INR (fact (div2 (S N))))) - (pred N)). -apply sum_Rle; intros. -rewrite sum_cte. -replace (S (pred (N - n))) with (N - n)%nat. -right; apply Rmult_comm. -apply S_pred with 0%nat. -apply plus_lt_reg_l with n. -rewrite <- le_plus_minus. -replace (n + 0)%nat with n; [ idtac | ring ]. -apply le_lt_trans with (pred N). -apply H0. -apply lt_pred_n_n. -apply H. -apply le_trans with (pred N). -apply H0. -apply le_pred_n. -apply Rle_trans with - (sum_f_R0 (fun k:nat => INR N * / Rsqr (INR (fact (div2 (S N))))) (pred N)). -apply sum_Rle; intros. -do 2 rewrite <- (Rmult_comm (/ Rsqr (INR (fact (div2 (S N)))))). -apply Rmult_le_compat_l. -left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt. -apply INR_fact_neq_0. -apply le_INR. -apply (fun p n m:nat => plus_le_reg_l n m p) with n. -rewrite <- le_plus_minus. -apply le_plus_r. -apply le_trans with (pred N). -apply H0. -apply le_pred_n. -rewrite sum_cte; replace (S (pred N)) with N. -cut (div2 (S N) = S (div2 (pred N))). -intro; rewrite H0. -rewrite fact_simpl; rewrite mult_comm; rewrite mult_INR; rewrite Rsqr_mult. -rewrite Rinv_mult_distr. -rewrite (Rmult_comm (INR N)); repeat rewrite Rmult_assoc; - apply Rmult_le_compat_l. -left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt; apply INR_fact_neq_0. -rewrite <- H0. -cut (INR N <= INR (2 * div2 (S N))). -intro; apply Rmult_le_reg_l with (Rsqr (INR (div2 (S N)))). -apply Rsqr_pos_lt. -apply not_O_INR; red in |- *; intro. -cut (1 < S N)%nat. -intro; assert (H4 := div2_not_R0 _ H3). -rewrite H2 in H4; elim (lt_n_O _ H4). -apply lt_n_S; apply H. -repeat rewrite <- Rmult_assoc. -rewrite <- Rinv_r_sym. -rewrite Rmult_1_l. -replace (INR N * INR N) with (Rsqr (INR N)); [ idtac | reflexivity ]. -rewrite Rmult_assoc. -rewrite Rmult_comm. -replace 4 with (Rsqr 2); [ idtac | ring_Rsqr ]. -rewrite <- Rsqr_mult. -apply Rsqr_incr_1. -replace 2 with (INR 2). -rewrite <- mult_INR; apply H1. -reflexivity. -left; apply lt_INR_0; apply H. -left; apply Rmult_lt_0_compat. -prove_sup0. -apply lt_INR_0; apply div2_not_R0. -apply lt_n_S; apply H. -cut (1 < S N)%nat. -intro; unfold Rsqr in |- *; apply prod_neq_R0; apply not_O_INR; intro; - assert (H4 := div2_not_R0 _ H2); rewrite H3 in H4; - elim (lt_n_O _ H4). -apply lt_n_S; apply H. -assert (H1 := even_odd_cor N). -elim H1; intros N0 H2. -elim H2; intro. -pattern N at 2 in |- *; rewrite H3. -rewrite div2_S_double. -right; rewrite H3; reflexivity. -pattern N at 2 in |- *; rewrite H3. -replace (S (S (2 * N0))) with (2 * S N0)%nat. -rewrite div2_double. -rewrite H3. -rewrite S_INR; do 2 rewrite mult_INR. -rewrite (S_INR N0). -rewrite Rmult_plus_distr_l. -apply Rplus_le_compat_l. -rewrite Rmult_1_r. -simpl in |- *. -pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; - apply Rlt_0_1. -apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; - ring. -unfold Rsqr in |- *; apply prod_neq_R0; apply INR_fact_neq_0. -unfold Rsqr in |- *; apply prod_neq_R0; apply not_O_INR; discriminate. -assert (H0 := even_odd_cor N). -elim H0; intros N0 H1. -elim H1; intro. -cut (0 < N0)%nat. -intro; rewrite H2. -rewrite div2_S_double. -replace (2 * N0)%nat with (S (S (2 * pred N0))). -replace (pred (S (S (2 * pred N0)))) with (S (2 * pred N0)). -rewrite div2_S_double. -apply S_pred with 0%nat; apply H3. -reflexivity. -replace N0 with (S (pred N0)). -apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; - ring. -symmetry in |- *; apply S_pred with 0%nat; apply H3. -rewrite H2 in H. -apply neq_O_lt. -red in |- *; intro. -rewrite <- H3 in H. -simpl in H. -elim (lt_n_O _ H). -rewrite H2. -replace (pred (S (2 * N0))) with (2 * N0)%nat; [ idtac | reflexivity ]. -replace (S (S (2 * N0))) with (2 * S N0)%nat. -do 2 rewrite div2_double. -reflexivity. -apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; - ring. -apply S_pred with 0%nat; apply H. + pred (N - k)))) (pred N)). + apply + (Rsum_abs + (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)). + apply Rle_trans with + (sum_f_R0 + (fun k:nat => + sum_f_R0 + (fun l:nat => + Rabs + (/ INR (fact (S (l + k))) * x ^ S (l + k) * + (/ INR (fact (N - l)) * y ^ (N - l)))) ( + pred (N - k))) (pred N)). + apply sum_Rle; intros. + apply + (Rsum_abs + (fun l:nat => + / INR (fact (S (l + n))) * x ^ S (l + n) * + (/ INR (fact (N - l)) * y ^ (N - l)))). + apply Rle_trans with + (sum_f_R0 + (fun k:nat => + sum_f_R0 + (fun l:nat => + M ^ (2 * N) * / INR (fact (S l)) * / INR (fact (N - l))) + (pred (N - k))) (pred N)). + apply sum_Rle; intros. + apply sum_Rle; intros. + repeat rewrite Rabs_mult. + do 2 rewrite <- RPow_abs. + rewrite (Rabs_right (/ INR (fact (S (n0 + n))))). + rewrite (Rabs_right (/ INR (fact (N - n0)))). + replace + (/ INR (fact (S (n0 + n))) * Rabs x ^ S (n0 + n) * + (/ INR (fact (N - n0)) * Rabs y ^ (N - n0))) with + (/ INR (fact (N - n0)) * / INR (fact (S (n0 + n))) * Rabs x ^ S (n0 + n) * + Rabs y ^ (N - n0)); [ idtac | ring ]. + rewrite <- (Rmult_comm (/ INR (fact (N - n0)))). + repeat rewrite Rmult_assoc. + apply Rmult_le_compat_l. + left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. + apply Rle_trans with + (/ INR (fact (S n0)) * Rabs x ^ S (n0 + n) * Rabs y ^ (N - n0)). + rewrite (Rmult_comm (/ INR (fact (S (n0 + n))))); + rewrite (Rmult_comm (/ INR (fact (S n0)))); repeat rewrite Rmult_assoc; + apply Rmult_le_compat_l. + apply pow_le; apply Rabs_pos. + rewrite (Rmult_comm (/ INR (fact (S n0)))); apply Rmult_le_compat_l. + apply pow_le; apply Rabs_pos. + apply Rle_Rinv. + apply INR_fact_lt_0. + apply INR_fact_lt_0. + apply le_INR; apply fact_le; apply le_n_S. + apply le_plus_l. + rewrite (Rmult_comm (M ^ (2 * N))); rewrite Rmult_assoc; + apply Rmult_le_compat_l. + left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. + apply Rle_trans with (M ^ S (n0 + n) * Rabs y ^ (N - n0)). + do 2 rewrite <- (Rmult_comm (Rabs y ^ (N - n0))). + apply Rmult_le_compat_l. + apply pow_le; apply Rabs_pos. + apply pow_incr; split. + apply Rabs_pos. + apply Rle_trans with (Rmax (Rabs x) (Rabs y)). + apply RmaxLess1. + unfold M in |- *; apply RmaxLess2. + apply Rle_trans with (M ^ S (n0 + n) * M ^ (N - n0)). + apply Rmult_le_compat_l. + apply pow_le; apply Rle_trans with 1. + left; apply Rlt_0_1. + unfold M in |- *; apply RmaxLess1. + apply pow_incr; split. + apply Rabs_pos. + apply Rle_trans with (Rmax (Rabs x) (Rabs y)). + apply RmaxLess2. + unfold M in |- *; apply RmaxLess2. + rewrite <- pow_add; replace (S (n0 + n) + (N - n0))%nat with (N + S n)%nat. + apply Rle_pow. + unfold M in |- *; apply RmaxLess1. + replace (2 * N)%nat with (N + N)%nat; [ idtac | ring ]. + apply plus_le_compat_l. + replace N with (S (pred N)). + apply le_n_S; apply H0. + symmetry in |- *; apply S_pred with 0%nat; apply H. + apply INR_eq; do 2 rewrite plus_INR; do 2 rewrite S_INR; rewrite plus_INR; + rewrite minus_INR. + ring. + apply le_trans with (pred (N - n)). + apply H1. + apply le_S_n. + replace (S (pred (N - n))) with (N - n)%nat. + apply le_trans with N. + apply (fun p n m:nat => plus_le_reg_l n m p) with n. + rewrite <- le_plus_minus. + apply le_plus_r. + apply le_trans with (pred N). + apply H0. + apply le_pred_n. + apply le_n_Sn. + apply S_pred with 0%nat. + apply plus_lt_reg_l with n. + rewrite <- le_plus_minus. + replace (n + 0)%nat with n; [ idtac | ring ]. + apply le_lt_trans with (pred N). + apply H0. + apply lt_pred_n_n. + apply H. + apply le_trans with (pred N). + apply H0. + apply le_pred_n. + apply Rle_ge; left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. + apply Rle_ge; left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. + rewrite scal_sum. + apply sum_Rle; intros. + rewrite <- Rmult_comm. + rewrite scal_sum. + apply sum_Rle; intros. + rewrite (Rmult_comm (/ Rsqr (INR (fact (div2 (S N)))))). + rewrite Rmult_assoc; apply Rmult_le_compat_l. + apply pow_le. + apply Rle_trans with 1. + left; apply Rlt_0_1. + unfold M in |- *; apply RmaxLess1. + assert (H2 := even_odd_cor N). + elim H2; intros N0 H3. + elim H3; intro. + apply Rle_trans with (/ INR (fact n0) * / INR (fact (N - n0))). + do 2 rewrite <- (Rmult_comm (/ INR (fact (N - n0)))). + apply Rmult_le_compat_l. + left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. + apply Rle_Rinv. + apply INR_fact_lt_0. + apply INR_fact_lt_0. + apply le_INR. + apply fact_le. + apply le_n_Sn. + replace (/ INR (fact n0) * / INR (fact (N - n0))) with + (C N n0 / INR (fact N)). + pattern N at 1 in |- *; rewrite H4. + apply Rle_trans with (C N N0 / INR (fact N)). + unfold Rdiv in |- *; do 2 rewrite <- (Rmult_comm (/ INR (fact N))). + apply Rmult_le_compat_l. + left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. + rewrite H4. + apply C_maj. + rewrite <- H4; apply le_trans with (pred (N - n)). + apply H1. + apply le_S_n. + replace (S (pred (N - n))) with (N - n)%nat. + apply le_trans with N. + apply (fun p n m:nat => plus_le_reg_l n m p) with n. + rewrite <- le_plus_minus. + apply le_plus_r. + apply le_trans with (pred N). + apply H0. + apply le_pred_n. + apply le_n_Sn. + apply S_pred with 0%nat. + apply plus_lt_reg_l with n. + rewrite <- le_plus_minus. + replace (n + 0)%nat with n; [ idtac | ring ]. + apply le_lt_trans with (pred N). + apply H0. + apply lt_pred_n_n. + apply H. + apply le_trans with (pred N). + apply H0. + apply le_pred_n. + replace (C N N0 / INR (fact N)) with (/ Rsqr (INR (fact N0))). + rewrite H4; rewrite div2_S_double; right; reflexivity. + unfold Rsqr, C, Rdiv in |- *. + repeat rewrite Rinv_mult_distr. + rewrite (Rmult_comm (INR (fact N))). + repeat rewrite Rmult_assoc. + rewrite <- Rinv_r_sym. + rewrite Rmult_1_r; replace (N - N0)%nat with N0. + ring. + replace N with (N0 + N0)%nat. + symmetry in |- *; apply minus_plus. + rewrite H4. + ring. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + unfold C, Rdiv in |- *. + rewrite (Rmult_comm (INR (fact N))). + repeat rewrite Rmult_assoc. + rewrite <- Rinv_r_sym. + rewrite Rinv_mult_distr. + rewrite Rmult_1_r; ring. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + replace (/ INR (fact (S n0)) * / INR (fact (N - n0))) with + (C (S N) (S n0) / INR (fact (S N))). + apply Rle_trans with (C (S N) (S N0) / INR (fact (S N))). + unfold Rdiv in |- *; do 2 rewrite <- (Rmult_comm (/ INR (fact (S N)))). + apply Rmult_le_compat_l. + left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. + cut (S N = (2 * S N0)%nat). + intro; rewrite H5; apply C_maj. + rewrite <- H5; apply le_n_S. + apply le_trans with (pred (N - n)). + apply H1. + apply le_S_n. + replace (S (pred (N - n))) with (N - n)%nat. + apply le_trans with N. + apply (fun p n m:nat => plus_le_reg_l n m p) with n. + rewrite <- le_plus_minus. + apply le_plus_r. + apply le_trans with (pred N). + apply H0. + apply le_pred_n. + apply le_n_Sn. + apply S_pred with 0%nat. + apply plus_lt_reg_l with n. + rewrite <- le_plus_minus. + replace (n + 0)%nat with n; [ idtac | ring ]. + apply le_lt_trans with (pred N). + apply H0. + apply lt_pred_n_n. + apply H. + apply le_trans with (pred N). + apply H0. + apply le_pred_n. + rewrite H4; ring_nat. + cut (S N = (2 * S N0)%nat). + intro. + replace (C (S N) (S N0) / INR (fact (S N))) with (/ Rsqr (INR (fact (S N0)))). + rewrite H5; rewrite div2_double. + right; reflexivity. + unfold Rsqr, C, Rdiv in |- *. + repeat rewrite Rinv_mult_distr. + replace (S N - S N0)%nat with (S N0). + rewrite (Rmult_comm (INR (fact (S N)))). + repeat rewrite Rmult_assoc. + rewrite <- Rinv_r_sym. + rewrite Rmult_1_r; reflexivity. + apply INR_fact_neq_0. + replace (S N) with (S N0 + S N0)%nat. + symmetry in |- *; apply minus_plus. + rewrite H5; ring. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + rewrite H4; ring_nat. + unfold C, Rdiv in |- *. + rewrite (Rmult_comm (INR (fact (S N)))). + rewrite Rmult_assoc; rewrite <- Rinv_r_sym. + rewrite Rmult_1_r; rewrite Rinv_mult_distr. + reflexivity. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + unfold maj_Reste_E in |- *. + unfold Rdiv in |- *; rewrite (Rmult_comm 4). + rewrite Rmult_assoc. + apply Rmult_le_compat_l. + apply pow_le. + apply Rle_trans with 1. + left; apply Rlt_0_1. + apply RmaxLess1. + apply Rle_trans with + (sum_f_R0 (fun k:nat => INR (N - k) * / Rsqr (INR (fact (div2 (S N))))) + (pred N)). + apply sum_Rle; intros. + rewrite sum_cte. + replace (S (pred (N - n))) with (N - n)%nat. + right; apply Rmult_comm. + apply S_pred with 0%nat. + apply plus_lt_reg_l with n. + rewrite <- le_plus_minus. + replace (n + 0)%nat with n; [ idtac | ring ]. + apply le_lt_trans with (pred N). + apply H0. + apply lt_pred_n_n. + apply H. + apply le_trans with (pred N). + apply H0. + apply le_pred_n. + apply Rle_trans with + (sum_f_R0 (fun k:nat => INR N * / Rsqr (INR (fact (div2 (S N))))) (pred N)). + apply sum_Rle; intros. + do 2 rewrite <- (Rmult_comm (/ Rsqr (INR (fact (div2 (S N)))))). + apply Rmult_le_compat_l. + left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt. + apply INR_fact_neq_0. + apply le_INR. + apply (fun p n m:nat => plus_le_reg_l n m p) with n. + rewrite <- le_plus_minus. + apply le_plus_r. + apply le_trans with (pred N). + apply H0. + apply le_pred_n. + rewrite sum_cte; replace (S (pred N)) with N. + cut (div2 (S N) = S (div2 (pred N))). + intro; rewrite H0. + rewrite fact_simpl; rewrite mult_comm; rewrite mult_INR; rewrite Rsqr_mult. + rewrite Rinv_mult_distr. + rewrite (Rmult_comm (INR N)); repeat rewrite Rmult_assoc; + apply Rmult_le_compat_l. + left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt; apply INR_fact_neq_0. + rewrite <- H0. + cut (INR N <= INR (2 * div2 (S N))). + intro; apply Rmult_le_reg_l with (Rsqr (INR (div2 (S N)))). + apply Rsqr_pos_lt. + apply not_O_INR; red in |- *; intro. + cut (1 < S N)%nat. + intro; assert (H4 := div2_not_R0 _ H3). + rewrite H2 in H4; elim (lt_n_O _ H4). + apply lt_n_S; apply H. + repeat rewrite <- Rmult_assoc. + rewrite <- Rinv_r_sym. + rewrite Rmult_1_l. + replace (INR N * INR N) with (Rsqr (INR N)); [ idtac | reflexivity ]. + rewrite Rmult_assoc. + rewrite Rmult_comm. + replace 4 with (Rsqr 2); [ idtac | ring_Rsqr ]. + rewrite <- Rsqr_mult. + apply Rsqr_incr_1. + replace 2 with (INR 2). + rewrite <- mult_INR; apply H1. + reflexivity. + left; apply lt_INR_0; apply H. + left; apply Rmult_lt_0_compat. + prove_sup0. + apply lt_INR_0; apply div2_not_R0. + apply lt_n_S; apply H. + cut (1 < S N)%nat. + intro; unfold Rsqr in |- *; apply prod_neq_R0; apply not_O_INR; intro; + assert (H4 := div2_not_R0 _ H2); rewrite H3 in H4; + elim (lt_n_O _ H4). + apply lt_n_S; apply H. + assert (H1 := even_odd_cor N). + elim H1; intros N0 H2. + elim H2; intro. + pattern N at 2 in |- *; rewrite H3. + rewrite div2_S_double. + right; rewrite H3; reflexivity. + pattern N at 2 in |- *; rewrite H3. + replace (S (S (2 * N0))) with (2 * S N0)%nat. + rewrite div2_double. + rewrite H3. + rewrite S_INR; do 2 rewrite mult_INR. + rewrite (S_INR N0). + rewrite Rmult_plus_distr_l. + apply Rplus_le_compat_l. + rewrite Rmult_1_r. + simpl in |- *. + pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; + apply Rlt_0_1. + ring_nat. + unfold Rsqr in |- *; apply prod_neq_R0; apply INR_fact_neq_0. + unfold Rsqr in |- *; apply prod_neq_R0; apply not_O_INR; discriminate. + assert (H0 := even_odd_cor N). + elim H0; intros N0 H1. + elim H1; intro. + cut (0 < N0)%nat. + intro; rewrite H2. + rewrite div2_S_double. + replace (2 * N0)%nat with (S (S (2 * pred N0))). + replace (pred (S (S (2 * pred N0)))) with (S (2 * pred N0)). + rewrite div2_S_double. + apply S_pred with 0%nat; apply H3. + reflexivity. + omega. + omega. + rewrite H2. + replace (pred (S (2 * N0))) with (2 * N0)%nat; [ idtac | reflexivity ]. + replace (S (S (2 * N0))) with (2 * S N0)%nat. + do 2 rewrite div2_double. + reflexivity. + ring_nat. + apply S_pred with 0%nat; apply H. Qed. Lemma maj_Reste_cv_R0 : forall x y:R, Un_cv (maj_Reste_E x y) 0. -intros; assert (H := Majxy_cv_R0 x y). -unfold Un_cv in H; unfold Un_cv in |- *; intros. -cut (0 < eps / 4); - [ intro - | unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. -elim (H _ H1); intros N0 H2. -exists (max (2 * S N0) 2); intros. -unfold R_dist in H2; unfold R_dist in |- *; rewrite Rminus_0_r; - unfold Majxy in H2; unfold maj_Reste_E in |- *. -rewrite Rabs_right. -apply Rle_lt_trans with - (4 * +Proof. + intros; assert (H := Majxy_cv_R0 x y). + unfold Un_cv in H; unfold Un_cv in |- *; intros. + cut (0 < eps / 4); + [ intro + | unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. + elim (H _ H1); intros N0 H2. + exists (max (2 * S N0) 2); intros. + unfold R_dist in H2; unfold R_dist in |- *; rewrite Rminus_0_r; + unfold Majxy in H2; unfold maj_Reste_E in |- *. + rewrite Rabs_right. + apply Rle_lt_trans with + (4 * + (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S (div2 (pred n))) / + INR (fact (div2 (pred n))))). + apply Rmult_le_compat_l. + left; prove_sup0. + unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr. + rewrite (Rmult_comm (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (2 * n))); + rewrite + (Rmult_comm (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S (div2 (pred n))))) + ; rewrite Rmult_assoc; apply Rmult_le_compat_l. + left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. + apply Rle_trans with (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (2 * n)). + rewrite Rmult_comm; + pattern (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (2 * n)) at 2 in |- *; + rewrite <- Rmult_1_r; apply Rmult_le_compat_l. + apply pow_le; apply Rle_trans with 1. + left; apply Rlt_0_1. + apply RmaxLess1. + apply Rmult_le_reg_l with (INR (fact (div2 (pred n)))). + apply INR_fact_lt_0. + rewrite Rmult_1_r; rewrite <- Rinv_r_sym. + replace 1 with (INR 1); [ apply le_INR | reflexivity ]. + apply lt_le_S. + apply INR_lt. + apply INR_fact_lt_0. + apply INR_fact_neq_0. + apply Rle_pow. + apply RmaxLess1. + assert (H4 := even_odd_cor n). + elim H4; intros N1 H5. + elim H5; intro. + cut (0 < N1)%nat. + intro. + rewrite H6. + replace (pred (2 * N1)) with (S (2 * pred N1)). + rewrite div2_S_double. + omega. + omega. + assert (0 < n)%nat. + apply lt_le_trans with 2%nat. + apply lt_O_Sn. + apply le_trans with (max (2 * S N0) 2). + apply le_max_r. + apply H3. + omega. + rewrite H6. + replace (pred (S (2 * N1))) with (2 * N1)%nat. + rewrite div2_double. + replace (4 * S N1)%nat with (2 * (2 * S N1))%nat. + apply (fun m n p:nat => mult_le_compat_l p n m). + replace (2 * S N1)%nat with (S (S (2 * N1))). + apply le_n_Sn. + ring_nat. + ring_nat. + reflexivity. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + apply Rmult_lt_reg_l with (/ 4). + apply Rinv_0_lt_compat; prove_sup0. + rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. + rewrite Rmult_1_l; rewrite Rmult_comm. + replace (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S (div2 (pred n))) / - INR (fact (div2 (pred n))))). -apply Rmult_le_compat_l. -left; prove_sup0. -unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr. -rewrite (Rmult_comm (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (2 * n))); - rewrite - (Rmult_comm (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S (div2 (pred n))))) - ; rewrite Rmult_assoc; apply Rmult_le_compat_l. -left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. -apply Rle_trans with (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (2 * n)). -rewrite Rmult_comm; - pattern (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (2 * n)) at 2 in |- *; - rewrite <- Rmult_1_r; apply Rmult_le_compat_l. -apply pow_le; apply Rle_trans with 1. -left; apply Rlt_0_1. -apply RmaxLess1. -apply Rmult_le_reg_l with (INR (fact (div2 (pred n)))). -apply INR_fact_lt_0. -rewrite Rmult_1_r; rewrite <- Rinv_r_sym. -replace 1 with (INR 1); [ apply le_INR | reflexivity ]. -apply lt_le_S. -apply INR_lt. -apply INR_fact_lt_0. -apply INR_fact_neq_0. -apply Rle_pow. -apply RmaxLess1. -assert (H4 := even_odd_cor n). -elim H4; intros N1 H5. -elim H5; intro. -cut (0 < N1)%nat. -intro. -rewrite H6. -replace (pred (2 * N1)) with (S (2 * pred N1)). -rewrite div2_S_double. -replace (S (pred N1)) with N1. -apply INR_le. -right. -do 3 rewrite mult_INR; repeat rewrite S_INR; ring. -apply S_pred with 0%nat; apply H7. -replace (2 * N1)%nat with (S (S (2 * pred N1))). -reflexivity. -pattern N1 at 2 in |- *; replace N1 with (S (pred N1)). -apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; - ring. -symmetry in |- *; apply S_pred with 0%nat; apply H7. -apply INR_lt. -apply Rmult_lt_reg_l with (INR 2). -simpl in |- *; prove_sup0. -rewrite Rmult_0_r; rewrite <- mult_INR. -apply lt_INR_0. -rewrite <- H6. -apply lt_le_trans with 2%nat. -apply lt_O_Sn. -apply le_trans with (max (2 * S N0) 2). -apply le_max_r. -apply H3. -rewrite H6. -replace (pred (S (2 * N1))) with (2 * N1)%nat. -rewrite div2_double. -replace (4 * S N1)%nat with (2 * (2 * S N1))%nat. -apply (fun m n p:nat => mult_le_compat_l p n m). -replace (2 * S N1)%nat with (S (S (2 * N1))). -apply le_n_Sn. -apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; - ring. -ring. -reflexivity. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -apply Rmult_lt_reg_l with (/ 4). -apply Rinv_0_lt_compat; prove_sup0. -rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. -rewrite Rmult_1_l; rewrite Rmult_comm. -replace - (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S (div2 (pred n))) / - INR (fact (div2 (pred n)))) with - (Rabs + INR (fact (div2 (pred n)))) with + (Rabs (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S (div2 (pred n))) / - INR (fact (div2 (pred n))) - 0)). -apply H2; unfold ge in |- *. -cut (2 * S N0 <= n)%nat. -intro; apply le_S_n. -apply INR_le; apply Rmult_le_reg_l with (INR 2). -simpl in |- *; prove_sup0. -do 2 rewrite <- mult_INR; apply le_INR. -apply le_trans with n. -apply H4. -assert (H5 := even_odd_cor n). -elim H5; intros N1 H6. -elim H6; intro. -cut (0 < N1)%nat. -intro. -rewrite H7. -apply (fun m n p:nat => mult_le_compat_l p n m). -replace (pred (2 * N1)) with (S (2 * pred N1)). -rewrite div2_S_double. -replace (S (pred N1)) with N1. -apply le_n. -apply S_pred with 0%nat; apply H8. -replace (2 * N1)%nat with (S (S (2 * pred N1))). -reflexivity. -pattern N1 at 2 in |- *; replace N1 with (S (pred N1)). -apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; - ring. -symmetry in |- *; apply S_pred with 0%nat; apply H8. -apply INR_lt. -apply Rmult_lt_reg_l with (INR 2). -simpl in |- *; prove_sup0. -rewrite Rmult_0_r; rewrite <- mult_INR. -apply lt_INR_0. -rewrite <- H7. -apply lt_le_trans with 2%nat. -apply lt_O_Sn. -apply le_trans with (max (2 * S N0) 2). -apply le_max_r. -apply H3. -rewrite H7. -replace (pred (S (2 * N1))) with (2 * N1)%nat. -rewrite div2_double. -replace (2 * S N1)%nat with (S (S (2 * N1))). -apply le_n_Sn. -apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; - ring. -reflexivity. -apply le_trans with (max (2 * S N0) 2). -apply le_max_l. -apply H3. -rewrite Rminus_0_r; apply Rabs_right. -apply Rle_ge. -unfold Rdiv in |- *; repeat apply Rmult_le_pos. -apply pow_le. -apply Rle_trans with 1. -left; apply Rlt_0_1. -apply RmaxLess1. -left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. -discrR. -apply Rle_ge. -unfold Rdiv in |- *; apply Rmult_le_pos. -left; prove_sup0. -apply Rmult_le_pos. -apply pow_le. -apply Rle_trans with 1. -left; apply Rlt_0_1. -apply RmaxLess1. -left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt; apply INR_fact_neq_0. + INR (fact (div2 (pred n))) - 0)). + apply H2; unfold ge in |- *. + cut (2 * S N0 <= n)%nat. + intro; apply le_S_n. + apply INR_le; apply Rmult_le_reg_l with (INR 2). + simpl in |- *; prove_sup0. + do 2 rewrite <- mult_INR; apply le_INR. + apply le_trans with n. + apply H4. + assert (H5 := even_odd_cor n). + elim H5; intros N1 H6. + elim H6; intro. + cut (0 < N1)%nat. + intro. + rewrite H7. + apply (fun m n p:nat => mult_le_compat_l p n m). + replace (pred (2 * N1)) with (S (2 * pred N1)). + rewrite div2_S_double. + replace (S (pred N1)) with N1. + apply le_n. + apply S_pred with 0%nat; apply H8. + replace (2 * N1)%nat with (S (S (2 * pred N1))). + reflexivity. + pattern N1 at 2 in |- *; replace N1 with (S (pred N1)). + ring_nat. + symmetry in |- *; apply S_pred with 0%nat; apply H8. + apply INR_lt. + apply Rmult_lt_reg_l with (INR 2). + simpl in |- *; prove_sup0. + rewrite Rmult_0_r; rewrite <- mult_INR. + apply lt_INR_0. + rewrite <- H7. + apply lt_le_trans with 2%nat. + apply lt_O_Sn. + apply le_trans with (max (2 * S N0) 2). + apply le_max_r. + apply H3. + rewrite H7. + replace (pred (S (2 * N1))) with (2 * N1)%nat. + rewrite div2_double. + replace (2 * S N1)%nat with (S (S (2 * N1))). + apply le_n_Sn. + ring_nat. + reflexivity. + apply le_trans with (max (2 * S N0) 2). + apply le_max_l. + apply H3. + rewrite Rminus_0_r; apply Rabs_right. + apply Rle_ge. + unfold Rdiv in |- *; repeat apply Rmult_le_pos. + apply pow_le. + apply Rle_trans with 1. + left; apply Rlt_0_1. + apply RmaxLess1. + left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. + discrR. + apply Rle_ge. + unfold Rdiv in |- *; apply Rmult_le_pos. + left; prove_sup0. + apply Rmult_le_pos. + apply pow_le. + apply Rle_trans with 1. + left; apply Rlt_0_1. + apply RmaxLess1. + left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt; apply INR_fact_neq_0. Qed. (**********) Lemma Reste_E_cv : forall x y:R, Un_cv (Reste_E x y) 0. -intros; assert (H := maj_Reste_cv_R0 x y). -unfold Un_cv in H; unfold Un_cv in |- *; intros; elim (H _ H0); intros. -exists (max x0 1); intros. -unfold R_dist in |- *; rewrite Rminus_0_r. -apply Rle_lt_trans with (maj_Reste_E x y n). -apply Reste_E_maj. -apply lt_le_trans with 1%nat. -apply lt_O_Sn. -apply le_trans with (max x0 1). -apply le_max_r. -apply H2. -replace (maj_Reste_E x y n) with (R_dist (maj_Reste_E x y n) 0). -apply H1. -unfold ge in |- *; apply le_trans with (max x0 1). -apply le_max_l. -apply H2. -unfold R_dist in |- *; rewrite Rminus_0_r; apply Rabs_right. -apply Rle_ge; apply Rle_trans with (Rabs (Reste_E x y n)). -apply Rabs_pos. -apply Reste_E_maj. -apply lt_le_trans with 1%nat. -apply lt_O_Sn. -apply le_trans with (max x0 1). -apply le_max_r. -apply H2. +Proof. + intros; assert (H := maj_Reste_cv_R0 x y). + unfold Un_cv in H; unfold Un_cv in |- *; intros; elim (H _ H0); intros. + exists (max x0 1); intros. + unfold R_dist in |- *; rewrite Rminus_0_r. + apply Rle_lt_trans with (maj_Reste_E x y n). + apply Reste_E_maj. + apply lt_le_trans with 1%nat. + apply lt_O_Sn. + apply le_trans with (max x0 1). + apply le_max_r. + apply H2. + replace (maj_Reste_E x y n) with (R_dist (maj_Reste_E x y n) 0). + apply H1. + unfold ge in |- *; apply le_trans with (max x0 1). + apply le_max_l. + apply H2. + unfold R_dist in |- *; rewrite Rminus_0_r; apply Rabs_right. + apply Rle_ge; apply Rle_trans with (Rabs (Reste_E x y n)). + apply Rabs_pos. + apply Reste_E_maj. + apply lt_le_trans with 1%nat. + apply lt_O_Sn. + apply le_trans with (max x0 1). + apply le_max_r. + apply H2. Qed. (**********) Lemma exp_plus : forall x y:R, exp (x + y) = exp x * exp y. -intros; assert (H0 := E1_cvg x). -assert (H := E1_cvg y). -assert (H1 := E1_cvg (x + y)). -eapply UL_sequence. -apply H1. -assert (H2 := CV_mult _ _ _ _ H0 H). -assert (H3 := CV_minus _ _ _ _ H2 (Reste_E_cv x y)). -unfold Un_cv in |- *; unfold Un_cv in H3; intros. -elim (H3 _ H4); intros. -exists (S x0); intros. -rewrite <- (exp_form x y n). -rewrite Rminus_0_r in H5. -apply H5. -unfold ge in |- *; apply le_trans with (S x0). -apply le_n_Sn. -apply H6. -apply lt_le_trans with (S x0). -apply lt_O_Sn. -apply H6. +Proof. + intros; assert (H0 := E1_cvg x). + assert (H := E1_cvg y). + assert (H1 := E1_cvg (x + y)). + eapply UL_sequence. + apply H1. + assert (H2 := CV_mult _ _ _ _ H0 H). + assert (H3 := CV_minus _ _ _ _ H2 (Reste_E_cv x y)). + unfold Un_cv in |- *; unfold Un_cv in H3; intros. + elim (H3 _ H4); intros. + exists (S x0); intros. + rewrite <- (exp_form x y n). + rewrite Rminus_0_r in H5. + apply H5. + unfold ge in |- *; apply le_trans with (S x0). + apply le_n_Sn. + apply H6. + apply lt_le_trans with (S x0). + apply lt_O_Sn. + apply H6. Qed. (**********) Lemma exp_pos_pos : forall x:R, 0 < x -> 0 < exp x. -intros; set (An := fun N:nat => / INR (fact N) * x ^ N). -cut (Un_cv (fun n:nat => sum_f_R0 An n) (exp x)). -intro; apply Rlt_le_trans with (sum_f_R0 An 0). -unfold An in |- *; simpl in |- *; rewrite Rinv_1; rewrite Rmult_1_r; - apply Rlt_0_1. -apply sum_incr. -assumption. -intro; unfold An in |- *; left; apply Rmult_lt_0_compat. -apply Rinv_0_lt_compat; apply INR_fact_lt_0. -apply (pow_lt _ n H). -unfold exp in |- *; unfold projT1 in |- *; case (exist_exp x); intro. -unfold exp_in in |- *; unfold infinit_sum, Un_cv in |- *; trivial. +Proof. + intros; set (An := fun N:nat => / INR (fact N) * x ^ N). + cut (Un_cv (fun n:nat => sum_f_R0 An n) (exp x)). + intro; apply Rlt_le_trans with (sum_f_R0 An 0). + unfold An in |- *; simpl in |- *; rewrite Rinv_1; rewrite Rmult_1_r; + apply Rlt_0_1. + apply sum_incr. + assumption. + intro; unfold An in |- *; left; apply Rmult_lt_0_compat. + apply Rinv_0_lt_compat; apply INR_fact_lt_0. + apply (pow_lt _ n H). + unfold exp in |- *; unfold projT1 in |- *; case (exist_exp x); intro. + unfold exp_in in |- *; unfold infinit_sum, Un_cv in |- *; trivial. Qed. (**********) Lemma exp_pos : forall x:R, 0 < exp x. -intro; case (total_order_T 0 x); intro. -elim s; intro. -apply (exp_pos_pos _ a). -rewrite <- b; rewrite exp_0; apply Rlt_0_1. -replace (exp x) with (1 / exp (- x)). -unfold Rdiv in |- *; apply Rmult_lt_0_compat. -apply Rlt_0_1. -apply Rinv_0_lt_compat; apply exp_pos_pos. -apply (Ropp_0_gt_lt_contravar _ r). -cut (exp (- x) <> 0). -intro; unfold Rdiv in |- *; apply Rmult_eq_reg_l with (exp (- x)). -rewrite Rmult_1_l; rewrite <- Rinv_r_sym. -rewrite <- exp_plus. -rewrite Rplus_opp_l; rewrite exp_0; reflexivity. -apply H. -apply H. -assert (H := exp_plus x (- x)). -rewrite Rplus_opp_r in H; rewrite exp_0 in H. -red in |- *; intro; rewrite H0 in H. -rewrite Rmult_0_r in H. -elim R1_neq_R0; assumption. +Proof. + intro; case (total_order_T 0 x); intro. + elim s; intro. + apply (exp_pos_pos _ a). + rewrite <- b; rewrite exp_0; apply Rlt_0_1. + replace (exp x) with (1 / exp (- x)). + unfold Rdiv in |- *; apply Rmult_lt_0_compat. + apply Rlt_0_1. + apply Rinv_0_lt_compat; apply exp_pos_pos. + apply (Ropp_0_gt_lt_contravar _ r). + cut (exp (- x) <> 0). + intro; unfold Rdiv in |- *; apply Rmult_eq_reg_l with (exp (- x)). + rewrite Rmult_1_l; rewrite <- Rinv_r_sym. + rewrite <- exp_plus. + rewrite Rplus_opp_l; rewrite exp_0; reflexivity. + apply H. + apply H. + assert (H := exp_plus x (- x)). + rewrite Rplus_opp_r in H; rewrite exp_0 in H. + red in |- *; intro; rewrite H0 in H. + rewrite Rmult_0_r in H. + elim R1_neq_R0; assumption. Qed. (* ((exp h)-1)/h -> 0 quand h->0 *) Lemma derivable_pt_lim_exp_0 : derivable_pt_lim exp 0 1. -unfold derivable_pt_lim in |- *; intros. -set (fn := fun (N:nat) (x:R) => x ^ N / INR (fact (S N))). -cut (CVN_R fn). -intro; cut (forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)). -intro cv; cut (forall n:nat, continuity (fn n)). -intro; cut (continuity (SFL fn cv)). -intro; unfold continuity in H1. -assert (H2 := H1 0). -unfold continuity_pt in H2; unfold continue_in in H2; unfold limit1_in in H2; - unfold limit_in in H2; simpl in H2; unfold R_dist in H2. -elim (H2 _ H); intros alp H3. -elim H3; intros. -exists (mkposreal _ H4); intros. -rewrite Rplus_0_l; rewrite exp_0. -replace ((exp h - 1) / h) with (SFL fn cv h). -replace 1 with (SFL fn cv 0). -apply H5. -split. -unfold D_x, no_cond in |- *; split. -trivial. -apply (sym_not_eq H6). -rewrite Rminus_0_r; apply H7. -unfold SFL in |- *. -case (cv 0); intros. -eapply UL_sequence. -apply u. -unfold Un_cv, SP in |- *. -intros; exists 1%nat; intros. -unfold R_dist in |- *; rewrite decomp_sum. -rewrite (Rplus_comm (fn 0%nat 0)). -replace (fn 0%nat 0) with 1. -unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_r; - rewrite Rplus_0_r. -replace (sum_f_R0 (fun i:nat => fn (S i) 0) (pred n)) with 0. -rewrite Rabs_R0; apply H8. -symmetry in |- *; apply sum_eq_R0; intros. -unfold fn in |- *. -simpl in |- *. -unfold Rdiv in |- *; do 2 rewrite Rmult_0_l; reflexivity. -unfold fn in |- *; simpl in |- *. -unfold Rdiv in |- *; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. -apply lt_le_trans with 1%nat; [ apply lt_n_Sn | apply H9 ]. -unfold SFL, exp in |- *. -unfold projT1 in |- *. -case (cv h); case (exist_exp h); intros. -eapply UL_sequence. -apply u. -unfold Un_cv in |- *; intros. -unfold exp_in in e. -unfold infinit_sum in e. -cut (0 < eps0 * Rabs h). -intro; elim (e _ H9); intros N0 H10. -exists N0; intros. -unfold R_dist in |- *. -apply Rmult_lt_reg_l with (Rabs h). -apply Rabs_pos_lt; assumption. -rewrite <- Rabs_mult. -rewrite Rmult_minus_distr_l. -replace (h * ((x - 1) / h)) with (x - 1). -unfold R_dist in H10. -replace (h * SP fn n h - (x - 1)) with - (sum_f_R0 (fun i:nat => / INR (fact i) * h ^ i) (S n) - x). -rewrite (Rmult_comm (Rabs h)). -apply H10. -unfold ge in |- *. -apply le_trans with (S N0). -apply le_n_Sn. -apply le_n_S; apply H11. -rewrite decomp_sum. -replace (/ INR (fact 0) * h ^ 0) with 1. -unfold Rminus in |- *. -rewrite Ropp_plus_distr. -rewrite Ropp_involutive. -rewrite <- (Rplus_comm (- x)). -rewrite <- (Rplus_comm (- x + 1)). -rewrite Rplus_assoc; repeat apply Rplus_eq_compat_l. -replace (pred (S n)) with n; [ idtac | reflexivity ]. -unfold SP in |- *. -rewrite scal_sum. -apply sum_eq; intros. -unfold fn in |- *. -replace (h ^ S i) with (h * h ^ i). -unfold Rdiv in |- *; ring. -simpl in |- *; ring. -simpl in |- *; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. -apply lt_O_Sn. -unfold Rdiv in |- *. -rewrite <- Rmult_assoc. -symmetry in |- *; apply Rinv_r_simpl_m. -assumption. -apply Rmult_lt_0_compat. -apply H8. -apply Rabs_pos_lt; assumption. -apply SFL_continuity; assumption. -intro; unfold fn in |- *. -replace (fun x:R => x ^ n / INR (fact (S n))) with - (pow_fct n / fct_cte (INR (fact (S n))))%F; [ idtac | reflexivity ]. -apply continuity_div. -apply derivable_continuous; apply (derivable_pow n). -apply derivable_continuous; apply derivable_const. -intro; unfold fct_cte in |- *; apply INR_fact_neq_0. -apply (CVN_R_CVS _ X). -assert (H0 := Alembert_exp). -unfold CVN_R in |- *. -intro; unfold CVN_r in |- *. -apply existT with (fun N:nat => r ^ N / INR (fact (S N))). -cut - (sigT - (fun l:R => - Un_cv - (fun n:nat => - sum_f_R0 (fun k:nat => Rabs (r ^ k / INR (fact (S k)))) n) l)). -intro X. -elim X; intros. -exists x; intros. -split. -apply p. -unfold Boule in |- *; intros. -rewrite Rminus_0_r in H1. -unfold fn in |- *. -unfold Rdiv in |- *; rewrite Rabs_mult. -cut (0 < INR (fact (S n))). -intro. -rewrite (Rabs_right (/ INR (fact (S n)))). -do 2 rewrite <- (Rmult_comm (/ INR (fact (S n)))). -apply Rmult_le_compat_l. -left; apply Rinv_0_lt_compat; apply H2. -rewrite <- RPow_abs. -apply pow_maj_Rabs. -rewrite Rabs_Rabsolu; left; apply H1. -apply Rle_ge; left; apply Rinv_0_lt_compat; apply H2. -apply INR_fact_lt_0. -cut ((r:R) <> 0). -intro; apply Alembert_C2. -intro; apply Rabs_no_R0. -unfold Rdiv in |- *; apply prod_neq_R0. -apply pow_nonzero; assumption. -apply Rinv_neq_0_compat; apply INR_fact_neq_0. -unfold Un_cv in H0. -unfold Un_cv in |- *; intros. -cut (0 < eps0 / r); - [ intro - | unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ assumption | apply Rinv_0_lt_compat; apply (cond_pos r) ] ]. -elim (H0 _ H3); intros N0 H4. -exists N0; intros. -cut (S n >= N0)%nat. -intro hyp_sn. -assert (H6 := H4 _ hyp_sn). -unfold R_dist in H6; rewrite Rminus_0_r in H6. -rewrite Rabs_Rabsolu in H6. -unfold R_dist in |- *; rewrite Rminus_0_r. -rewrite Rabs_Rabsolu. -replace - (Rabs (r ^ S n / INR (fact (S (S n)))) / Rabs (r ^ n / INR (fact (S n)))) - with (r * / INR (fact (S (S n))) * / / INR (fact (S n))). -rewrite Rmult_assoc; rewrite Rabs_mult. -rewrite (Rabs_right r). -apply Rmult_lt_reg_l with (/ r). -apply Rinv_0_lt_compat; apply (cond_pos r). -rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. -rewrite Rmult_1_l; rewrite <- (Rmult_comm eps0). -apply H6. -assumption. -apply Rle_ge; left; apply (cond_pos r). -unfold Rdiv in |- *. -repeat rewrite Rabs_mult. -repeat rewrite Rabs_Rinv. -rewrite Rinv_mult_distr. -repeat rewrite Rabs_right. -rewrite Rinv_involutive. -rewrite (Rmult_comm r). -rewrite (Rmult_comm (r ^ S n)). -repeat rewrite Rmult_assoc. -apply Rmult_eq_compat_l. -rewrite (Rmult_comm r). -rewrite <- Rmult_assoc; rewrite <- (Rmult_comm (INR (fact (S n)))). -apply Rmult_eq_compat_l. -simpl in |- *. -rewrite Rmult_assoc; rewrite <- Rinv_r_sym. -ring. -apply pow_nonzero; assumption. -apply INR_fact_neq_0. -apply Rle_ge; left; apply INR_fact_lt_0. -apply Rle_ge; left; apply pow_lt; apply (cond_pos r). -apply Rle_ge; left; apply INR_fact_lt_0. -apply Rle_ge; left; apply pow_lt; apply (cond_pos r). -apply Rabs_no_R0; apply pow_nonzero; assumption. -apply Rinv_neq_0_compat; apply Rabs_no_R0; apply INR_fact_neq_0. -apply INR_fact_neq_0. -apply INR_fact_neq_0. -unfold ge in |- *; apply le_trans with n. -apply H5. -apply le_n_Sn. -assert (H1 := cond_pos r); red in |- *; intro; rewrite H2 in H1; - elim (Rlt_irrefl _ H1). +Proof. + unfold derivable_pt_lim in |- *; intros. + set (fn := fun (N:nat) (x:R) => x ^ N / INR (fact (S N))). + cut (CVN_R fn). + intro; cut (forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)). + intro cv; cut (forall n:nat, continuity (fn n)). + intro; cut (continuity (SFL fn cv)). + intro; unfold continuity in H1. + assert (H2 := H1 0). + unfold continuity_pt in H2; unfold continue_in in H2; unfold limit1_in in H2; + unfold limit_in in H2; simpl in H2; unfold R_dist in H2. + elim (H2 _ H); intros alp H3. + elim H3; intros. + exists (mkposreal _ H4); intros. + rewrite Rplus_0_l; rewrite exp_0. + replace ((exp h - 1) / h) with (SFL fn cv h). + replace 1 with (SFL fn cv 0). + apply H5. + split. + unfold D_x, no_cond in |- *; split. + trivial. + apply (sym_not_eq H6). + rewrite Rminus_0_r; apply H7. + unfold SFL in |- *. + case (cv 0); intros. + eapply UL_sequence. + apply u. + unfold Un_cv, SP in |- *. + intros; exists 1%nat; intros. + unfold R_dist in |- *; rewrite decomp_sum. + rewrite (Rplus_comm (fn 0%nat 0)). + replace (fn 0%nat 0) with 1. + unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_r; + rewrite Rplus_0_r. + replace (sum_f_R0 (fun i:nat => fn (S i) 0) (pred n)) with 0. + rewrite Rabs_R0; apply H8. + symmetry in |- *; apply sum_eq_R0; intros. + unfold fn in |- *. + simpl in |- *. + unfold Rdiv in |- *; do 2 rewrite Rmult_0_l; reflexivity. + unfold fn in |- *; simpl in |- *. + unfold Rdiv in |- *; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. + apply lt_le_trans with 1%nat; [ apply lt_n_Sn | apply H9 ]. + unfold SFL, exp in |- *. + unfold projT1 in |- *. + case (cv h); case (exist_exp h); intros. + eapply UL_sequence. + apply u. + unfold Un_cv in |- *; intros. + unfold exp_in in e. + unfold infinit_sum in e. + cut (0 < eps0 * Rabs h). + intro; elim (e _ H9); intros N0 H10. + exists N0; intros. + unfold R_dist in |- *. + apply Rmult_lt_reg_l with (Rabs h). + apply Rabs_pos_lt; assumption. + rewrite <- Rabs_mult. + rewrite Rmult_minus_distr_l. + replace (h * ((x - 1) / h)) with (x - 1). + unfold R_dist in H10. + replace (h * SP fn n h - (x - 1)) with + (sum_f_R0 (fun i:nat => / INR (fact i) * h ^ i) (S n) - x). + rewrite (Rmult_comm (Rabs h)). + apply H10. + unfold ge in |- *. + apply le_trans with (S N0). + apply le_n_Sn. + apply le_n_S; apply H11. + rewrite decomp_sum. + replace (/ INR (fact 0) * h ^ 0) with 1. + unfold Rminus in |- *. + rewrite Ropp_plus_distr. + rewrite Ropp_involutive. + rewrite <- (Rplus_comm (- x)). + rewrite <- (Rplus_comm (- x + 1)). + rewrite Rplus_assoc; repeat apply Rplus_eq_compat_l. + replace (pred (S n)) with n; [ idtac | reflexivity ]. + unfold SP in |- *. + rewrite scal_sum. + apply sum_eq; intros. + unfold fn in |- *. + replace (h ^ S i) with (h * h ^ i). + unfold Rdiv in |- *; ring. + simpl in |- *; ring. + simpl in |- *; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. + apply lt_O_Sn. + unfold Rdiv in |- *. + rewrite <- Rmult_assoc. + symmetry in |- *; apply Rinv_r_simpl_m. + assumption. + apply Rmult_lt_0_compat. + apply H8. + apply Rabs_pos_lt; assumption. + apply SFL_continuity; assumption. + intro; unfold fn in |- *. + replace (fun x:R => x ^ n / INR (fact (S n))) with + (pow_fct n / fct_cte (INR (fact (S n))))%F; [ idtac | reflexivity ]. + apply continuity_div. + apply derivable_continuous; apply (derivable_pow n). + apply derivable_continuous; apply derivable_const. + intro; unfold fct_cte in |- *; apply INR_fact_neq_0. + apply (CVN_R_CVS _ X). + assert (H0 := Alembert_exp). + unfold CVN_R in |- *. + intro; unfold CVN_r in |- *. + apply existT with (fun N:nat => r ^ N / INR (fact (S N))). + cut + (sigT + (fun l:R => + Un_cv + (fun n:nat => + sum_f_R0 (fun k:nat => Rabs (r ^ k / INR (fact (S k)))) n) l)). + intro X. + elim X; intros. + exists x; intros. + split. + apply p. + unfold Boule in |- *; intros. + rewrite Rminus_0_r in H1. + unfold fn in |- *. + unfold Rdiv in |- *; rewrite Rabs_mult. + cut (0 < INR (fact (S n))). + intro. + rewrite (Rabs_right (/ INR (fact (S n)))). + do 2 rewrite <- (Rmult_comm (/ INR (fact (S n)))). + apply Rmult_le_compat_l. + left; apply Rinv_0_lt_compat; apply H2. + rewrite <- RPow_abs. + apply pow_maj_Rabs. + rewrite Rabs_Rabsolu; left; apply H1. + apply Rle_ge; left; apply Rinv_0_lt_compat; apply H2. + apply INR_fact_lt_0. + cut ((r:R) <> 0). + intro; apply Alembert_C2. + intro; apply Rabs_no_R0. + unfold Rdiv in |- *; apply prod_neq_R0. + apply pow_nonzero; assumption. + apply Rinv_neq_0_compat; apply INR_fact_neq_0. + unfold Un_cv in H0. + unfold Un_cv in |- *; intros. + cut (0 < eps0 / r); + [ intro + | unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ assumption | apply Rinv_0_lt_compat; apply (cond_pos r) ] ]. + elim (H0 _ H3); intros N0 H4. + exists N0; intros. + cut (S n >= N0)%nat. + intro hyp_sn. + assert (H6 := H4 _ hyp_sn). + unfold R_dist in H6; rewrite Rminus_0_r in H6. + rewrite Rabs_Rabsolu in H6. + unfold R_dist in |- *; rewrite Rminus_0_r. + rewrite Rabs_Rabsolu. + replace + (Rabs (r ^ S n / INR (fact (S (S n)))) / Rabs (r ^ n / INR (fact (S n)))) + with (r * / INR (fact (S (S n))) * / / INR (fact (S n))). + rewrite Rmult_assoc; rewrite Rabs_mult. + rewrite (Rabs_right r). + apply Rmult_lt_reg_l with (/ r). + apply Rinv_0_lt_compat; apply (cond_pos r). + rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. + rewrite Rmult_1_l; rewrite <- (Rmult_comm eps0). + apply H6. + assumption. + apply Rle_ge; left; apply (cond_pos r). + unfold Rdiv in |- *. + repeat rewrite Rabs_mult. + repeat rewrite Rabs_Rinv. + rewrite Rinv_mult_distr. + repeat rewrite Rabs_right. + rewrite Rinv_involutive. + rewrite (Rmult_comm r). + rewrite (Rmult_comm (r ^ S n)). + repeat rewrite Rmult_assoc. + apply Rmult_eq_compat_l. + rewrite (Rmult_comm r). + rewrite <- Rmult_assoc; rewrite <- (Rmult_comm (INR (fact (S n)))). + apply Rmult_eq_compat_l. + simpl in |- *. + rewrite Rmult_assoc; rewrite <- Rinv_r_sym. + ring. + apply pow_nonzero; assumption. + apply INR_fact_neq_0. + apply Rle_ge; left; apply INR_fact_lt_0. + apply Rle_ge; left; apply pow_lt; apply (cond_pos r). + apply Rle_ge; left; apply INR_fact_lt_0. + apply Rle_ge; left; apply pow_lt; apply (cond_pos r). + apply Rabs_no_R0; apply pow_nonzero; assumption. + apply Rinv_neq_0_compat; apply Rabs_no_R0; apply INR_fact_neq_0. + apply INR_fact_neq_0. + apply INR_fact_neq_0. + unfold ge in |- *; apply le_trans with n. + apply H5. + apply le_n_Sn. + assert (H1 := cond_pos r); red in |- *; intro; rewrite H2 in H1; + elim (Rlt_irrefl _ H1). Qed. (**********) Lemma derivable_pt_lim_exp : forall x:R, derivable_pt_lim exp x (exp x). -intro; assert (H0 := derivable_pt_lim_exp_0). -unfold derivable_pt_lim in H0; unfold derivable_pt_lim in |- *; intros. -cut (0 < eps / exp x); - [ intro - | unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ apply H | apply Rinv_0_lt_compat; apply exp_pos ] ]. -elim (H0 _ H1); intros del H2. -exists del; intros. -assert (H5 := H2 _ H3 H4). -rewrite Rplus_0_l in H5; rewrite exp_0 in H5. -replace ((exp (x + h) - exp x) / h - exp x) with - (exp x * ((exp h - 1) / h - 1)). -rewrite Rabs_mult; rewrite (Rabs_right (exp x)). -apply Rmult_lt_reg_l with (/ exp x). -apply Rinv_0_lt_compat; apply exp_pos. -rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. -rewrite Rmult_1_l; rewrite <- (Rmult_comm eps). -apply H5. -assert (H6 := exp_pos x); red in |- *; intro; rewrite H7 in H6; - elim (Rlt_irrefl _ H6). -apply Rle_ge; left; apply exp_pos. -rewrite Rmult_minus_distr_l. -rewrite Rmult_1_r; unfold Rdiv in |- *; rewrite <- Rmult_assoc; - rewrite Rmult_minus_distr_l. -rewrite Rmult_1_r; rewrite exp_plus; reflexivity. +Proof. + intro; assert (H0 := derivable_pt_lim_exp_0). + unfold derivable_pt_lim in H0; unfold derivable_pt_lim in |- *; intros. + cut (0 < eps / exp x); + [ intro + | unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ apply H | apply Rinv_0_lt_compat; apply exp_pos ] ]. + elim (H0 _ H1); intros del H2. + exists del; intros. + assert (H5 := H2 _ H3 H4). + rewrite Rplus_0_l in H5; rewrite exp_0 in H5. + replace ((exp (x + h) - exp x) / h - exp x) with + (exp x * ((exp h - 1) / h - 1)). + rewrite Rabs_mult; rewrite (Rabs_right (exp x)). + apply Rmult_lt_reg_l with (/ exp x). + apply Rinv_0_lt_compat; apply exp_pos. + rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. + rewrite Rmult_1_l; rewrite <- (Rmult_comm eps). + apply H5. + assert (H6 := exp_pos x); red in |- *; intro; rewrite H7 in H6; + elim (Rlt_irrefl _ H6). + apply Rle_ge; left; apply exp_pos. + rewrite Rmult_minus_distr_l. + rewrite Rmult_1_r; unfold Rdiv in |- *; rewrite <- Rmult_assoc; + rewrite Rmult_minus_distr_l. + rewrite Rmult_1_r; rewrite exp_plus; reflexivity. Qed. |