proposition: Lemma representationPositive : forall {IS : IntegrationSpace} (fInt : @IntegralRepresentation IS), nonNegFunc (XinfiniteSumAbs (IntFn fInt)) -> 0 <= IntegralSeries fInt.
proof: Proof. intros IS [fn fnL sumAbsIFn H] H0. destruct (splitIntegralSumPosNeg fn fnL sumAbsIFn H) as [sumIPosFn [sumINegFn [[limPos limNeg] splitIntegral]]]. setoid_replace (IntegralSeries {| IntFn := fn; IntFnL := fnL; IntAbsSum := sumAbsIFn; IntAbsSumCv := H |}) with (sumIPosFn - sumINegFn). rewrite <- (CRplus_opp_r sumINegFn). apply CRplus_le_compat. 2: apply CRle_refl. intro absurd. destruct (splitInfiniteSumMaj (fun n : nat => I IS (XnegPart (fn n)) (LnegPartStable (fn n) (fnL n))) sumIPosFn sumINegFn limNeg) as [M H1]. assumption. destruct (Icontinuous IS (Xsum (fun n:nat => XnegPart (fn n)) M) (fun n:nat => Xplus (XposPart (fn n)) match le_dec n M with | left _ => Izero IS | _ => XnegPart (fn n) end) (LsumStable (fun n : nat => XnegPart (fn n)) (fun n => LnegPartStable (fn n) (fnL n)) M) (fun n:nat => LplusStable (ElemFunc IS) (XposPart (fn n)) (match le_dec n M with | left _ => Izero IS | _ => XnegPart (fn n) end) (LposPartStable (fn n) (fnL n)) (if le_dec n M as s return (L (ElemFunc IS) (if s then Izero IS else XnegPart (fn n))) then Izero_is_L IS else LnegPartStable (fn n) (fnL n))) ) as [[x xS xdfn] [sumPosNegFX [H2 H3]]]. - intros. intros z xdf. destruct (le_dec n M). destruct xdf. rewrite (applyXplus (XposPart (fn n)) (Izero IS)), <- (CRplus_0_r 0). apply CRplus_le_compat. apply applyXposPartNonNeg. rewrite applyIzero. apply CRle_refl. destruct xdf. rewrite (applyXplus (XposPart (fn n)) (XnegPart (fn n))), <- (CRplus_0_r 0). apply CRplus_le_compat. apply applyXposPartNonNeg. apply XnegPartNonNeg. - exists (sumIPosFn + (sumINegFn - CRsum (fun n : nat => I IS (XnegPart (fn n)) (LnegPartStable (fn n) (fnL n))) M)). split. + apply (series_cv_eq (fun n : nat => I IS (XposPart (fn n)) (LposPartStable (fn n) (fnL n)) + (I IS (if le_dec n M then Izero IS else XnegPart (fn n)) (if le_dec n M as s return (L (ElemFunc IS) (if s then Izero IS else XnegPart (fn n))) then Izero_is_L IS else LnegPartStable (fn n) (fnL n))))). intros. rewrite Iadditive. reflexivity. apply series_cv_plus. assumption. apply (series_cv_eq (fun n : nat => if le_dec n M then 0 else I IS (XnegPart (fn n)) (LnegPartStable (fn n) (fnL n)))). intros. destruct (le_dec n M). rewrite Izero_is_zero. reflexivity. reflexivity. apply infinite_sum_truncate_below. assumption. + rewrite IadditiveIterate. unfold CRminus. rewrite <- CRplus_assoc. apply CRltEpsilon. assumption. - pose proof (fun n:nat => domainPlusPosPartInc _ _ _ x (xdfn n)) as pxn. apply (series_cv_eq (fun n : nat => partialApply (Xplus (XposPart (fn n)) (if le_dec n M then Izero IS else XnegPart (fn n))) x (xdfn n)) (fun n : nat => CRmax 0 (partialApply (fn n) x (pxn n)) + (if le_dec n M then 0 else CRmax 0 (- partialApply (fn n) x (pxn n))))) in H2. assert (series_cv (fun n : nat => (if le_dec n M then CRmax 0 (- partialApply (fn n) x (pxn n)) else 0)) (CRsum (fun k => CRmax 0 (- partialApply (fn k) x (pxn k))) M)). { intros eps. exists M. intros. rewrite sum_truncate_above. unfold CRminus. rewrite CRplus_opp_r. rewrite CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. exact H4. } apply (series_cv_plus (fun n : nat => (CRmax 0 (partialApply (fn n) x (pxn n)) + (if le_dec n M then 0 else CRmax 0 (- partialApply (fn n) x (pxn n))))) (fun n : nat => if le_dec n M then CRmax 0 (- partialApply (fn n) x (pxn n)) else 0) sumPosNegFX (CRsum (fun k => CRmax 0 (- partialApply (fn k) x (pxn k))) M) H2) in H4. apply (series_cv_eq (fun n : nat => (CRmax 0 (partialApply (fn n) x (pxn n)) + (if le_dec n M then 0 else CRmax 0 (- partialApply (fn n) x (pxn n))) + (if le_dec n M then CRmax 0 (- partialApply (fn n) x (pxn n)) else 0))) (fun n : nat => CRabs _ (partialApply (fn n) x (pxn n)))) in H4. unfold nonNegFunc in H0. pose proof (domainInfiniteSumAbsInc fn x pxn (sumPosNegFX + CRsum (fun k : nat => CRmax 0 (- partialApply (fn k) x (pxn k))) M) H4) as y. specialize (H0 x y). destruct y as [yn ycv]; simpl in H0. apply series_cv_abs_le in H0. destruct H0 as [sumFX [H0 i]]. destruct (splitSumAbsPosNeg _ fn x pxn (sumPosNegFX + CRsum (fun k : nat => CRmax 0 (- partialApply (fn k) x (pxn k))) M) H4) as [H6 H7]. destruct H6 as [sumPosFnX [H6 limPosX]]. destruct H7 as [sumNegFnX [H7 limNegX]]. assert (sumPosFnX < sumNegFnX). { apply (CRle_lt_trans sumPosFnX sumPosNegFX). apply (series_cv_scale (-(1)) sumPosFnX) in limPosX. apply (series_cv_plus (fun n : nat => (CRmax 0 (partialApply (fn n) x (pxn n)) + (if le_dec n M then 0 else CRmax 0 (- partialApply (fn n) x (pxn n))))) (fun n : nat => (CRmax 0 (partialApply (fn n) x (pxn n)) * -(1))) sumPosNegFX (sumPosFnX * -(1))) in limPosX. apply series_cv_nonneg in limPosX. assert (sumPosFnX * (-(1)) == - sumPosFnX) as H8. rewrite <- CRopp_mult_distr_r, CRmult_1_r. reflexivity. rewrite H8 in limPosX. apply (CRplus_le_compat_l sumPosFnX) in limPosX. simpl in limPosX. unfold CRminus in limPosX. rewrite CRplus_0_r, CRplus_comm, CRplus_assoc, CRplus_opp_l, CRplus_0_r in limPosX. exact limPosX. intro n. assert (CRmax 0 (partialApply (fn n) x (pxn n)) + (if le_dec n M then 0 else CRmax 0 (- partialApply (fn n) x (pxn n))) + CRmax 0 (partialApply (fn n) x (pxn n)) * -(1) == (if le_dec n M then 0 else CRmax 0 (- partialApply (fn n) x (pxn n)))) as H8. rewrite <- CRopp_mult_distr_r, CRmult_1_r, CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. reflexivity. rewrite H8. destruct (le_dec n M). apply CRle_refl. apply CRmax_l. assumption. apply (CRlt_le_trans sumPosNegFX (partialApply (Xsum (fun n : nat => XnegPart (fn n)) M) x xS)). assumption. pose proof (fun n:nat => pair (pxn n) (pxn n)) as pxnn. rewrite (applyXsum (fun n : nat => XnegPart (fn n)) M x _ pxnn). rewrite <- (CRsum_eq (fun n:nat => CRmax 0 (- partialApply (fn n) x (pxn n)))). apply growing_ineq. intros p. simpl. rewrite <- CRplus_0_r, CRplus_assoc. apply CRplus_le_compat_l. rewrite CRplus_0_l. apply CRmax_l. assumption. intros. rewrite <- (applyXnegPart (fn i0)). apply DomainProp. } assert (sumFX == sumPosFnX - sumNegFnX). { apply (CR_cv_unique (CRsum (fun k : nat => partialApply (fn k) x (pxn k)))). apply (series_cv_eq (fun k : nat => partialApply (fn k) x (yn k))). intro n. apply DomainProp. apply i. apply infiniteSumPosNegParts. assumption. assumption. } rewrite H8 in H0. apply (CRplus_le_compat_l sumNegFnX) in H0. unfold CRminus in H0. rewrite CRplus_0_r, CRplus_comm, CRplus_assoc, CRplus_opp_l, CRplus_0_r in H0. apply H0. assumption. intros. destruct (le_dec n M). rewrite sumPosNegPart. rewrite CRplus_0_r. reflexivity. rewrite sumPosNegPart. rewrite CRplus_0_r. reflexivity. intro n. apply applyPlusTruncated. - apply (CR_cv_unique (CRsum (fun n : nat => I IS (fn n) (fnL n)))). simpl. destruct (series_cv_maj (fun n : nat => I IS (fn n) (fnL n)) (fun k : nat => Iabs (fn k) (fnL k)) sumAbsIFn (fun n : nat => integralAbsMaj (fn n) (fnL n)) H). apply p. assumption. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase