proposition: Lemma sum_cv_maj : forall (An:nat -> R) (fn:nat -> R -> R) (x l1 l2:R), Un_cv (fun n:nat => SP fn n x) l1 -> Un_cv (fun n:nat => sum_f_R0 An n) l2 -> (forall n:nat, Rabs (fn n x) <= An n) -> Rabs l1 <= l2.
proof: Proof. intros; destruct (total_order_T (Rabs l1) l2) as [[Hlt|Heq]|Hgt]. - left; apply Hlt. - right; apply Heq. - cut (forall n0:nat, Rabs (SP fn n0 x) <= sum_f_R0 An n0). { intro; cut (0 < (Rabs l1 - l2) / 2). - intro; unfold Un_cv in H, H0. elim (H _ H3); intros Na H4. elim (H0 _ H3); intros Nb H5. set (N := max Na Nb). unfold Rdist in H4, H5. cut (Rabs (sum_f_R0 An N - l2) < (Rabs l1 - l2) / 2). 1:intro; cut (Rabs (Rabs l1 - Rabs (SP fn N x)) < (Rabs l1 - l2) / 2). 1:intro; cut (sum_f_R0 An N < (Rabs l1 + l2) / 2). 1:intro; cut ((Rabs l1 + l2) / 2 < Rabs (SP fn N x)). 1:intro; cut (sum_f_R0 An N < Rabs (SP fn N x)). 1:intro; assert (H11 := H2 N). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H11 H10)). + apply Rlt_trans with ((Rabs l1 + l2) / 2); assumption. + destruct (Rcase_abs (Rabs l1 - Rabs (SP fn N x))) as [Hlt|Hge]. * apply Rlt_trans with (Rabs l1). -- apply Rmult_lt_reg_l with 2. ++ prove_sup0. ++ unfold Rdiv; rewrite (Rmult_comm 2); rewrite Rmult_assoc; rewrite Rinv_l. ** rewrite Rmult_1_r; rewrite <-Rplus_diag; apply Rplus_lt_compat_l; apply Hgt. ** discrR. -- apply (Rminus_lt _ _ Hlt). * rewrite (Rabs_right _ Hge) in H7. apply Rplus_lt_reg_l with ((Rabs l1 - l2) / 2 - Rabs (SP fn N x)). replace ((Rabs l1 - l2) / 2 - Rabs (SP fn N x) + (Rabs l1 + l2) / 2) with (Rabs l1 - Rabs (SP fn N x)). -- unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; apply H7. -- unfold Rdiv; rewrite Rmult_plus_distr_r; rewrite <- (Rmult_comm (/ 2)); rewrite Rmult_minus_distr_l; repeat rewrite (Rmult_comm (/ 2)); pattern (Rabs l1) at 1; rewrite <-Rplus_half_diag; unfold Rdiv in |- *; ring. + destruct (Rcase_abs (sum_f_R0 An N - l2)) as [Hlt|Hge]. * apply Rlt_trans with l2. -- apply (Rminus_lt _ _ Hlt). -- apply Rmult_lt_reg_l with 2. ++ prove_sup0. ++ rewrite <-(Rplus_diag l2); unfold Rdiv; rewrite (Rmult_comm 2); rewrite Rmult_assoc; rewrite Rinv_l. ** rewrite Rmult_1_r; rewrite (Rplus_comm (Rabs l1)); apply Rplus_lt_compat_l; apply Hgt. ** discrR. * rewrite (Rabs_right _ Hge) in H6; apply Rplus_lt_reg_l with (- l2). replace (- l2 + (Rabs l1 + l2) / 2) with ((Rabs l1 - l2) / 2). -- rewrite Rplus_comm; apply H6. -- unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite Rmult_minus_distr_l; rewrite Rmult_plus_distr_r; pattern l2 at 2; rewrite <-Rplus_half_diag; repeat rewrite (Rmult_comm (/ 2)); rewrite Ropp_plus_distr; unfold Rdiv; ring. + apply Rle_lt_trans with (Rabs (SP fn N x - l1)). * rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply Rabs_triang_inv2. * apply H4; unfold ge, N; apply Nat.le_max_l. + apply H5; unfold ge, N; apply Nat.le_max_r. - unfold Rdiv; apply Rmult_lt_0_compat. + apply Rplus_lt_reg_l with l2. rewrite Rplus_0_r; replace (l2 + (Rabs l1 - l2)) with (Rabs l1); [ apply Hgt | ring ]. + apply Rinv_0_lt_compat; prove_sup0. } intros; induction n0 as [| n0 Hrecn0]. + unfold SP; simpl; apply H1. + unfold SP; simpl. apply Rle_trans with (Rabs (sum_f_R0 (fun k:nat => fn k x) n0) + Rabs (fn (S n0) x)). * apply Rabs_triang. * apply Rle_trans with (sum_f_R0 An n0 + Rabs (fn (S n0) x)). -- do 2 rewrite <- (Rplus_comm (Rabs (fn (S n0) x))). apply Rplus_le_compat_l; apply Hrecn0. -- apply Rplus_le_compat_l; apply H1. Qed.
imports: Rbase Rfunctions Rseries Rcomplete