proposition: Lemma series_cv_maj : forall {R : ConstructiveReals} (un vn : nat -> CRcarrier R) (s : CRcarrier R), (forall n:nat, CRabs R (un n) <= vn n) -> series_cv vn s -> { l : CRcarrier R & prod (series_cv un l) (l <= s) }.
proof: Proof. intros. destruct (CR_complete R (CRsum un)). - intros n. specialize (H0 (2*n)%positive) as [N maj]. exists N. intros i j H0 H1. apply (CRle_trans _ (CRsum vn (max i j) - CRsum vn (min i j))). + apply Abs_sum_maj. apply H. + setoid_replace (CRsum vn (max i j) - CRsum vn (min i j)) with (CRabs R (CRsum vn (max i j) - (CRsum vn (min i j)))). * setoid_replace (CRsum vn (Init.Nat.max i j) - CRsum vn (Init.Nat.min i j)) with (CRsum vn (Init.Nat.max i j) - s - (CRsum vn (Init.Nat.min i j) - s)). -- apply (CRle_trans _ _ _ (CRabs_triang _ _)). setoid_replace (1#n)%Q with ((1#2*n) + (1#2*n))%Q. ++ rewrite CR_of_Q_plus. apply CRplus_le_compat. ** apply maj. apply (Nat.le_trans _ i). { assumption. } apply Nat.le_max_l. ** rewrite CRabs_opp. apply maj. apply Nat.min_case. { apply (Nat.le_trans _ i). - assumption. - apply Nat.le_refl. } assumption. ++ rewrite Qinv_plus_distr. reflexivity. -- unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. ++ reflexivity. ++ rewrite CRopp_plus_distr, CRopp_involutive. rewrite CRplus_comm, CRplus_assoc, CRplus_opp_r, CRplus_0_r. reflexivity. * rewrite CRabs_right. -- reflexivity. -- rewrite <- (CRplus_opp_r (CRsum vn (Init.Nat.min i j))). apply CRplus_le_compat. ++ apply pos_sum_more. ** intros. apply (CRle_trans _ (CRabs R (un k))), H. apply CRabs_pos. ** apply (Nat.le_trans _ i), Nat.le_max_l. apply Nat.le_min_l. ++ apply CRle_refl. - exists x. split. + assumption. + apply (CRplus_le_reg_r (-x)). rewrite CRplus_opp_r. apply (CR_cv_bound_down (fun n => CRsum vn n - CRsum un n) _ _ 0). * intros. rewrite <- (CRplus_opp_r (CRsum un n)). apply CRplus_le_compat. -- apply sum_Rle. intros. apply (CRle_trans _ (CRabs R (un k))). ++ apply CRle_abs. ++ apply H. -- apply CRle_refl. * apply CR_cv_plus. -- assumption. -- apply CR_cv_opp. assumption. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits