diff options
Diffstat (limited to 'theories/Reals/Exp_prop.v')
| -rw-r--r-- | theories/Reals/Exp_prop.v | 230 |
1 files changed, 108 insertions, 122 deletions
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index dd97b865..b65ab045 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,23 +9,23 @@ Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. -Require Import Rtrigo. +Require Import Rtrigo1. Require Import Ranalysis1. Require Import PSeries_reg. Require Import Div2. Require Import Even. Require Import Max. -Open Local Scope nat_scope. -Open Local Scope R_scope. +Local Open Scope nat_scope. +Local Open Scope R_scope. Definition E1 (x:R) (N:nat) : R := sum_f_R0 (fun k:nat => / INR (fact k) * x ^ k) N. Lemma E1_cvg : forall x:R, Un_cv (E1 x) (exp x). Proof. - intro; unfold exp in |- *; unfold projT1 in |- *. + intro; unfold exp; unfold projT1. case (exist_exp x); intro. - unfold exp_in, Un_cv in |- *; unfold infinite_sum, E1 in |- *; trivial. + unfold exp_in, Un_cv; unfold infinite_sum, E1; trivial. Qed. Definition Reste_E (x y:R) (N:nat) : R := @@ -41,14 +41,14 @@ 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. Proof. - intros; unfold E1 in |- *. + intros; unfold E1. rewrite cauchy_finite. - unfold Reste_E in |- *; unfold Rminus in |- *; rewrite Rplus_assoc; + unfold Reste_E; unfold Rminus; 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; + unfold C; unfold Rdiv; 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. @@ -64,27 +64,13 @@ Definition maj_Reste_E (x y:R) (N:nat) : R := (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (2 * N) / Rsqr (INR (fact (div2 (pred N))))). -Lemma Rle_Rinv : forall x y:R, 0 < x -> 0 < y -> x <= y -> / y <= / x. -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. 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. + simpl; simpl in HrecN; rewrite HrecN; reflexivity. ring. Qed. @@ -93,7 +79,7 @@ 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. + simpl; simpl in HrecN; rewrite HrecN; reflexivity. ring. Qed. @@ -107,7 +93,7 @@ Proof. 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. + rewrite H1; simpl; apply lt_O_Sn. inversion H. right; reflexivity. left; apply lt_le_trans with 2%nat; [ apply lt_n_Sn | apply H1 ]. @@ -124,7 +110,7 @@ Proof. (fun k:nat => sum_f_R0 (fun l:nat => / Rsqr (INR (fact (div2 (S N))))) (pred (N - k))) (pred N)). - unfold Reste_E in |- *. + unfold Reste_E. apply Rle_trans with (sum_f_R0 (fun k:nat => @@ -203,25 +189,25 @@ Proof. apply Rabs_pos. apply Rle_trans with (Rmax (Rabs x) (Rabs y)). apply RmaxLess1. - unfold M in |- *; apply RmaxLess2. + unfold M; 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. + unfold M; 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. + unfold M; 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. + unfold M; 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. + symmetry ; 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. @@ -260,7 +246,7 @@ Proof. apply pow_le. apply Rle_trans with 1. left; apply Rlt_0_1. - unfold M in |- *; apply RmaxLess1. + unfold M; apply RmaxLess1. assert (H2 := even_odd_cor N). elim H2; intros N0 H3. elim H3; intro. @@ -276,9 +262,9 @@ Proof. 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. + pattern N at 1; rewrite H4. apply Rle_trans with (C N N0 / INR (fact N)). - unfold Rdiv in |- *; do 2 rewrite <- (Rmult_comm (/ INR (fact N))). + unfold Rdiv; 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. @@ -308,7 +294,7 @@ Proof. 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 |- *. + unfold Rsqr, C, Rdiv. repeat rewrite Rinv_mult_distr. rewrite (Rmult_comm (INR (fact N))). repeat rewrite Rmult_assoc. @@ -316,7 +302,7 @@ Proof. rewrite Rmult_1_r; replace (N - N0)%nat with N0. ring. replace N with (N0 + N0)%nat. - symmetry in |- *; apply minus_plus. + symmetry ; apply minus_plus. rewrite H4. ring. apply INR_fact_neq_0. @@ -324,7 +310,7 @@ Proof. apply INR_fact_neq_0. apply INR_fact_neq_0. apply INR_fact_neq_0. - unfold C, Rdiv in |- *. + unfold C, Rdiv. rewrite (Rmult_comm (INR (fact N))). repeat rewrite Rmult_assoc. rewrite <- Rinv_r_sym. @@ -336,7 +322,7 @@ Proof. 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)))). + unfold Rdiv; 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). @@ -371,7 +357,7 @@ Proof. 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 |- *. + unfold Rsqr, C, Rdiv. repeat rewrite Rinv_mult_distr. replace (S N - S N0)%nat with (S N0). rewrite (Rmult_comm (INR (fact (S N)))). @@ -380,14 +366,14 @@ Proof. rewrite Rmult_1_r; reflexivity. apply INR_fact_neq_0. replace (S N) with (S N0 + S N0)%nat. - symmetry in |- *; apply minus_plus. + 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. rewrite H4; ring. - unfold C, Rdiv in |- *. + unfold C, Rdiv. rewrite (Rmult_comm (INR (fact (S N)))). rewrite Rmult_assoc; rewrite <- Rinv_r_sym. rewrite Rmult_1_r; rewrite Rinv_mult_distr. @@ -395,8 +381,8 @@ Proof. 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). + unfold maj_Reste_E. + unfold Rdiv; rewrite (Rmult_comm 4). rewrite Rmult_assoc. apply Rmult_le_compat_l. apply pow_le. @@ -447,7 +433,7 @@ Proof. 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. + apply not_O_INR; red; intro. cut (1 < S N)%nat. intro; assert (H4 := div2_not_R0 _ H3). rewrite H2 in H4; elim (lt_n_O _ H4). @@ -470,17 +456,17 @@ Proof. 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; + 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 N at 2 in |- *; rewrite H3. + pattern N at 2; rewrite H3. rewrite div2_S_double. right; rewrite H3; reflexivity. - pattern N at 2 in |- *; rewrite H3. + pattern N at 2; rewrite H3. replace (S (S (2 * N0))) with (2 * S N0)%nat. rewrite div2_double. rewrite H3. @@ -489,12 +475,12 @@ Proof. 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; + simpl. + pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply Rlt_0_1. 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. + 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. @@ -520,15 +506,15 @@ Qed. Lemma maj_Reste_cv_R0 : forall x y:R, Un_cv (maj_Reste_E x y) 0. Proof. intros; assert (H := Majxy_cv_R0 x y). - unfold Un_cv in H; unfold Un_cv in |- *; intros. + unfold Un_cv in H; unfold Un_cv; intros. cut (0 < eps / 4); [ intro - | unfold Rdiv in |- *; apply Rmult_lt_0_compat; + | unfold Rdiv; 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 |- *. + unfold R_dist in H2; unfold R_dist; rewrite Rminus_0_r; + unfold Majxy in H2; unfold maj_Reste_E. rewrite Rabs_right. apply Rle_lt_trans with (4 * @@ -536,7 +522,7 @@ Proof. INR (fact (div2 (pred n))))). apply Rmult_le_compat_l. left; prove_sup0. - unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr. + unfold Rdiv, Rsqr; 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))))) @@ -544,7 +530,7 @@ Proof. 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 |- *; + pattern (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (2 * n)) at 2; rewrite <- Rmult_1_r; apply Rmult_le_compat_l. apply pow_le; apply Rle_trans with 1. left; apply Rlt_0_1. @@ -598,11 +584,11 @@ Proof. (Rabs (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S (div2 (pred n))) / INR (fact (div2 (pred n))) - 0)). - apply H2; unfold ge in |- *. + apply H2; unfold ge. 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. + simpl; prove_sup0. do 2 rewrite <- mult_INR; apply le_INR. apply le_trans with n. apply H4. @@ -620,12 +606,12 @@ Proof. 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)). + pattern N1 at 2; replace N1 with (S (pred N1)). ring. - symmetry in |- *; apply S_pred with 0%nat; apply H8. + symmetry ; apply S_pred with 0%nat; apply H8. apply INR_lt. apply Rmult_lt_reg_l with (INR 2). - simpl in |- *; prove_sup0. + simpl; prove_sup0. rewrite Rmult_0_r; rewrite <- mult_INR. apply lt_INR_0. rewrite <- H7. @@ -646,7 +632,7 @@ Proof. apply H3. rewrite Rminus_0_r; apply Rabs_right. apply Rle_ge. - unfold Rdiv in |- *; apply Rmult_le_pos. + unfold Rdiv; apply Rmult_le_pos. apply pow_le. apply Rle_trans with 1. left; apply Rlt_0_1. @@ -654,7 +640,7 @@ Proof. left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. discrR. apply Rle_ge. - unfold Rdiv in |- *; apply Rmult_le_pos. + unfold Rdiv; apply Rmult_le_pos. left; prove_sup0. apply Rmult_le_pos. apply pow_le. @@ -668,9 +654,9 @@ Qed. Lemma Reste_E_cv : forall x y:R, Un_cv (Reste_E x y) 0. Proof. intros; assert (H := maj_Reste_cv_R0 x y). - unfold Un_cv in H; unfold Un_cv in |- *; intros; elim (H _ H0); intros. + unfold Un_cv in H; unfold Un_cv; intros; elim (H _ H0); intros. exists (max x0 1); intros. - unfold R_dist in |- *; rewrite Rminus_0_r. + unfold R_dist; 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. @@ -680,10 +666,10 @@ Proof. 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). + unfold ge; apply le_trans with (max x0 1). apply le_max_l. apply H2. - unfold R_dist in |- *; rewrite Rminus_0_r; apply Rabs_right. + unfold R_dist; 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. @@ -704,13 +690,13 @@ Proof. 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. + unfold Un_cv; 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). + unfold ge; apply le_trans with (S x0). apply le_n_Sn. apply H6. apply lt_le_trans with (S x0). @@ -724,15 +710,15 @@ 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; + unfold An; simpl; 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. + intro; unfold An; 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 infinite_sum, Un_cv in |- *; trivial. + unfold exp; unfold projT1; case (exist_exp x); intro. + unfold exp_in; unfold infinite_sum, Un_cv; trivial. Qed. (**********) @@ -743,12 +729,12 @@ Proof. 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. + unfold Rdiv; 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)). + intro; unfold Rdiv; 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. @@ -756,7 +742,7 @@ Proof. 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. + red; intro; rewrite H0 in H. rewrite Rmult_0_r in H. elim R1_neq_R0; assumption. Qed. @@ -764,7 +750,7 @@ Qed. (* ((exp h)-1)/h -> 0 quand h->0 *) Lemma derivable_pt_lim_exp_0 : derivable_pt_lim exp 0 1. Proof. - unfold derivable_pt_lim in |- *; intros. + unfold derivable_pt_lim; intros. set (fn := fun (N:nat) (x:R) => x ^ N / INR (fact (S N))). cut (CVN_R fn). intro; cut (forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }). @@ -782,41 +768,41 @@ Proof. replace 1 with (SFL fn cv 0). apply H5. split. - unfold D_x, no_cond in |- *; split. + unfold D_x, no_cond; split. trivial. - apply (sym_not_eq H6). + apply (not_eq_sym H6). rewrite Rminus_0_r; apply H7. - unfold SFL in |- *. + unfold SFL. case (cv 0); intros. eapply UL_sequence. apply u. - unfold Un_cv, SP in |- *. + unfold Un_cv, SP. intros; exists 1%nat; intros. - unfold R_dist in |- *; rewrite decomp_sum. + unfold R_dist; 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; + unfold Rminus; 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. + symmetry ; apply sum_eq_R0; intros. + unfold fn. + simpl. + unfold Rdiv; do 2 rewrite Rmult_0_l; reflexivity. + unfold fn; simpl. + unfold Rdiv; 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 SFL, exp. case (cv h); case (exist_exp h); simpl; intros. eapply UL_sequence. apply u. - unfold Un_cv in |- *; intros. + unfold Un_cv; intros. unfold exp_in in e. unfold infinite_sum in e. cut (0 < eps0 * Rabs h). intro; elim (e _ H9); intros N0 H10. exists N0; intros. - unfold R_dist in |- *. + unfold R_dist. apply Rmult_lt_reg_l with (Rabs h). apply Rabs_pos_lt; assumption. rewrite <- Rabs_mult. @@ -827,47 +813,47 @@ Proof. (sum_f_R0 (fun i:nat => / INR (fact i) * h ^ i) (S n) - x). rewrite (Rmult_comm (Rabs h)). apply H10. - unfold ge in |- *. + unfold ge. 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 |- *. + unfold Rminus. 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 |- *. + unfold SP. rewrite scal_sum. apply sum_eq; intros. - unfold fn in |- *. + unfold fn. 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. + unfold Rdiv; ring. + simpl; ring. + simpl; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. apply lt_O_Sn. - unfold Rdiv in |- *. + unfold Rdiv. rewrite <- Rmult_assoc. - symmetry in |- *; apply Rinv_r_simpl_m. + symmetry ; 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 |- *. + intro; unfold fn. 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. + intro; unfold fct_cte; apply INR_fact_neq_0. apply (CVN_R_CVS _ X). assert (H0 := Alembert_exp). - unfold CVN_R in |- *. - intro; unfold CVN_r in |- *. + unfold CVN_R. + intro; unfold CVN_r. exists (fun N:nat => r ^ N / INR (fact (S N))). cut { l:R | @@ -879,10 +865,10 @@ Proof. exists x; intros. split. apply p. - unfold Boule in |- *; intros. + unfold Boule; intros. rewrite Rminus_0_r in H1. - unfold fn in |- *. - unfold Rdiv in |- *; rewrite Rabs_mult. + unfold fn. + unfold Rdiv; rewrite Rabs_mult. cut (0 < INR (fact (S n))). intro. rewrite (Rabs_right (/ INR (fact (S n)))). @@ -897,14 +883,14 @@ Proof. cut ((r:R) <> 0). intro; apply Alembert_C2. intro; apply Rabs_no_R0. - unfold Rdiv in |- *; apply prod_neq_R0. + unfold Rdiv; 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. + unfold Un_cv; intros. cut (0 < eps0 / r); [ intro - | unfold Rdiv in |- *; apply Rmult_lt_0_compat; + | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; apply (cond_pos r) ] ]. elim (H0 _ H3); intros N0 H4. exists N0; intros. @@ -913,7 +899,7 @@ Proof. 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. + unfold R_dist; rewrite Rminus_0_r. rewrite Rabs_Rabsolu. replace (Rabs (r ^ S n / INR (fact (S (S n)))) / Rabs (r ^ n / INR (fact (S n)))) @@ -927,7 +913,7 @@ Proof. apply H6. assumption. apply Rle_ge; left; apply (cond_pos r). - unfold Rdiv in |- *. + unfold Rdiv. repeat rewrite Rabs_mult. repeat rewrite Rabs_Rinv. rewrite Rinv_mult_distr. @@ -940,7 +926,7 @@ Proof. rewrite (Rmult_comm r). rewrite <- Rmult_assoc; rewrite <- (Rmult_comm (INR (fact (S n)))). apply Rmult_eq_compat_l. - simpl in |- *. + simpl. rewrite Rmult_assoc; rewrite <- Rinv_r_sym. ring. apply pow_nonzero; assumption. @@ -953,10 +939,10 @@ Proof. 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. + unfold ge; apply le_trans with n. apply H5. apply le_n_Sn. - assert (H1 := cond_pos r); red in |- *; intro; rewrite H2 in H1; + assert (H1 := cond_pos r); red; intro; rewrite H2 in H1; elim (Rlt_irrefl _ H1). Qed. @@ -964,10 +950,10 @@ Qed. Lemma derivable_pt_lim_exp : forall x:R, derivable_pt_lim exp x (exp x). Proof. intro; assert (H0 := derivable_pt_lim_exp_0). - unfold derivable_pt_lim in H0; unfold derivable_pt_lim in |- *; intros. + unfold derivable_pt_lim in H0; unfold derivable_pt_lim; intros. cut (0 < eps / exp x); [ intro - | unfold Rdiv in |- *; apply Rmult_lt_0_compat; + | unfold Rdiv; apply Rmult_lt_0_compat; [ apply H | apply Rinv_0_lt_compat; apply exp_pos ] ]. elim (H0 _ H1); intros del H2. exists del; intros. @@ -981,11 +967,11 @@ Proof. 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; + assert (H6 := exp_pos x); red; 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_1_r; unfold Rdiv; rewrite <- Rmult_assoc; rewrite Rmult_minus_distr_l. rewrite Rmult_1_r; rewrite exp_plus; reflexivity. Qed. |