proposition: Lemma splitSumAbsPosNeg : forall {R : ConstructiveReals} (X : Set) (fn : nat -> PartialFunction X) (x : X) (xn : forall n:nat, Domain (fn n) x) (A : CRcarrier R), series_cv (fun n => CRabs _ (partialApply (fn n) x (xn n))) A -> prod { pos : CRcarrier R & prod (pos <= A) (series_cv (fun n => CRmax 0 (partialApply (fn n) x (xn n))) pos) } { neg : CRcarrier R & prod (neg <= A) (series_cv (fun n => CRmax 0 (- partialApply (fn n) x (xn n))) neg) }.
proof: Proof. intros. split. - destruct (series_cv_maj (fun n => CRmax 0 (partialApply (fn n) x (xn n))) (fun n : nat => CRabs _ (partialApply (fn n) x (xn n))) A) as [l cvl]. intro n. simpl. rewrite CRabs_right. apply CRmax_lub. apply CRabs_pos. apply CRle_abs. apply CRmax_l. assumption. exists l. split; apply cvl. - destruct (series_cv_maj (fun n => CRmax 0 (- partialApply (fn n) x (xn n))) (fun n : nat => CRabs _ (partialApply (fn n) x (xn n))) A) as [l cvl]. intro n. simpl. rewrite CRabs_right. apply CRmax_lub. apply CRabs_pos. rewrite <- CRabs_opp. apply CRle_abs. apply CRmax_l. assumption. exists l. split; apply cvl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase