proposition: Lemma splitIntegralSumPosNeg : forall {IS : IntegrationSpace} (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnL : forall n:nat, L (ElemFunc IS) (fn n)) (sumAbsIFn : CRcarrier (RealT (ElemFunc IS))), (series_cv (fun n => Iabs (fn n) (fnL n)) sumAbsIFn) -> { sumIPosFn : CRcarrier _ & { sumINegFn : CRcarrier _ & series_cv (fun n0 : nat => I IS (XposPart (fn n0)) (LposPartStable (fn n0) (fnL n0))) sumIPosFn * series_cv (fun n0 : nat => I IS (XnegPart (fn n0)) (LnegPartStable (fn n0) (fnL n0))) sumINegFn * series_cv (fun n => I IS (fn n) (fnL n)) (sumIPosFn - sumINegFn) }}%type.
proof: Proof. intros. destruct (series_cv_maj (fun n0 : nat => I IS (XposPart (fn n0)) (LposPartStable (fn n0) (fnL n0))) (fun n0 : nat => Iabs (fn n0) (fnL n0)) sumAbsIFn) as [sumIPosFn [limPos _]]. { intro n. apply (CRle_trans _ (Iabs (XposPart (fn n)) (LposPartStable (fn n) (fnL n)))). apply integralAbsMaj. apply INonDecreasing. intros. rewrite applyXabs, CRabs_right. 2: apply applyXposPartNonNeg. rewrite <- (DomainProp (XposPart (fn n)) x (y, y)). rewrite (applyXposPart (fn n)). rewrite applyXabs. apply CRmax_lub. apply CRabs_pos. apply CRle_abs. } assumption. destruct (series_cv_maj (fun n0 : nat => I IS (XnegPart (fn n0)) (LnegPartStable (fn n0) (fnL n0))) (fun n0 : nat => Iabs (fn n0) (fnL n0)) sumAbsIFn) as [sumINegFn [limNeg _]]. { intro n. apply (CRle_trans _ (Iabs (XnegPart (fn n)) (LnegPartStable (fn n) (fnL n)))). apply integralAbsMaj. apply INonDecreasing. intros. rewrite applyXabs, CRabs_right. 2: apply XnegPartNonNeg. rewrite <- (DomainProp (XnegPart (fn n)) x (y,y)). rewrite (applyXnegPart (fn n)). rewrite applyXabs. apply CRmax_lub. apply CRabs_pos. rewrite <- CRabs_opp. apply CRle_abs. } apply H. exists sumIPosFn. exists sumINegFn. repeat split. assumption. assumption. apply (series_cv_scale (-(1)) sumINegFn) in limNeg. apply (series_cv_plus (fun n0 : nat => I IS (XposPart (fn n0)) (LposPartStable (fn n0) (fnL n0))) (fun n : nat => (I IS (XnegPart (fn n)) (LnegPartStable (fn n) (fnL n)) * -(1))) sumIPosFn (sumINegFn * -(1)) limPos) in limNeg. apply (series_cv_eq (fun n : nat => (I IS (XposPart (fn n)) (LposPartStable (fn n) (fnL n)) + I IS (XnegPart (fn n)) (LnegPartStable (fn n) (fnL n)) * -(1))) (fun n : nat => I IS (fn n) (fnL n))) in limNeg. apply (CR_cv_proper _ (sumIPosFn + sumINegFn * - (1))). exact limNeg. rewrite <- CRopp_mult_distr_r, CRmult_1_r. reflexivity. intro n. assert ((I IS (XposPart (fn n)) (LposPartStable (fn n) (fnL n)) + I IS (XnegPart (fn n)) (LnegPartStable (fn n) (fnL n)) * -(1)) == (I IS (XposPart (fn n)) (LposPartStable (fn n) (fnL n)) - I IS (XnegPart (fn n)) (LnegPartStable (fn n) (fnL n)))). rewrite <- CRopp_mult_distr_r, CRmult_1_r. reflexivity. rewrite H0. clear H0. rewrite <- splitIntegralPosNeg. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase