diff options
Diffstat (limited to 'theories7/Reals/Exp_prop.v')
| -rw-r--r-- | theories7/Reals/Exp_prop.v | 890 |
1 files changed, 0 insertions, 890 deletions
diff --git a/theories7/Reals/Exp_prop.v b/theories7/Reals/Exp_prop.v deleted file mode 100644 index 6ed9c00b..00000000 --- a/theories7/Reals/Exp_prop.v +++ /dev/null @@ -1,890 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Exp_prop.v,v 1.1.2.1 2004/07/16 19:31:32 herbelin Exp $ i*) - -Require Rbase. -Require Rfunctions. -Require SeqSeries. -Require Rtrigo. -Require Ranalysis1. -Require PSeries_reg. -Require Div2. -Require Even. -Require Max. -V7only [Import R_scope.]. -Open Local Scope nat_scope. -V7only [Import nat_scope.]. -Open Local Scope R_scope. - -Definition E1 [x:R] : nat->R := [N:nat](sum_f_R0 [k:nat]``/(INR (fact k))*(pow x k)`` N). - -Lemma E1_cvg : (x:R) (Un_cv (E1 x) (exp x)). -Intro; Unfold exp; Unfold projT1. -Case (exist_exp x); Intro. -Unfold exp_in Un_cv; Unfold infinit_sum E1; Trivial. -Qed. - -Definition Reste_E [x,y:R] : nat->R := [N:nat](sum_f_R0 [k:nat](sum_f_R0 [l:nat]``/(INR (fact (S (plus l k))))*(pow x (S (plus l k)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))`` (pred (minus N k))) (pred N)). - -Lemma exp_form : (x,y:R;n:nat) (lt O n) -> ``(E1 x n)*(E1 y n)-(Reste_E x y n)==(E1 (x+y) n)``. -Intros; Unfold E1. -Rewrite cauchy_finite. -Unfold Reste_E; Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Or; Apply sum_eq; Intros. -Rewrite binomial. -Rewrite scal_sum; Apply sum_eq; Intros. -Unfold C; Unfold Rdiv; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym (INR (fact i))); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Rewrite Rinv_Rmult. -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] : nat->R := [N:nat]``4*(pow (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S O)) N))/(Rsqr (INR (fact (div2 (pred N)))))``. - -Lemma Rle_Rinv : (x,y:R) ``0<x`` -> ``0<y`` -> ``x<=y`` -> ``/y<=/x``. -Intros; Apply Rle_monotony_contra with x. -Apply H. -Rewrite <- Rinv_r_sym. -Apply Rle_monotony_contra with y. -Apply H0. -Rewrite Rmult_1r; Rewrite Rmult_sym; Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Apply H1. -Red; Intro; Rewrite H2 in H0; Elim (Rlt_antirefl ? H0). -Red; Intro; Rewrite H2 in H; Elim (Rlt_antirefl ? H). -Qed. - -(**********) -Lemma div2_double : (N:nat) (div2 (mult (2) N))=N. -Intro; Induction N. -Reflexivity. -Replace (mult (2) (S N)) with (S (S (mult (2) N))). -Simpl; Simpl in HrecN; Rewrite HrecN; Reflexivity. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Qed. - -Lemma div2_S_double : (N:nat) (div2 (S (mult (2) N)))=N. -Intro; Induction N. -Reflexivity. -Replace (mult (2) (S N)) with (S (S (mult (2) N))). -Simpl; Simpl in HrecN; Rewrite HrecN; Reflexivity. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Qed. - -Lemma div2_not_R0 : (N:nat) (lt (1) N) -> (lt O (div2 N)). -Intros; Induction N. -Elim (lt_n_O ? H). -Cut (lt (1) N)\/N=(1). -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; Apply lt_O_Sn. -Inversion H. -Right; Reflexivity. -Left; Apply lt_le_trans with (2); [Apply lt_n_Sn | Apply H1]. -Qed. - -Lemma Reste_E_maj : (x,y:R;N:nat) (lt O N) -> ``(Rabsolu (Reste_E x y N))<=(maj_Reste_E x y N)``. -Intros; Pose M := (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))). -Apply Rle_trans with (Rmult (pow M (mult (2) N)) (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``/(Rsqr (INR (fact (div2 (S N)))))`` (pred (minus N k))) (pred N))). -Unfold Reste_E. -Apply Rle_trans with (sum_f_R0 [k:nat](Rabsolu (sum_f_R0 [l:nat]``/(INR (fact (S (plus l k))))*(pow x (S (plus l k)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))`` (pred (minus N k)))) (pred N)). -Apply (sum_Rabsolu [k:nat](sum_f_R0 [l:nat]``/(INR (fact (S (plus l k))))*(pow x (S (plus l k)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))`` (pred (minus N k))) (pred N)). -Apply Rle_trans with (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(Rabsolu (/(INR (fact (S (plus l k))))*(pow x (S (plus l k)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))))`` (pred (minus N k))) (pred N)). -Apply sum_Rle; Intros. -Apply (sum_Rabsolu [l:nat]``/(INR (fact (S (plus l n))))*(pow x (S (plus l n)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))``). -Apply Rle_trans with (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(pow M (mult (S (S O)) N))*/(INR (fact (S l)))*/(INR (fact (minus N l)))`` (pred (minus N k))) (pred N)). -Apply sum_Rle; Intros. -Apply sum_Rle; Intros. -Repeat Rewrite Rabsolu_mult. -Do 2 Rewrite <- Pow_Rabsolu. -Rewrite (Rabsolu_right ``/(INR (fact (S (plus n0 n))))``). -Rewrite (Rabsolu_right ``/(INR (fact (minus N n0)))``). -Replace ``/(INR (fact (S (plus n0 n))))*(pow (Rabsolu x) (S (plus n0 n)))* - (/(INR (fact (minus N n0)))*(pow (Rabsolu y) (minus N n0)))`` with ``/(INR (fact (minus N n0)))*/(INR (fact (S (plus n0 n))))*(pow (Rabsolu x) (S (plus n0 n)))*(pow (Rabsolu y) (minus N n0))``; [Idtac | Ring]. -Rewrite <- (Rmult_sym ``/(INR (fact (minus N n0)))``). -Repeat Rewrite Rmult_assoc. -Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Apply Rle_trans with ``/(INR (fact (S n0)))*(pow (Rabsolu x) (S (plus n0 n)))*(pow (Rabsolu y) (minus N n0))``. -Rewrite (Rmult_sym ``/(INR (fact (S (plus n0 n))))``); Rewrite (Rmult_sym ``/(INR (fact (S n0)))``); Repeat Rewrite Rmult_assoc; Apply Rle_monotony. -Apply pow_le; Apply Rabsolu_pos. -Rewrite (Rmult_sym ``/(INR (fact (S n0)))``); Apply Rle_monotony. -Apply pow_le; Apply Rabsolu_pos. -Apply Rle_Rinv. -Apply INR_fact_lt_0. -Apply INR_fact_lt_0. -Apply le_INR; Apply fact_growing; Apply le_n_S. -Apply le_plus_l. -Rewrite (Rmult_sym ``(pow M (mult (S (S O)) N))``); Rewrite Rmult_assoc; Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Apply Rle_trans with ``(pow M (S (plus n0 n)))*(pow (Rabsolu y) (minus N n0))``. -Do 2 Rewrite <- (Rmult_sym ``(pow (Rabsolu y) (minus N n0))``). -Apply Rle_monotony. -Apply pow_le; Apply Rabsolu_pos. -Apply pow_incr; Split. -Apply Rabsolu_pos. -Apply Rle_trans with (Rmax (Rabsolu x) (Rabsolu y)). -Apply RmaxLess1. -Unfold M; Apply RmaxLess2. -Apply Rle_trans with ``(pow M (S (plus n0 n)))*(pow M (minus N n0))``. -Apply Rle_monotony. -Apply pow_le; Apply Rle_trans with R1. -Left; Apply Rlt_R0_R1. -Unfold M; Apply RmaxLess1. -Apply pow_incr; Split. -Apply Rabsolu_pos. -Apply Rle_trans with (Rmax (Rabsolu x) (Rabsolu y)). -Apply RmaxLess2. -Unfold M; Apply RmaxLess2. -Rewrite <- pow_add; Replace (plus (S (plus n0 n)) (minus N n0)) with (plus N (S n)). -Apply Rle_pow. -Unfold M; Apply RmaxLess1. -Replace (mult (2) N) with (plus N N); [Idtac | Ring]. -Apply le_reg_l. -Replace N with (S (pred N)). -Apply le_n_S; Apply H0. -Symmetry; Apply S_pred with O; 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 (minus N n)). -Apply H1. -Apply le_S_n. -Replace (S (pred (minus N n))) with (minus N n). -Apply le_trans with N. -Apply simpl_le_plus_l 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 O. -Apply simpl_lt_plus_l with n. -Rewrite <- le_plus_minus. -Replace (plus n (0)) 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_sym1; Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Rewrite scal_sum. -Apply sum_Rle; Intros. -Rewrite <- Rmult_sym. -Rewrite scal_sum. -Apply sum_Rle; Intros. -Rewrite (Rmult_sym ``/(Rsqr (INR (fact (div2 (S N)))))``). -Rewrite Rmult_assoc; Apply Rle_monotony. -Apply pow_le. -Apply Rle_trans with R1. -Left; Apply Rlt_R0_R1. -Unfold M; 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 (minus N n0)))``. -Do 2 Rewrite <- (Rmult_sym ``/(INR (fact (minus N n0)))``). -Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Apply Rle_Rinv. -Apply INR_fact_lt_0. -Apply INR_fact_lt_0. -Apply le_INR. -Apply fact_growing. -Apply le_n_Sn. -Replace ``/(INR (fact n0))*/(INR (fact (minus N n0)))`` with ``(C N n0)/(INR (fact N))``. -Pattern 1 N; Rewrite H4. -Apply Rle_trans with ``(C N N0)/(INR (fact N))``. -Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/(INR (fact N))``). -Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Rewrite H4. -Apply C_maj. -Rewrite <- H4; Apply le_trans with (pred (minus N n)). -Apply H1. -Apply le_S_n. -Replace (S (pred (minus N n))) with (minus N n). -Apply le_trans with N. -Apply simpl_le_plus_l 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 O. -Apply simpl_lt_plus_l with n. -Rewrite <- le_plus_minus. -Replace (plus n (0)) 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. -Repeat Rewrite Rinv_Rmult. -Rewrite (Rmult_sym (INR (fact N))). -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Replace (minus N N0) with N0. -Ring. -Replace N with (plus N0 N0). -Symmetry; 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. -Rewrite (Rmult_sym (INR (fact N))). -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_r_sym. -Rewrite Rinv_Rmult. -Rewrite Rmult_1r; Ring. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Replace ``/(INR (fact (S n0)))*/(INR (fact (minus 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; Do 2 Rewrite <- (Rmult_sym ``/(INR (fact (S N)))``). -Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Cut (S N) = (mult (2) (S N0)). -Intro; Rewrite H5; Apply C_maj. -Rewrite <- H5; Apply le_n_S. -Apply le_trans with (pred (minus N n)). -Apply H1. -Apply le_S_n. -Replace (S (pred (minus N n))) with (minus N n). -Apply le_trans with N. -Apply simpl_le_plus_l 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 O. -Apply simpl_lt_plus_l with n. -Rewrite <- le_plus_minus. -Replace (plus n (0)) 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) = (mult (2) (S N0)). -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. -Repeat Rewrite Rinv_Rmult. -Replace (minus (S N) (S N0)) with (S N0). -Rewrite (Rmult_sym (INR (fact (S N)))). -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Reflexivity. -Apply INR_fact_neq_0. -Replace (S N) with (plus (S N0) (S N0)). -Symmetry; 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. -Rewrite (Rmult_sym (INR (fact (S N)))). -Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Rewrite Rinv_Rmult. -Reflexivity. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Unfold maj_Reste_E. -Unfold Rdiv; Rewrite (Rmult_sym ``4``). -Rewrite Rmult_assoc. -Apply Rle_monotony. -Apply pow_le. -Apply Rle_trans with R1. -Left; Apply Rlt_R0_R1. -Apply RmaxLess1. -Apply Rle_trans with (sum_f_R0 [k:nat]``(INR (minus N k))*/(Rsqr (INR (fact (div2 (S N)))))`` (pred N)). -Apply sum_Rle; Intros. -Rewrite sum_cte. -Replace (S (pred (minus N n))) with (minus N n). -Right; Apply Rmult_sym. -Apply S_pred with O. -Apply simpl_lt_plus_l with n. -Rewrite <- le_plus_minus. -Replace (plus n (0)) 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 [k:nat]``(INR N)*/(Rsqr (INR (fact (div2 (S N)))))`` (pred N)). -Apply sum_Rle; Intros. -Do 2 Rewrite <- (Rmult_sym ``/(Rsqr (INR (fact (div2 (S N)))))``). -Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply Rsqr_pos_lt. -Apply INR_fact_neq_0. -Apply le_INR. -Apply simpl_le_plus_l 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_sym; Rewrite mult_INR; Rewrite Rsqr_times. -Rewrite Rinv_Rmult. -Rewrite (Rmult_sym (INR N)); Repeat Rewrite Rmult_assoc; Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply Rsqr_pos_lt; Apply INR_fact_neq_0. -Rewrite <- H0. -Cut ``(INR N)<=(INR (mult (S (S O)) (div2 (S N))))``. -Intro; Apply Rle_monotony_contra with ``(Rsqr (INR (div2 (S N))))``. -Apply Rsqr_pos_lt. -Apply not_O_INR; Red; Intro. -Cut (lt (1) (S N)). -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_1l. -Replace ``(INR N)*(INR N)`` with (Rsqr (INR N)); [Idtac | Reflexivity]. -Rewrite Rmult_assoc. -Rewrite Rmult_sym. -Replace ``4`` with (Rsqr ``2``); [Idtac | SqRing]. -Rewrite <- Rsqr_times. -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_pos. -Sup0. -Apply lt_INR_0; Apply div2_not_R0. -Apply lt_n_S; Apply H. -Cut (lt (1) (S N)). -Intro; Unfold Rsqr; 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 2 N; Rewrite H3. -Rewrite div2_S_double. -Right; Rewrite H3; Reflexivity. -Pattern 2 N; Rewrite H3. -Replace (S (S (mult (2) N0))) with (mult (2) (S N0)). -Rewrite div2_double. -Rewrite H3. -Rewrite S_INR; Do 2 Rewrite mult_INR. -Rewrite (S_INR N0). -Rewrite Rmult_Rplus_distr. -Apply Rle_compatibility. -Rewrite Rmult_1r. -Simpl. -Pattern 1 R1; Rewrite <- Rplus_Or; Apply Rle_compatibility; Left; Apply Rlt_R0_R1. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Unfold Rsqr; Apply prod_neq_R0; Apply INR_fact_neq_0. -Unfold Rsqr; Apply prod_neq_R0; Apply not_O_INR; Discriminate. -Assert H0 := (even_odd_cor N). -Elim H0; Intros N0 H1. -Elim H1; Intro. -Cut (lt O N0). -Intro; Rewrite H2. -Rewrite div2_S_double. -Replace (mult (2) N0) with (S (S (mult (2) (pred N0)))). -Replace (pred (S (S (mult (2) (pred N0))))) with (S (mult (2) (pred N0))). -Rewrite div2_S_double. -Apply S_pred with O; 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; Apply S_pred with O; Apply H3. -Rewrite H2 in H. -Apply neq_O_lt. -Red; Intro. -Rewrite <- H3 in H. -Simpl in H. -Elim (lt_n_O ? H). -Rewrite H2. -Replace (pred (S (mult (2) N0))) with (mult (2) N0); [Idtac | Reflexivity]. -Replace (S (S (mult (2) N0))) with (mult (2) (S N0)). -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 O; Apply H. -Qed. - -Lemma maj_Reste_cv_R0 : (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; Intros. -Cut ``0<eps/4``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]]. -Elim (H ? H1); Intros N0 H2. -Exists (max (mult (2) (S N0)) (2)); Intros. -Unfold R_dist in H2; Unfold R_dist; Rewrite minus_R0; Unfold Majxy in H2; Unfold maj_Reste_E. -Rewrite Rabsolu_right. -Apply Rle_lt_trans with ``4*(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S (S (S O)))) (S (div2 (pred n)))))/(INR (fact (div2 (pred n))))``. -Apply Rle_monotony. -Left; Sup0. -Unfold Rdiv Rsqr; Rewrite Rinv_Rmult. -Rewrite (Rmult_sym ``(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S O)) n))``); Rewrite (Rmult_sym ``(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S (S (S O)))) (S (div2 (pred n)))))``); Rewrite Rmult_assoc; Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Apply Rle_trans with ``(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S O)) n))``. -Rewrite Rmult_sym; Pattern 2 (pow (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (2) n)); Rewrite <- Rmult_1r; Apply Rle_monotony. -Apply pow_le; Apply Rle_trans with R1. -Left; Apply Rlt_R0_R1. -Apply RmaxLess1. -Apply Rle_monotony_contra with ``(INR (fact (div2 (pred n))))``. -Apply INR_fact_lt_0. -Rewrite Rmult_1r; Rewrite <- Rinv_r_sym. -Replace R1 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 (lt O N1). -Intro. -Rewrite H6. -Replace (pred (mult (2) N1)) with (S (mult (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 O; Apply H7. -Replace (mult (2) N1) with (S (S (mult (2) (pred N1)))). -Reflexivity. -Pattern 2 N1; 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 ; Apply S_pred with O; Apply H7. -Apply INR_lt. -Apply Rlt_monotony_contra with (INR (2)). -Simpl; Sup0. -Rewrite Rmult_Or; Rewrite <- mult_INR. -Apply lt_INR_0. -Rewrite <- H6. -Apply lt_le_trans with (2). -Apply lt_O_Sn. -Apply le_trans with (max (mult (2) (S N0)) (2)). -Apply le_max_r. -Apply H3. -Rewrite H6. -Replace (pred (S (mult (2) N1))) with (mult (2) N1). -Rewrite div2_double. -Replace (mult (4) (S N1)) with (mult (2) (mult (2) (S N1))). -Apply mult_le. -Replace (mult (2) (S N1)) with (S (S (mult (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 Rlt_monotony_contra with ``/4``. -Apply Rlt_Rinv; Sup0. -Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1l; Rewrite Rmult_sym. -Replace ``(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S (S (S O)))) (S (div2 (pred n)))))/(INR (fact (div2 (pred n))))`` with ``(Rabsolu ((pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S (S (S O)))) (S (div2 (pred n)))))/(INR (fact (div2 (pred n))))-0))``. -Apply H2; Unfold ge. -Cut (le (mult (2) (S N0)) n). -Intro; Apply le_S_n. -Apply INR_le; Apply Rle_monotony_contra with (INR (2)). -Simpl; 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 (lt O N1). -Intro. -Rewrite H7. -Apply mult_le. -Replace (pred (mult (2) N1)) with (S (mult (2) (pred N1))). -Rewrite div2_S_double. -Replace (S (pred N1)) with N1. -Apply le_n. -Apply S_pred with O; Apply H8. -Replace (mult (2) N1) with (S (S (mult (2) (pred N1)))). -Reflexivity. -Pattern 2 N1; 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; Apply S_pred with O; Apply H8. -Apply INR_lt. -Apply Rlt_monotony_contra with (INR (2)). -Simpl; Sup0. -Rewrite Rmult_Or; Rewrite <- mult_INR. -Apply lt_INR_0. -Rewrite <- H7. -Apply lt_le_trans with (2). -Apply lt_O_Sn. -Apply le_trans with (max (mult (2) (S N0)) (2)). -Apply le_max_r. -Apply H3. -Rewrite H7. -Replace (pred (S (mult (2) N1))) with (mult (2) N1). -Rewrite div2_double. -Replace (mult (2) (S N1)) with (S (S (mult (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 (mult (2) (S N0)) (2)). -Apply le_max_l. -Apply H3. -Rewrite minus_R0; Apply Rabsolu_right. -Apply Rle_sym1. -Unfold Rdiv; Repeat Apply Rmult_le_pos. -Apply pow_le. -Apply Rle_trans with R1. -Left; Apply Rlt_R0_R1. -Apply RmaxLess1. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -DiscrR. -Apply Rle_sym1. -Unfold Rdiv; Apply Rmult_le_pos. -Left; Sup0. -Apply Rmult_le_pos. -Apply pow_le. -Apply Rle_trans with R1. -Left; Apply Rlt_R0_R1. -Apply RmaxLess1. -Left; Apply Rlt_Rinv; Apply Rsqr_pos_lt; Apply INR_fact_neq_0. -Qed. - -(**********) -Lemma Reste_E_cv : (x,y:R) (Un_cv (Reste_E x y) R0). -Intros; Assert H := (maj_Reste_cv_R0 x y). -Unfold Un_cv in H; Unfold Un_cv; Intros; Elim (H ? H0); Intros. -Exists (max x0 (1)); Intros. -Unfold R_dist; Rewrite minus_R0. -Apply Rle_lt_trans with (maj_Reste_E x y n). -Apply Reste_E_maj. -Apply lt_le_trans with (1). -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) R0). -Apply H1. -Unfold ge; Apply le_trans with (max x0 (1)). -Apply le_max_l. -Apply H2. -Unfold R_dist; Rewrite minus_R0; Apply Rabsolu_right. -Apply Rle_sym1; Apply Rle_trans with (Rabsolu (Reste_E x y n)). -Apply Rabsolu_pos. -Apply Reste_E_maj. -Apply lt_le_trans with (1). -Apply lt_O_Sn. -Apply le_trans with (max x0 (1)). -Apply le_max_r. -Apply H2. -Qed. - -(**********) -Lemma exp_plus : (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; Unfold Un_cv in H3; Intros. -Elim (H3 ? H4); Intros. -Exists (S x0); Intros. -Rewrite <- (exp_form x y n). -Rewrite minus_R0 in H5. -Apply H5. -Unfold ge; 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 : (x:R) ``0<x`` -> ``0<(exp x)``. -Intros; Pose An := [N:nat]``/(INR (fact N))*(pow x N)``. -Cut (Un_cv [n:nat](sum_f_R0 An n) (exp x)). -Intro; Apply Rlt_le_trans with (sum_f_R0 An O). -Unfold An; Simpl; Rewrite Rinv_R1; Rewrite Rmult_1r; Apply Rlt_R0_R1. -Apply sum_incr. -Assumption. -Intro; Unfold An; Left; Apply Rmult_lt_pos. -Apply Rlt_Rinv; Apply INR_fact_lt_0. -Apply (pow_lt ? n H). -Unfold exp; Unfold projT1; Case (exist_exp x); Intro. -Unfold exp_in; Unfold infinit_sum Un_cv; Trivial. -Qed. - -(**********) -Lemma exp_pos : (x:R) ``0<(exp x)``. -Intro; Case (total_order_T R0 x); Intro. -Elim s; Intro. -Apply (exp_pos_pos ? a). -Rewrite <- b; Rewrite exp_0; Apply Rlt_R0_R1. -Replace (exp x) with ``1/(exp (-x))``. -Unfold Rdiv; Apply Rmult_lt_pos. -Apply Rlt_R0_R1. -Apply Rlt_Rinv; Apply exp_pos_pos. -Apply (Rgt_RO_Ropp ? r). -Cut ``(exp (-x))<>0``. -Intro; Unfold Rdiv; Apply r_Rmult_mult with ``(exp (-x))``. -Rewrite Rmult_1l; Rewrite <- Rinv_r_sym. -Rewrite <- exp_plus. -Rewrite Rplus_Ropp_l; Rewrite exp_0; Reflexivity. -Apply H. -Apply H. -Assert H := (exp_plus x ``-x``). -Rewrite Rplus_Ropp_r in H; Rewrite exp_0 in H. -Red; Intro; Rewrite H0 in H. -Rewrite Rmult_Or 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; Intros. -Pose fn := [N:nat][x:R]``(pow x N)/(INR (fact (S N)))``. -Cut (CVN_R fn). -Intro; Cut (x:R)(sigTT ? [l:R](Un_cv [N:nat](SP fn N x) l)). -Intro cv; Cut ((n:nat)(continuity (fn n))). -Intro; Cut (continuity (SFL fn cv)). -Intro; Unfold continuity in H1. -Assert H2 := (H1 R0). -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_Ol; Rewrite exp_0. -Replace ``((exp h)-1)/h`` with (SFL fn cv h). -Replace R1 with (SFL fn cv R0). -Apply H5. -Split. -Unfold D_x no_cond; Split. -Trivial. -Apply (not_sym ? ? H6). -Rewrite minus_R0; Apply H7. -Unfold SFL. -Case (cv ``0``); Intros. -EApply UL_sequence. -Apply u. -Unfold Un_cv SP. -Intros; Exists (1); Intros. -Unfold R_dist; Rewrite decomp_sum. -Rewrite (Rplus_sym (fn O R0)). -Replace (fn O R0) with R1. -Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Or. -Replace (sum_f_R0 [i:nat](fn (S i) ``0``) (pred n)) with R0. -Rewrite Rabsolu_R0; Apply H8. -Symmetry; Apply sum_eq_R0; Intros. -Unfold fn. -Simpl. -Unfold Rdiv; Do 2 Rewrite Rmult_Ol; Reflexivity. -Unfold fn; Simpl. -Unfold Rdiv; Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity. -Apply lt_le_trans with (1); [Apply lt_n_Sn | Apply H9]. -Unfold SFL exp. -Unfold projT1. -Case (cv h); Case (exist_exp h); Intros. -EApply UL_sequence. -Apply u. -Unfold Un_cv; Intros. -Unfold exp_in in e. -Unfold infinit_sum in e. -Cut ``0<eps0*(Rabsolu h)``. -Intro; Elim (e ? H9); Intros N0 H10. -Exists N0; Intros. -Unfold R_dist. -Apply Rlt_monotony_contra with ``(Rabsolu h)``. -Apply Rabsolu_pos_lt; Assumption. -Rewrite <- Rabsolu_mult. -Rewrite Rminus_distr. -Replace ``h*(x-1)/h`` with ``(x-1)``. -Unfold R_dist in H10. -Replace ``h*(SP fn n h)-(x-1)`` with (Rminus (sum_f_R0 [i:nat]``/(INR (fact i))*(pow h i)`` (S n)) x). -Rewrite (Rmult_sym (Rabsolu h)). -Apply H10. -Unfold ge. -Apply le_trans with (S N0). -Apply le_n_Sn. -Apply le_n_S; Apply H11. -Rewrite decomp_sum. -Replace ``/(INR (fact O))*(pow h O)`` with R1. -Unfold Rminus. -Rewrite Ropp_distr1. -Rewrite Ropp_Ropp. -Rewrite <- (Rplus_sym ``-x``). -Rewrite <- (Rplus_sym ``-x+1``). -Rewrite Rplus_assoc; Repeat Apply Rplus_plus_r. -Replace (pred (S n)) with n; [Idtac | Reflexivity]. -Unfold SP. -Rewrite scal_sum. -Apply sum_eq; Intros. -Unfold fn. -Replace (pow h (S i)) with ``h*(pow h i)``. -Unfold Rdiv; Ring. -Simpl; Ring. -Simpl; Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity. -Apply lt_O_Sn. -Unfold Rdiv. -Rewrite <- Rmult_assoc. -Symmetry; Apply Rinv_r_simpl_m. -Assumption. -Apply Rmult_lt_pos. -Apply H8. -Apply Rabsolu_pos_lt; Assumption. -Apply SFL_continuity; Assumption. -Intro; Unfold fn. -Replace [x:R]``(pow x n)/(INR (fact (S n)))`` with (div_fct (pow_fct n) (fct_cte (INR (fact (S n))))); [Idtac | Reflexivity]. -Apply continuity_div. -Apply derivable_continuous; Apply (derivable_pow n). -Apply derivable_continuous; Apply derivable_const. -Intro; Unfold fct_cte; Apply INR_fact_neq_0. -Apply (CVN_R_CVS ? X). -Assert H0 := Alembert_exp. -Unfold CVN_R. -Intro; Unfold CVN_r. -Apply Specif.existT with [N:nat]``(pow r N)/(INR (fact (S N)))``. -Cut (SigT ? [l:R](Un_cv [n:nat](sum_f_R0 [k:nat](Rabsolu ``(pow r k)/(INR (fact (S k)))``) n) l)). -Intro. -Elim X; Intros. -Exists x; Intros. -Split. -Apply p. -Unfold Boule; Intros. -Rewrite minus_R0 in H1. -Unfold fn. -Unfold Rdiv; Rewrite Rabsolu_mult. -Cut ``0<(INR (fact (S n)))``. -Intro. -Rewrite (Rabsolu_right ``/(INR (fact (S n)))``). -Do 2 Rewrite <- (Rmult_sym ``/(INR (fact (S n)))``). -Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply H2. -Rewrite <- Pow_Rabsolu. -Apply pow_maj_Rabs. -Rewrite Rabsolu_Rabsolu; Left; Apply H1. -Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply H2. -Apply INR_fact_lt_0. -Cut (r::R)<>``0``. -Intro; Apply Alembert_C2. -Intro; Apply Rabsolu_no_R0. -Unfold Rdiv; Apply prod_neq_R0. -Apply pow_nonzero; Assumption. -Apply Rinv_neq_R0; Apply INR_fact_neq_0. -Unfold Un_cv in H0. -Unfold Un_cv; Intros. -Cut ``0<eps0/r``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply (cond_pos r)]]. -Elim (H0 ? H3); Intros N0 H4. -Exists N0; Intros. -Cut (ge (S n) N0). -Intro hyp_sn. -Assert H6 := (H4 ? hyp_sn). -Unfold R_dist in H6; Rewrite minus_R0 in H6. -Rewrite Rabsolu_Rabsolu in H6. -Unfold R_dist; Rewrite minus_R0. -Rewrite Rabsolu_Rabsolu. -Replace ``(Rabsolu ((pow r (S n))/(INR (fact (S (S n))))))/ - (Rabsolu ((pow r n)/(INR (fact (S n)))))`` with ``r*/(INR (fact (S (S n))))*//(INR (fact (S n)))``. -Rewrite Rmult_assoc; Rewrite Rabsolu_mult. -Rewrite (Rabsolu_right r). -Apply Rlt_monotony_contra with ``/r``. -Apply Rlt_Rinv; Apply (cond_pos r). -Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1l; Rewrite <- (Rmult_sym eps0). -Apply H6. -Assumption. -Apply Rle_sym1; Left; Apply (cond_pos r). -Unfold Rdiv. -Repeat Rewrite Rabsolu_mult. -Repeat Rewrite Rabsolu_Rinv. -Rewrite Rinv_Rmult. -Repeat Rewrite Rabsolu_right. -Rewrite Rinv_Rinv. -Rewrite (Rmult_sym r). -Rewrite (Rmult_sym (pow r (S n))). -Repeat Rewrite Rmult_assoc. -Apply Rmult_mult_r. -Rewrite (Rmult_sym r). -Rewrite <- Rmult_assoc; Rewrite <- (Rmult_sym (INR (fact (S n)))). -Apply Rmult_mult_r. -Simpl. -Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Ring. -Apply pow_nonzero; Assumption. -Apply INR_fact_neq_0. -Apply Rle_sym1; Left; Apply INR_fact_lt_0. -Apply Rle_sym1; Left; Apply pow_lt; Apply (cond_pos r). -Apply Rle_sym1; Left; Apply INR_fact_lt_0. -Apply Rle_sym1; Left; Apply pow_lt; Apply (cond_pos r). -Apply Rabsolu_no_R0; Apply pow_nonzero; Assumption. -Apply Rinv_neq_R0; Apply Rabsolu_no_R0; Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Unfold ge; Apply le_trans with n. -Apply H5. -Apply le_n_Sn. -Assert H1 := (cond_pos r); Red; Intro; Rewrite H2 in H1; Elim (Rlt_antirefl ? H1). -Qed. - -(**********) -Lemma derivable_pt_lim_exp : (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; Intros. -Cut ``0<eps/(exp x)``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Apply H | Apply Rlt_Rinv; Apply exp_pos]]. -Elim (H0 ? H1); Intros del H2. -Exists del; Intros. -Assert H5 := (H2 ? H3 H4). -Rewrite Rplus_Ol 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 Rabsolu_mult; Rewrite (Rabsolu_right (exp x)). -Apply Rlt_monotony_contra with ``/(exp x)``. -Apply Rlt_Rinv; Apply exp_pos. -Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1l; Rewrite <- (Rmult_sym eps). -Apply H5. -Assert H6 := (exp_pos x); Red; Intro; Rewrite H7 in H6; Elim (Rlt_antirefl ? H6). -Apply Rle_sym1; Left; Apply exp_pos. -Rewrite Rminus_distr. -Rewrite Rmult_1r; Unfold Rdiv; Rewrite <- Rmult_assoc; Rewrite Rminus_distr. -Rewrite Rmult_1r; Rewrite exp_plus; Reflexivity. -Qed. |