proposition: Lemma domainXinfinitePosNeg : forall {R : ConstructiveReals} {X : Set} (fn : nat -> @PartialFunction R X) (x : X), (Domain (XinfiniteSumAbs (fun n => XposPart (fn n))) x) -> (Domain (XinfiniteSumAbs (fun n => XnegPart (fn n))) x) -> Domain (XinfiniteSumAbs fn) x.
proof: Proof. intros. destruct H, H0. exists (fun n => fst (x0 n)). apply CR_complete in c. apply CR_complete in c0. destruct c,c0. apply (Rcv_cauchy_mod _ (x2+x3)). pose proof (series_cv_plus _ _ _ _ c c0). apply (series_cv_eq (fun n : nat => (fun n0 : nat => CRabs R (partialApply (XposPart (fn n0)) x (x0 n0))) n + (fun n0 : nat => CRabs R (partialApply (XnegPart (fn n0)) x (x1 n0))) n)). intro n. rewrite CRabs_right, CRabs_right. simpl. destruct (x0 n), (x1 n). rewrite <- CRmult_plus_distr_l. rewrite <- CRopp_mult_distr_l, CRmult_1_l, CRplus_comm, CRplus_assoc. rewrite <- (CRplus_assoc (- partialApply (fn n) x d2)). rewrite (DomainProp (fn n) x d2 d), CRplus_opp_l, CRplus_0_l. apply (CRmult_eq_reg_l (CR_of_Q R 2)). right. apply CR_of_Q_pos. reflexivity. rewrite <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace (2 * (1 # 2))%Q with 1%Q. 2: reflexivity. rewrite (CR_of_Q_plus R 1 1), CRmult_1_l. rewrite CRmult_plus_distr_r, CRmult_1_l. rewrite (DomainProp (fn n) x (fst (d,d0)) d0), (DomainProp (fn n) x d1 d0). reflexivity. apply applyXnegPartNonNeg. apply applyXposPartNonNeg. exact H. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity