proposition: Lemma series_cv_abs_remainder : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (s sAbs : CRcarrier R) (n : nat), series_cv u s -> series_cv (fun n => CRabs R (u n)) sAbs -> CRabs R (CRsum u n - s) <= sAbs - CRsum (fun n => CRabs R (u n)) n.
proof: Proof. intros. apply (CR_cv_le (fun N => CRabs R (CRsum u n - (CRsum u (n + N)))) (fun N => CRsum (fun n : nat => CRabs R (u n)) (n + N) - CRsum (fun n : nat => CRabs R (u n)) n)). - intro N. destruct N. + rewrite Nat.add_0_r. unfold CRminus. rewrite CRplus_opp_r. rewrite CRplus_opp_r. rewrite CRabs_right. * apply CRle_refl. * apply CRle_refl. + rewrite Nat.add_succ_r. replace (S (n + N)) with (S n + N)%nat. 2: reflexivity. unfold CRminus. rewrite sum_assoc. rewrite sum_assoc. rewrite CRopp_plus_distr. rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l, CRabs_opp. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l. rewrite CRplus_0_l. apply multiTriangleIneg. - apply CR_cv_dist_cont. intros eps. specialize (H eps) as [N lim]. exists N. intros. rewrite Nat.add_comm. apply lim. apply (Nat.le_trans N i). + assumption. + rewrite <- (Nat.add_0_r i), <- Nat.add_assoc. apply Nat.add_le_mono_l, Nat.le_0_l. - apply CR_cv_plus. 2: apply CR_cv_const. intros eps. specialize (H0 eps) as [N lim]. exists N. intros. rewrite Nat.add_comm. apply lim. apply (Nat.le_trans N i). + assumption. + rewrite <- (Nat.add_0_r i), <- Nat.add_assoc. apply Nat.add_le_mono_l, Nat.le_0_l. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits