proposition: Lemma Abs_sum_maj : forall {R : ConstructiveReals} (un vn : nat -> CRcarrier R), (forall n:nat, CRabs R (un n) <= (vn n)) -> forall n p:nat, (CRabs R (CRsum un n - CRsum un p) <= CRsum vn (Init.Nat.max n p) - CRsum vn (Init.Nat.min n p)).
proof: Proof. intros. destruct (le_lt_dec n p). - destruct (Nat.le_exists_sub n p) as [k [maj _]]. + assumption. + subst p. rewrite max_r. 2:assumption. rewrite min_l. 2:assumption. setoid_replace (CRsum un n - CRsum un (k + n)) with (-(CRsum un (k + n) - CRsum un n)). * rewrite CRabs_opp. destruct k. -- simpl. unfold CRminus. rewrite CRplus_opp_r. rewrite CRplus_opp_r. rewrite CRabs_right; apply CRle_refl. -- replace (S k + n)%nat with (S n + k)%nat. ++ unfold CRminus. rewrite sum_assoc. rewrite sum_assoc. rewrite CRplus_comm. rewrite <- CRplus_assoc. rewrite CRplus_opp_l. rewrite CRplus_0_l. rewrite CRplus_comm. rewrite <- CRplus_assoc. rewrite CRplus_opp_l. rewrite CRplus_0_l. apply (CRle_trans _ (CRsum (fun k0 : nat => CRabs R (un (S n + k0)%nat)) k)). ** apply multiTriangleIneg. ** apply sum_Rle. intros. apply H. ++ rewrite Nat.add_comm, Nat.add_succ_r. reflexivity. * unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive, CRplus_comm. reflexivity. - destruct (Nat.le_exists_sub p n) as [k [maj _]]. + unfold lt in l. apply (Nat.le_trans p (S p)). * apply le_S. apply Nat.le_refl. * assumption. + subst n. rewrite max_l. * rewrite min_r. -- destruct k. ++ simpl. unfold CRminus. rewrite CRplus_opp_r. rewrite CRplus_opp_r. rewrite CRabs_right. ** apply CRle_refl. ** apply CRle_refl. ++ replace (S k + p)%nat with (S p + k)%nat. ** unfold CRminus. rewrite sum_assoc. rewrite sum_assoc. rewrite CRplus_comm. rewrite <- CRplus_assoc. rewrite CRplus_opp_l. rewrite CRplus_0_l. rewrite CRplus_comm. rewrite <- CRplus_assoc. rewrite CRplus_opp_l. rewrite CRplus_0_l. apply (CRle_trans _ (CRsum (fun k0 : nat => CRabs R (un (S p + k0)%nat)) k)). { apply multiTriangleIneg. } apply sum_Rle. intros. apply H. ** rewrite Nat.add_comm, Nat.add_succ_r. reflexivity. -- apply (Nat.le_trans p (S p)). ++ apply le_S. apply Nat.le_refl. ++ assumption. * apply (Nat.le_trans p (S p)). -- apply le_S. apply Nat.le_refl. -- assumption. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits