diff options
Diffstat (limited to 'theories/Reals/Ranalysis2.v')
| -rw-r--r-- | theories/Reals/Ranalysis2.v | 775 |
1 files changed, 394 insertions, 381 deletions
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 0627e22c..fb89da67 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ranalysis2.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Ranalysis2.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -14,437 +14,450 @@ Require Import Ranalysis1. Open Local Scope R_scope. (**********) Lemma formule : - forall (x h l1 l2:R) (f1 f2:R -> R), - h <> 0 -> - f2 x <> 0 -> - f2 (x + h) <> 0 -> - (f1 (x + h) / f2 (x + h) - f1 x / f2 x) / h - - (l1 * f2 x - l2 * f1 x) / Rsqr (f2 x) = - / f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1) + - l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h)) - - f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2) + - l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x). -intros; unfold Rdiv, Rminus, Rsqr in |- *. -repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l; - repeat rewrite Rinv_mult_distr; try assumption. -replace (l1 * f2 x * (/ f2 x * / f2 x)) with (l1 * / f2 x * (f2 x * / f2 x)); - [ idtac | ring ]. -replace (l1 * (/ f2 x * / f2 (x + h)) * f2 x) with - (l1 * / f2 (x + h) * (f2 x * / f2 x)); [ idtac | ring ]. -replace (l1 * (/ f2 x * / f2 (x + h)) * - f2 (x + h)) with - (- (l1 * / f2 x * (f2 (x + h) * / f2 (x + h)))); [ idtac | ring ]. -replace (f1 x * (/ f2 x * / f2 (x + h)) * (f2 (x + h) * / h)) with - (f1 x * / f2 x * / h * (f2 (x + h) * / f2 (x + h))); - [ idtac | ring ]. -replace (f1 x * (/ f2 x * / f2 (x + h)) * (- f2 x * / h)) with - (- (f1 x * / f2 (x + h) * / h * (f2 x * / f2 x))); - [ idtac | ring ]. -replace (l2 * f1 x * (/ f2 x * / f2 x * / f2 (x + h)) * f2 (x + h)) with - (l2 * f1 x * / f2 x * / f2 x * (f2 (x + h) * / f2 (x + h))); - [ idtac | ring ]. -replace (l2 * f1 x * (/ f2 x * / f2 x * / f2 (x + h)) * - f2 x) with - (- (l2 * f1 x * / f2 x * / f2 (x + h) * (f2 x * / f2 x))); - [ idtac | ring ]. -repeat rewrite <- Rinv_r_sym; try assumption || ring. -apply prod_neq_R0; assumption. + forall (x h l1 l2:R) (f1 f2:R -> R), + h <> 0 -> + f2 x <> 0 -> + f2 (x + h) <> 0 -> + (f1 (x + h) / f2 (x + h) - f1 x / f2 x) / h - + (l1 * f2 x - l2 * f1 x) / Rsqr (f2 x) = + / f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1) + + l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h)) - + f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2) + + l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x). +Proof. + intros; unfold Rdiv, Rminus, Rsqr in |- *. + repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l; + repeat rewrite Rinv_mult_distr; try assumption. + replace (l1 * f2 x * (/ f2 x * / f2 x)) with (l1 * / f2 x * (f2 x * / f2 x)); + [ idtac | ring ]. + replace (l1 * (/ f2 x * / f2 (x + h)) * f2 x) with + (l1 * / f2 (x + h) * (f2 x * / f2 x)); [ idtac | ring ]. + replace (l1 * (/ f2 x * / f2 (x + h)) * - f2 (x + h)) with + (- (l1 * / f2 x * (f2 (x + h) * / f2 (x + h)))); [ idtac | ring ]. + replace (f1 x * (/ f2 x * / f2 (x + h)) * (f2 (x + h) * / h)) with + (f1 x * / f2 x * / h * (f2 (x + h) * / f2 (x + h))); + [ idtac | ring ]. + replace (f1 x * (/ f2 x * / f2 (x + h)) * (- f2 x * / h)) with + (- (f1 x * / f2 (x + h) * / h * (f2 x * / f2 x))); + [ idtac | ring ]. + replace (l2 * f1 x * (/ f2 x * / f2 x * / f2 (x + h)) * f2 (x + h)) with + (l2 * f1 x * / f2 x * / f2 x * (f2 (x + h) * / f2 (x + h))); + [ idtac | ring ]. + replace (l2 * f1 x * (/ f2 x * / f2 x * / f2 (x + h)) * - f2 x) with + (- (l2 * f1 x * / f2 x * / f2 (x + h) * (f2 x * / f2 x))); + [ idtac | ring ]. + repeat rewrite <- Rinv_r_sym; try assumption || ring. + apply prod_neq_R0; assumption. Qed. Lemma Rmin_pos : forall x y:R, 0 < x -> 0 < y -> 0 < Rmin x y. -intros; unfold Rmin in |- *. -case (Rle_dec x y); intro; assumption. +Proof. + intros; unfold Rmin in |- *. + case (Rle_dec x y); intro; assumption. Qed. Lemma maj_term1 : - forall (x h eps l1 alp_f2:R) (eps_f2 alp_f1d:posreal) - (f1 f2:R -> R), - 0 < eps -> - f2 x <> 0 -> - f2 (x + h) <> 0 -> - (forall h:R, + forall (x h eps l1 alp_f2:R) (eps_f2 alp_f1d:posreal) + (f1 f2:R -> R), + 0 < eps -> + f2 x <> 0 -> + f2 (x + h) <> 0 -> + (forall h:R, h <> 0 -> Rabs h < alp_f1d -> Rabs ((f1 (x + h) - f1 x) / h - l1) < Rabs (eps * f2 x / 8)) -> - (forall a:R, + (forall a:R, Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) -> - h <> 0 -> - Rabs h < alp_f1d -> - Rabs h < Rmin eps_f2 alp_f2 -> - Rabs (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) < eps / 4. -intros. -assert (H7 := H3 h H6). -assert (H8 := H2 h H4 H5). -apply Rle_lt_trans with - (2 / Rabs (f2 x) * Rabs ((f1 (x + h) - f1 x) / h - l1)). -rewrite Rabs_mult. -apply Rmult_le_compat_r. -apply Rabs_pos. -rewrite Rabs_Rinv; [ left; exact H7 | assumption ]. -apply Rlt_le_trans with (2 / Rabs (f2 x) * Rabs (eps * f2 x / 8)). -apply Rmult_lt_compat_l. -unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ prove_sup0 | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ]. -exact H8. -right; unfold Rdiv in |- *. -repeat rewrite Rabs_mult. -rewrite Rabs_Rinv; discrR. -replace (Rabs 8) with 8. -replace 8 with 8; [ idtac | ring ]. -rewrite Rinv_mult_distr; [ idtac | discrR | discrR ]. -replace (2 * / Rabs (f2 x) * (Rabs eps * Rabs (f2 x) * (/ 2 * / 4))) with - (Rabs eps * / 4 * (2 * / 2) * (Rabs (f2 x) * / Rabs (f2 x))); - [ idtac | ring ]. -replace (Rabs eps) with eps. -repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption). -ring. -symmetry in |- *; apply Rabs_right; left; assumption. -symmetry in |- *; apply Rabs_right; left; prove_sup. + h <> 0 -> + Rabs h < alp_f1d -> + Rabs h < Rmin eps_f2 alp_f2 -> + Rabs (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) < eps / 4. +Proof. + intros. + assert (H7 := H3 h H6). + assert (H8 := H2 h H4 H5). + apply Rle_lt_trans with + (2 / Rabs (f2 x) * Rabs ((f1 (x + h) - f1 x) / h - l1)). + rewrite Rabs_mult. + apply Rmult_le_compat_r. + apply Rabs_pos. + rewrite Rabs_Rinv; [ left; exact H7 | assumption ]. + apply Rlt_le_trans with (2 / Rabs (f2 x) * Rabs (eps * f2 x / 8)). + apply Rmult_lt_compat_l. + unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ prove_sup0 | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ]. + exact H8. + right; unfold Rdiv in |- *. + repeat rewrite Rabs_mult. + rewrite Rabs_Rinv; discrR. + replace (Rabs 8) with 8. + replace 8 with 8; [ idtac | ring ]. + rewrite Rinv_mult_distr; [ idtac | discrR | discrR ]. + replace (2 * / Rabs (f2 x) * (Rabs eps * Rabs (f2 x) * (/ 2 * / 4))) with + (Rabs eps * / 4 * (2 * / 2) * (Rabs (f2 x) * / Rabs (f2 x))); + [ idtac | ring ]. + replace (Rabs eps) with eps. + repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption). + ring. + symmetry in |- *; apply Rabs_right; left; assumption. + symmetry in |- *; apply Rabs_right; left; prove_sup. Qed. Lemma maj_term2 : - forall (x h eps l1 alp_f2 alp_f2t2:R) (eps_f2:posreal) - (f2:R -> R), - 0 < eps -> - f2 x <> 0 -> - f2 (x + h) <> 0 -> - (forall a:R, + forall (x h eps l1 alp_f2 alp_f2t2:R) (eps_f2:posreal) + (f2:R -> R), + 0 < eps -> + f2 x <> 0 -> + f2 (x + h) <> 0 -> + (forall a:R, Rabs a < alp_f2t2 -> Rabs (f2 (x + a) - f2 x) < Rabs (eps * Rsqr (f2 x) / (8 * l1))) -> - (forall a:R, + (forall a:R, Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) -> - h <> 0 -> - Rabs h < alp_f2t2 -> - Rabs h < Rmin eps_f2 alp_f2 -> - l1 <> 0 -> Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) < eps / 4. -intros. -assert (H8 := H3 h H6). -assert (H9 := H2 h H5). -apply Rle_lt_trans with - (Rabs (l1 / (f2 x * f2 (x + h))) * Rabs (eps * Rsqr (f2 x) / (8 * l1))). -rewrite Rabs_mult; apply Rmult_le_compat_l. -apply Rabs_pos. -rewrite <- (Rabs_Ropp (f2 x - f2 (x + h))); rewrite Ropp_minus_distr. -left; apply H9. -apply Rlt_le_trans with - (Rabs (2 * (l1 / (f2 x * f2 x))) * Rabs (eps * Rsqr (f2 x) / (8 * l1))). -apply Rmult_lt_compat_r. -apply Rabs_pos_lt. -unfold Rdiv in |- *; unfold Rsqr in |- *; repeat apply prod_neq_R0; - try assumption || discrR. -red in |- *; intro H10; rewrite H10 in H; elim (Rlt_irrefl _ H). -apply Rinv_neq_0_compat; apply prod_neq_R0; try assumption || discrR. -unfold Rdiv in |- *. -repeat rewrite Rinv_mult_distr; try assumption. -repeat rewrite Rabs_mult. -replace (Rabs 2) with 2. -rewrite (Rmult_comm 2). -replace (Rabs l1 * (Rabs (/ f2 x) * Rabs (/ f2 x)) * 2) with - (Rabs l1 * (Rabs (/ f2 x) * (Rabs (/ f2 x) * 2))); - [ idtac | ring ]. -repeat apply Rmult_lt_compat_l. -apply Rabs_pos_lt; assumption. -apply Rabs_pos_lt; apply Rinv_neq_0_compat; assumption. -repeat rewrite Rabs_Rinv; try assumption. -rewrite <- (Rmult_comm 2). -unfold Rdiv in H8; exact H8. -symmetry in |- *; apply Rabs_right; left; prove_sup0. -right. -unfold Rsqr, Rdiv in |- *. -do 1 rewrite Rinv_mult_distr; try assumption || discrR. -do 1 rewrite Rinv_mult_distr; try assumption || discrR. -repeat rewrite Rabs_mult. -repeat rewrite Rabs_Rinv; try assumption || discrR. -replace (Rabs eps) with eps. -replace (Rabs 8) with 8. -replace (Rabs 2) with 2. -replace 8 with (4 * 2); [ idtac | ring ]. -rewrite Rinv_mult_distr; discrR. -replace - (2 * (Rabs l1 * (/ Rabs (f2 x) * / Rabs (f2 x))) * - (eps * (Rabs (f2 x) * Rabs (f2 x)) * (/ 4 * / 2 * / Rabs l1))) with - (eps * / 4 * (Rabs l1 * / Rabs l1) * (Rabs (f2 x) * / Rabs (f2 x)) * - (Rabs (f2 x) * / Rabs (f2 x)) * (2 * / 2)); [ idtac | ring ]. -repeat rewrite <- Rinv_r_sym; try (apply Rabs_no_R0; assumption) || discrR. -ring. -symmetry in |- *; apply Rabs_right; left; prove_sup0. -symmetry in |- *; apply Rabs_right; left; prove_sup. -symmetry in |- *; apply Rabs_right; left; assumption. + h <> 0 -> + Rabs h < alp_f2t2 -> + Rabs h < Rmin eps_f2 alp_f2 -> + l1 <> 0 -> Rabs (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) < eps / 4. +Proof. + intros. + assert (H8 := H3 h H6). + assert (H9 := H2 h H5). + apply Rle_lt_trans with + (Rabs (l1 / (f2 x * f2 (x + h))) * Rabs (eps * Rsqr (f2 x) / (8 * l1))). + rewrite Rabs_mult; apply Rmult_le_compat_l. + apply Rabs_pos. + rewrite <- (Rabs_Ropp (f2 x - f2 (x + h))); rewrite Ropp_minus_distr. + left; apply H9. + apply Rlt_le_trans with + (Rabs (2 * (l1 / (f2 x * f2 x))) * Rabs (eps * Rsqr (f2 x) / (8 * l1))). + apply Rmult_lt_compat_r. + apply Rabs_pos_lt. + unfold Rdiv in |- *; unfold Rsqr in |- *; repeat apply prod_neq_R0; + try assumption || discrR. + red in |- *; intro H10; rewrite H10 in H; elim (Rlt_irrefl _ H). + apply Rinv_neq_0_compat; apply prod_neq_R0; try assumption || discrR. + unfold Rdiv in |- *. + repeat rewrite Rinv_mult_distr; try assumption. + repeat rewrite Rabs_mult. + replace (Rabs 2) with 2. + rewrite (Rmult_comm 2). + replace (Rabs l1 * (Rabs (/ f2 x) * Rabs (/ f2 x)) * 2) with + (Rabs l1 * (Rabs (/ f2 x) * (Rabs (/ f2 x) * 2))); + [ idtac | ring ]. + repeat apply Rmult_lt_compat_l. + apply Rabs_pos_lt; assumption. + apply Rabs_pos_lt; apply Rinv_neq_0_compat; assumption. + repeat rewrite Rabs_Rinv; try assumption. + rewrite <- (Rmult_comm 2). + unfold Rdiv in H8; exact H8. + symmetry in |- *; apply Rabs_right; left; prove_sup0. + right. + unfold Rsqr, Rdiv in |- *. + do 1 rewrite Rinv_mult_distr; try assumption || discrR. + do 1 rewrite Rinv_mult_distr; try assumption || discrR. + repeat rewrite Rabs_mult. + repeat rewrite Rabs_Rinv; try assumption || discrR. + replace (Rabs eps) with eps. + replace (Rabs 8) with 8. + replace (Rabs 2) with 2. + replace 8 with (4 * 2); [ idtac | ring ]. + rewrite Rinv_mult_distr; discrR. + replace + (2 * (Rabs l1 * (/ Rabs (f2 x) * / Rabs (f2 x))) * + (eps * (Rabs (f2 x) * Rabs (f2 x)) * (/ 4 * / 2 * / Rabs l1))) with + (eps * / 4 * (Rabs l1 * / Rabs l1) * (Rabs (f2 x) * / Rabs (f2 x)) * + (Rabs (f2 x) * / Rabs (f2 x)) * (2 * / 2)); [ idtac | ring ]. + repeat rewrite <- Rinv_r_sym; try (apply Rabs_no_R0; assumption) || discrR. + ring. + symmetry in |- *; apply Rabs_right; left; prove_sup0. + symmetry in |- *; apply Rabs_right; left; prove_sup. + symmetry in |- *; apply Rabs_right; left; assumption. Qed. Lemma maj_term3 : - forall (x h eps l2 alp_f2:R) (eps_f2 alp_f2d:posreal) - (f1 f2:R -> R), - 0 < eps -> - f2 x <> 0 -> - f2 (x + h) <> 0 -> - (forall h:R, + forall (x h eps l2 alp_f2:R) (eps_f2 alp_f2d:posreal) + (f1 f2:R -> R), + 0 < eps -> + f2 x <> 0 -> + f2 (x + h) <> 0 -> + (forall h:R, h <> 0 -> Rabs h < alp_f2d -> Rabs ((f2 (x + h) - f2 x) / h - l2) < Rabs (Rsqr (f2 x) * eps / (8 * f1 x))) -> - (forall a:R, + (forall a:R, Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) -> - h <> 0 -> - Rabs h < alp_f2d -> - Rabs h < Rmin eps_f2 alp_f2 -> - f1 x <> 0 -> - Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) < - eps / 4. -intros. -assert (H8 := H2 h H4 H5). -assert (H9 := H3 h H6). -apply Rle_lt_trans with - (Rabs (f1 x / (f2 x * f2 (x + h))) * Rabs (Rsqr (f2 x) * eps / (8 * f1 x))). -rewrite Rabs_mult. -apply Rmult_le_compat_l. -apply Rabs_pos. -left; apply H8. -apply Rlt_le_trans with - (Rabs (2 * (f1 x / (f2 x * f2 x))) * Rabs (Rsqr (f2 x) * eps / (8 * f1 x))). -apply Rmult_lt_compat_r. -apply Rabs_pos_lt. -unfold Rdiv in |- *; unfold Rsqr in |- *; repeat apply prod_neq_R0; - try assumption. -red in |- *; intro H10; rewrite H10 in H; elim (Rlt_irrefl _ H). -apply Rinv_neq_0_compat; apply prod_neq_R0; discrR || assumption. -unfold Rdiv in |- *. -repeat rewrite Rinv_mult_distr; try assumption. -repeat rewrite Rabs_mult. -replace (Rabs 2) with 2. -rewrite (Rmult_comm 2). -replace (Rabs (f1 x) * (Rabs (/ f2 x) * Rabs (/ f2 x)) * 2) with - (Rabs (f1 x) * (Rabs (/ f2 x) * (Rabs (/ f2 x) * 2))); - [ idtac | ring ]. -repeat apply Rmult_lt_compat_l. -apply Rabs_pos_lt; assumption. -apply Rabs_pos_lt; apply Rinv_neq_0_compat; assumption. -repeat rewrite Rabs_Rinv; assumption || idtac. -rewrite <- (Rmult_comm 2). -unfold Rdiv in H9; exact H9. -symmetry in |- *; apply Rabs_right; left; prove_sup0. -right. -unfold Rsqr, Rdiv in |- *. -rewrite Rinv_mult_distr; try assumption || discrR. -rewrite Rinv_mult_distr; try assumption || discrR. -repeat rewrite Rabs_mult. -repeat rewrite Rabs_Rinv; try assumption || discrR. -replace (Rabs eps) with eps. -replace (Rabs 8) with 8. -replace (Rabs 2) with 2. -replace 8 with (4 * 2); [ idtac | ring ]. -rewrite Rinv_mult_distr; discrR. -replace - (2 * (Rabs (f1 x) * (/ Rabs (f2 x) * / Rabs (f2 x))) * - (Rabs (f2 x) * Rabs (f2 x) * eps * (/ 4 * / 2 * / Rabs (f1 x)))) with - (eps * / 4 * (Rabs (f2 x) * / Rabs (f2 x)) * (Rabs (f2 x) * / Rabs (f2 x)) * - (Rabs (f1 x) * / Rabs (f1 x)) * (2 * / 2)); [ idtac | ring ]. -repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption). -ring. -symmetry in |- *; apply Rabs_right; left; prove_sup0. -symmetry in |- *; apply Rabs_right; left; prove_sup. -symmetry in |- *; apply Rabs_right; left; assumption. + h <> 0 -> + Rabs h < alp_f2d -> + Rabs h < Rmin eps_f2 alp_f2 -> + f1 x <> 0 -> + Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) < + eps / 4. +Proof. + intros. + assert (H8 := H2 h H4 H5). + assert (H9 := H3 h H6). + apply Rle_lt_trans with + (Rabs (f1 x / (f2 x * f2 (x + h))) * Rabs (Rsqr (f2 x) * eps / (8 * f1 x))). + rewrite Rabs_mult. + apply Rmult_le_compat_l. + apply Rabs_pos. + left; apply H8. + apply Rlt_le_trans with + (Rabs (2 * (f1 x / (f2 x * f2 x))) * Rabs (Rsqr (f2 x) * eps / (8 * f1 x))). + apply Rmult_lt_compat_r. + apply Rabs_pos_lt. + unfold Rdiv in |- *; unfold Rsqr in |- *; repeat apply prod_neq_R0; + try assumption. + red in |- *; intro H10; rewrite H10 in H; elim (Rlt_irrefl _ H). + apply Rinv_neq_0_compat; apply prod_neq_R0; discrR || assumption. + unfold Rdiv in |- *. + repeat rewrite Rinv_mult_distr; try assumption. + repeat rewrite Rabs_mult. + replace (Rabs 2) with 2. + rewrite (Rmult_comm 2). + replace (Rabs (f1 x) * (Rabs (/ f2 x) * Rabs (/ f2 x)) * 2) with + (Rabs (f1 x) * (Rabs (/ f2 x) * (Rabs (/ f2 x) * 2))); + [ idtac | ring ]. + repeat apply Rmult_lt_compat_l. + apply Rabs_pos_lt; assumption. + apply Rabs_pos_lt; apply Rinv_neq_0_compat; assumption. + repeat rewrite Rabs_Rinv; assumption || idtac. + rewrite <- (Rmult_comm 2). + unfold Rdiv in H9; exact H9. + symmetry in |- *; apply Rabs_right; left; prove_sup0. + right. + unfold Rsqr, Rdiv in |- *. + rewrite Rinv_mult_distr; try assumption || discrR. + rewrite Rinv_mult_distr; try assumption || discrR. + repeat rewrite Rabs_mult. + repeat rewrite Rabs_Rinv; try assumption || discrR. + replace (Rabs eps) with eps. + replace (Rabs 8) with 8. + replace (Rabs 2) with 2. + replace 8 with (4 * 2); [ idtac | ring ]. + rewrite Rinv_mult_distr; discrR. + replace + (2 * (Rabs (f1 x) * (/ Rabs (f2 x) * / Rabs (f2 x))) * + (Rabs (f2 x) * Rabs (f2 x) * eps * (/ 4 * / 2 * / Rabs (f1 x)))) with + (eps * / 4 * (Rabs (f2 x) * / Rabs (f2 x)) * (Rabs (f2 x) * / Rabs (f2 x)) * + (Rabs (f1 x) * / Rabs (f1 x)) * (2 * / 2)); [ idtac | ring ]. + repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption). + ring. + symmetry in |- *; apply Rabs_right; left; prove_sup0. + symmetry in |- *; apply Rabs_right; left; prove_sup. + symmetry in |- *; apply Rabs_right; left; assumption. Qed. Lemma maj_term4 : - forall (x h eps l2 alp_f2 alp_f2c:R) (eps_f2:posreal) - (f1 f2:R -> R), - 0 < eps -> - f2 x <> 0 -> - f2 (x + h) <> 0 -> - (forall a:R, + forall (x h eps l2 alp_f2 alp_f2c:R) (eps_f2:posreal) + (f1 f2:R -> R), + 0 < eps -> + f2 x <> 0 -> + f2 (x + h) <> 0 -> + (forall a:R, Rabs a < alp_f2c -> Rabs (f2 (x + a) - f2 x) < Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))) -> - (forall a:R, + (forall a:R, Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) -> - h <> 0 -> - Rabs h < alp_f2c -> - Rabs h < Rmin eps_f2 alp_f2 -> - f1 x <> 0 -> - l2 <> 0 -> - Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x)) < - eps / 4. -intros. -assert (H9 := H2 h H5). -assert (H10 := H3 h H6). -apply Rle_lt_trans with - (Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h))) * - Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))). -rewrite Rabs_mult. -apply Rmult_le_compat_l. -apply Rabs_pos. -left; apply H9. -apply Rlt_le_trans with - (Rabs (2 * l2 * (f1 x / (Rsqr (f2 x) * f2 x))) * - Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))). -apply Rmult_lt_compat_r. -apply Rabs_pos_lt. -unfold Rdiv in |- *; unfold Rsqr in |- *; repeat apply prod_neq_R0; - assumption || idtac. -red in |- *; intro H11; rewrite H11 in H; elim (Rlt_irrefl _ H). -apply Rinv_neq_0_compat; apply prod_neq_R0. -apply prod_neq_R0. -discrR. -assumption. -assumption. -unfold Rdiv in |- *. -repeat rewrite Rinv_mult_distr; - try assumption || (unfold Rsqr in |- *; apply prod_neq_R0; assumption). -repeat rewrite Rabs_mult. -replace (Rabs 2) with 2. -replace - (2 * Rabs l2 * (Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * Rabs (/ f2 x)))) with - (Rabs l2 * (Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * (Rabs (/ f2 x) * 2)))); - [ idtac | ring ]. -replace - (Rabs l2 * Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * Rabs (/ f2 (x + h)))) with - (Rabs l2 * (Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * Rabs (/ f2 (x + h))))); - [ idtac | ring ]. -repeat apply Rmult_lt_compat_l. -apply Rabs_pos_lt; assumption. -apply Rabs_pos_lt; assumption. -apply Rabs_pos_lt; apply Rinv_neq_0_compat; unfold Rsqr in |- *; - apply prod_neq_R0; assumption. -repeat rewrite Rabs_Rinv; [ idtac | assumption | assumption ]. -rewrite <- (Rmult_comm 2). -unfold Rdiv in H10; exact H10. -symmetry in |- *; apply Rabs_right; left; prove_sup0. -right; unfold Rsqr, Rdiv in |- *. -rewrite Rinv_mult_distr; try assumption || discrR. -rewrite Rinv_mult_distr; try assumption || discrR. -rewrite Rinv_mult_distr; try assumption || discrR. -rewrite Rinv_mult_distr; try assumption || discrR. -repeat rewrite Rabs_mult. -repeat rewrite Rabs_Rinv; try assumption || discrR. -replace (Rabs eps) with eps. -replace (Rabs 8) with 8. -replace (Rabs 2) with 2. -replace 8 with (4 * 2); [ idtac | ring ]. -rewrite Rinv_mult_distr; discrR. -replace - (2 * Rabs l2 * - (Rabs (f1 x) * (/ Rabs (f2 x) * / Rabs (f2 x) * / Rabs (f2 x))) * - (Rabs (f2 x) * Rabs (f2 x) * Rabs (f2 x) * eps * - (/ 4 * / 2 * / Rabs (f1 x) * / Rabs l2))) with - (eps * / 4 * (Rabs l2 * / Rabs l2) * (Rabs (f1 x) * / Rabs (f1 x)) * - (Rabs (f2 x) * / Rabs (f2 x)) * (Rabs (f2 x) * / Rabs (f2 x)) * - (Rabs (f2 x) * / Rabs (f2 x)) * (2 * / 2)); [ idtac | ring ]. -repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption). -ring. -symmetry in |- *; apply Rabs_right; left; prove_sup0. -symmetry in |- *; apply Rabs_right; left; prove_sup. -symmetry in |- *; apply Rabs_right; left; assumption. -apply prod_neq_R0; assumption || discrR. -apply prod_neq_R0; assumption. + h <> 0 -> + Rabs h < alp_f2c -> + Rabs h < Rmin eps_f2 alp_f2 -> + f1 x <> 0 -> + l2 <> 0 -> + Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x)) < + eps / 4. +Proof. + intros. + assert (H9 := H2 h H5). + assert (H10 := H3 h H6). + apply Rle_lt_trans with + (Rabs (l2 * f1 x / (Rsqr (f2 x) * f2 (x + h))) * + Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))). + rewrite Rabs_mult. + apply Rmult_le_compat_l. + apply Rabs_pos. + left; apply H9. + apply Rlt_le_trans with + (Rabs (2 * l2 * (f1 x / (Rsqr (f2 x) * f2 x))) * + Rabs (Rsqr (f2 x) * f2 x * eps / (8 * f1 x * l2))). + apply Rmult_lt_compat_r. + apply Rabs_pos_lt. + unfold Rdiv in |- *; unfold Rsqr in |- *; repeat apply prod_neq_R0; + assumption || idtac. + red in |- *; intro H11; rewrite H11 in H; elim (Rlt_irrefl _ H). + apply Rinv_neq_0_compat; apply prod_neq_R0. + apply prod_neq_R0. + discrR. + assumption. + assumption. + unfold Rdiv in |- *. + repeat rewrite Rinv_mult_distr; + try assumption || (unfold Rsqr in |- *; apply prod_neq_R0; assumption). + repeat rewrite Rabs_mult. + replace (Rabs 2) with 2. + replace + (2 * Rabs l2 * (Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * Rabs (/ f2 x)))) with + (Rabs l2 * (Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * (Rabs (/ f2 x) * 2)))); + [ idtac | ring ]. + replace + (Rabs l2 * Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * Rabs (/ f2 (x + h)))) with + (Rabs l2 * (Rabs (f1 x) * (Rabs (/ Rsqr (f2 x)) * Rabs (/ f2 (x + h))))); + [ idtac | ring ]. + repeat apply Rmult_lt_compat_l. + apply Rabs_pos_lt; assumption. + apply Rabs_pos_lt; assumption. + apply Rabs_pos_lt; apply Rinv_neq_0_compat; unfold Rsqr in |- *; + apply prod_neq_R0; assumption. + repeat rewrite Rabs_Rinv; [ idtac | assumption | assumption ]. + rewrite <- (Rmult_comm 2). + unfold Rdiv in H10; exact H10. + symmetry in |- *; apply Rabs_right; left; prove_sup0. + right; unfold Rsqr, Rdiv in |- *. + rewrite Rinv_mult_distr; try assumption || discrR. + rewrite Rinv_mult_distr; try assumption || discrR. + rewrite Rinv_mult_distr; try assumption || discrR. + rewrite Rinv_mult_distr; try assumption || discrR. + repeat rewrite Rabs_mult. + repeat rewrite Rabs_Rinv; try assumption || discrR. + replace (Rabs eps) with eps. + replace (Rabs 8) with 8. + replace (Rabs 2) with 2. + replace 8 with (4 * 2); [ idtac | ring ]. + rewrite Rinv_mult_distr; discrR. + replace + (2 * Rabs l2 * + (Rabs (f1 x) * (/ Rabs (f2 x) * / Rabs (f2 x) * / Rabs (f2 x))) * + (Rabs (f2 x) * Rabs (f2 x) * Rabs (f2 x) * eps * + (/ 4 * / 2 * / Rabs (f1 x) * / Rabs l2))) with + (eps * / 4 * (Rabs l2 * / Rabs l2) * (Rabs (f1 x) * / Rabs (f1 x)) * + (Rabs (f2 x) * / Rabs (f2 x)) * (Rabs (f2 x) * / Rabs (f2 x)) * + (Rabs (f2 x) * / Rabs (f2 x)) * (2 * / 2)); [ idtac | ring ]. + repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption). + ring. + symmetry in |- *; apply Rabs_right; left; prove_sup0. + symmetry in |- *; apply Rabs_right; left; prove_sup. + symmetry in |- *; apply Rabs_right; left; assumption. + apply prod_neq_R0; assumption || discrR. + apply prod_neq_R0; assumption. Qed. Lemma D_x_no_cond : forall x a:R, a <> 0 -> D_x no_cond x (x + a). -intros. -unfold D_x, no_cond in |- *. -split. -trivial. -apply Rminus_not_eq. -unfold Rminus in |- *. -rewrite Ropp_plus_distr. -rewrite <- Rplus_assoc. -rewrite Rplus_opp_r. -rewrite Rplus_0_l. -apply Ropp_neq_0_compat; assumption. +Proof. + intros. + unfold D_x, no_cond in |- *. + split. + trivial. + apply Rminus_not_eq. + unfold Rminus in |- *. + rewrite Ropp_plus_distr. + rewrite <- Rplus_assoc. + rewrite Rplus_opp_r. + rewrite Rplus_0_l. + apply Ropp_neq_0_compat; assumption. Qed. Lemma Rabs_4 : - forall a b c d:R, Rabs (a + b + c + d) <= Rabs a + Rabs b + Rabs c + Rabs d. -intros. -apply Rle_trans with (Rabs (a + b) + Rabs (c + d)). -replace (a + b + c + d) with (a + b + (c + d)); [ apply Rabs_triang | ring ]. -apply Rle_trans with (Rabs a + Rabs b + Rabs (c + d)). -apply Rplus_le_compat_r. -apply Rabs_triang. -repeat rewrite Rplus_assoc; repeat apply Rplus_le_compat_l. -apply Rabs_triang. + forall a b c d:R, Rabs (a + b + c + d) <= Rabs a + Rabs b + Rabs c + Rabs d. +Proof. + intros. + apply Rle_trans with (Rabs (a + b) + Rabs (c + d)). + replace (a + b + c + d) with (a + b + (c + d)); [ apply Rabs_triang | ring ]. + apply Rle_trans with (Rabs a + Rabs b + Rabs (c + d)). + apply Rplus_le_compat_r. + apply Rabs_triang. + repeat rewrite Rplus_assoc; repeat apply Rplus_le_compat_l. + apply Rabs_triang. Qed. Lemma Rlt_4 : - forall a b c d e f g h:R, - a < b -> c < d -> e < f -> g < h -> a + c + e + g < b + d + f + h. -intros; apply Rlt_trans with (b + c + e + g). -repeat apply Rplus_lt_compat_r; assumption. -repeat rewrite Rplus_assoc; apply Rplus_lt_compat_l. -apply Rlt_trans with (d + e + g). -rewrite Rplus_assoc; apply Rplus_lt_compat_r; assumption. -rewrite Rplus_assoc; apply Rplus_lt_compat_l; apply Rlt_trans with (f + g). -apply Rplus_lt_compat_r; assumption. -apply Rplus_lt_compat_l; assumption. + forall a b c d e f g h:R, + a < b -> c < d -> e < f -> g < h -> a + c + e + g < b + d + f + h. +Proof. + intros; apply Rlt_trans with (b + c + e + g). + repeat apply Rplus_lt_compat_r; assumption. + repeat rewrite Rplus_assoc; apply Rplus_lt_compat_l. + apply Rlt_trans with (d + e + g). + rewrite Rplus_assoc; apply Rplus_lt_compat_r; assumption. + rewrite Rplus_assoc; apply Rplus_lt_compat_l; apply Rlt_trans with (f + g). + apply Rplus_lt_compat_r; assumption. + apply Rplus_lt_compat_l; assumption. Qed. Lemma Rmin_2 : forall a b c:R, a < b -> a < c -> a < Rmin b c. -intros; unfold Rmin in |- *; case (Rle_dec b c); intro; assumption. +Proof. + intros; unfold Rmin in |- *; case (Rle_dec b c); intro; assumption. Qed. Lemma quadruple : forall x:R, 4 * x = x + x + x + x. -intro; ring. +Proof. + intro; ring. Qed. Lemma quadruple_var : forall x:R, x = x / 4 + x / 4 + x / 4 + x / 4. -intro; rewrite <- quadruple. -unfold Rdiv in |- *; rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m; discrR. -reflexivity. +Proof. + intro; rewrite <- quadruple. + unfold Rdiv in |- *; rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m; discrR. + reflexivity. Qed. (**********) Lemma continuous_neq_0 : - forall (f:R -> R) (x0:R), - continuity_pt f x0 -> - f x0 <> 0 -> + forall (f:R -> R) (x0:R), + continuity_pt f x0 -> + f x0 <> 0 -> exists eps : posreal, (forall h:R, Rabs h < eps -> f (x0 + h) <> 0). -intros; unfold continuity_pt in H; unfold continue_in in H; - unfold limit1_in in H; unfold limit_in in H; elim (H (Rabs (f x0 / 2))). -intros; elim H1; intros. -exists (mkposreal x H2). -intros; assert (H5 := H3 (x0 + h)). -cut - (dist R_met (x0 + h) x0 < x -> - dist R_met (f (x0 + h)) (f x0) < Rabs (f x0 / 2)). -unfold dist in |- *; simpl in |- *; unfold R_dist in |- *; - replace (x0 + h - x0) with h. -intros; assert (H7 := H6 H4). -red in |- *; intro. -rewrite H8 in H7; unfold Rminus in H7; rewrite Rplus_0_l in H7; - rewrite Rabs_Ropp in H7; unfold Rdiv in H7; rewrite Rabs_mult in H7; - pattern (Rabs (f x0)) at 1 in H7; rewrite <- Rmult_1_r in H7. -cut (0 < Rabs (f x0)). -intro; assert (H10 := Rmult_lt_reg_l _ _ _ H9 H7). -cut (Rabs (/ 2) = / 2). -assert (Hyp : 0 < 2). -prove_sup0. -intro; rewrite H11 in H10; assert (H12 := Rmult_lt_compat_l 2 _ _ Hyp H10); - rewrite Rmult_1_r in H12; rewrite <- Rinv_r_sym in H12; - [ idtac | discrR ]. -cut (IZR 1 < IZR 2). -unfold IZR in |- *; unfold INR, nat_of_P in |- *; simpl in |- *; intro; - elim (Rlt_irrefl 1 (Rlt_trans _ _ _ H13 H12)). -apply IZR_lt; omega. -unfold Rabs in |- *; case (Rcase_abs (/ 2)); intro. -assert (Hyp : 0 < 2). -prove_sup0. -assert (H11 := Rmult_lt_compat_l 2 _ _ Hyp r); rewrite Rmult_0_r in H11; - rewrite <- Rinv_r_sym in H11; [ idtac | discrR ]. -elim (Rlt_irrefl 0 (Rlt_trans _ _ _ Rlt_0_1 H11)). -reflexivity. -apply (Rabs_pos_lt _ H0). -ring. -assert (H6 := Req_dec x0 (x0 + h)); elim H6; intro. -intro; rewrite <- H7; unfold dist, R_met in |- *; unfold R_dist in |- *; - unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; - apply Rabs_pos_lt. -unfold Rdiv in |- *; apply prod_neq_R0; - [ assumption | apply Rinv_neq_0_compat; discrR ]. -intro; apply H5. -split. -unfold D_x, no_cond in |- *. -split; trivial || assumption. -assumption. -change (0 < Rabs (f x0 / 2)) in |- *. -apply Rabs_pos_lt; unfold Rdiv in |- *; apply prod_neq_R0. -assumption. -apply Rinv_neq_0_compat; discrR. -Qed.
\ No newline at end of file +Proof. + intros; unfold continuity_pt in H; unfold continue_in in H; + unfold limit1_in in H; unfold limit_in in H; elim (H (Rabs (f x0 / 2))). + intros; elim H1; intros. + exists (mkposreal x H2). + intros; assert (H5 := H3 (x0 + h)). + cut + (dist R_met (x0 + h) x0 < x -> + dist R_met (f (x0 + h)) (f x0) < Rabs (f x0 / 2)). + unfold dist in |- *; simpl in |- *; unfold R_dist in |- *; + replace (x0 + h - x0) with h. + intros; assert (H7 := H6 H4). + red in |- *; intro. + rewrite H8 in H7; unfold Rminus in H7; rewrite Rplus_0_l in H7; + rewrite Rabs_Ropp in H7; unfold Rdiv in H7; rewrite Rabs_mult in H7; + pattern (Rabs (f x0)) at 1 in H7; rewrite <- Rmult_1_r in H7. + cut (0 < Rabs (f x0)). + intro; assert (H10 := Rmult_lt_reg_l _ _ _ H9 H7). + cut (Rabs (/ 2) = / 2). + assert (Hyp : 0 < 2). + prove_sup0. + intro; rewrite H11 in H10; assert (H12 := Rmult_lt_compat_l 2 _ _ Hyp H10); + rewrite Rmult_1_r in H12; rewrite <- Rinv_r_sym in H12; + [ idtac | discrR ]. + cut (IZR 1 < IZR 2). + unfold IZR in |- *; unfold INR, nat_of_P in |- *; simpl in |- *; intro; + elim (Rlt_irrefl 1 (Rlt_trans _ _ _ H13 H12)). + apply IZR_lt; omega. + unfold Rabs in |- *; case (Rcase_abs (/ 2)); intro. + assert (Hyp : 0 < 2). + prove_sup0. + assert (H11 := Rmult_lt_compat_l 2 _ _ Hyp r); rewrite Rmult_0_r in H11; + rewrite <- Rinv_r_sym in H11; [ idtac | discrR ]. + elim (Rlt_irrefl 0 (Rlt_trans _ _ _ Rlt_0_1 H11)). + reflexivity. + apply (Rabs_pos_lt _ H0). + ring. + assert (H6 := Req_dec x0 (x0 + h)); elim H6; intro. + intro; rewrite <- H7; unfold dist, R_met in |- *; unfold R_dist in |- *; + unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; + apply Rabs_pos_lt. + unfold Rdiv in |- *; apply prod_neq_R0; + [ assumption | apply Rinv_neq_0_compat; discrR ]. + intro; apply H5. + split. + unfold D_x, no_cond in |- *. + split; trivial || assumption. + assumption. + change (0 < Rabs (f x0 / 2)) in |- *. + apply Rabs_pos_lt; unfold Rdiv in |- *; apply prod_neq_R0. + assumption. + apply Rinv_neq_0_compat; discrR. +Qed. |