proposition: Lemma infiniteSumPosNegParts : forall {R : ConstructiveReals} (X : Set) (fn : nat -> PartialFunction X) (x : X) (xn : forall n:nat, Domain (fn n) x) (pos neg : CRcarrier R), series_cv (fun n => CRmax 0 (partialApply (fn n) x (xn n))) pos -> series_cv (fun n => CRmax 0 (- partialApply (fn n) x (xn n))) neg -> series_cv (fun n => partialApply (fn n) x (xn n)) (pos - neg).
proof: Proof. intros. apply (series_cv_scale (-(1)) neg) in H0. apply (series_cv_plus (fun n : nat => CRmax 0 (partialApply (fn n) x (xn n))) (fun n : nat => (CRmax 0 (- partialApply (fn n) x (xn n)) * -(1))) pos (neg * -(1)) H) in H0. assert (pos + neg * -(1) == pos - neg). rewrite <- CRopp_mult_distr_r, CRmult_1_r. reflexivity. rewrite H1 in H0. apply (series_cv_eq (fun n : nat => (CRmax 0 (partialApply (fn n) x (xn n)) + CRmax 0 (- partialApply (fn n) x (xn n)) * -(1))) (fun n : nat => partialApply (fn n) x (xn n))). intro n. rewrite <- (CRopp_mult_distr_r _ 1). rewrite CRmult_1_r. symmetry. apply minusPosNegPart. apply H0. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase