proposition: Lemma CSUCIntegralContinuous {R : ConstructiveReals} : @ElemIntegralContinuous (@ElemCSUC R) IntegralCSUC.
proof: Proof. intros. apply IcontinuousClassic. - apply CSUCIntegralHomogeneous. - apply CSUCIntegralAdditiveIterate. - intros g gL. assert (nonNegFunc (PartializeFunc (CRcarrier R) (CSUCUnitTrapeze (CSUC_low g gL) (CSUC_high g gL) 1 (CRzero_lt_one R)))) as ZnonNeg. { intros x xdf. simpl. apply (CSUCTrapezeBounded (CSUC_low g gL) (CSUC_high g gL) 1 x (CRzero_lt_one R)). apply (CSUC_lowHigh g gL). } exists (existT _ (PartializeFunc (CRcarrier R) (CSUCUnitTrapeze (CSUC_low g gL) (CSUC_high g gL) 1 (CRzero_lt_one R))) (pair (CSUCTrapeze_IS_CSUC (CSUC_low g gL) (CSUC_high g gL) 1 (CRzero_lt_one R) (CSUC_lowHigh g gL)) ZnonNeg)). intros. assert (forall (k : nat) (x : CRcarrier R), (0 <= (fun n : nat => TotalizeFunc (CRcarrier R) (fn n) (CSUC_fullDomain (fn n) (fnL n))) k x)) as fnPos. { intros. unfold TotalizeFunc. specialize (H k). clear H0. unfold nonNegFunc in H. destruct (fnL k), (fn k); simpl; simpl in H. apply H. } destruct H0 as [sIfn [icv imaj]]. assert (forall n : nat, (CRabs _ ((fun k : nat => UC_integral ((fun n0 : nat => TotalizeFunc (CRcarrier R) (fn n0) (CSUC_fullDomain (fn n0) (fnL n0))) k) (CSUC_low g gL) (CSUC_high g gL) ((fun n0 : nat => CSUC_cont_mod (fn n0) (fnL n0)) k) ((fun n0 : nat => fst (CSUC_adapt (fn n0) (fnL n0))) k) (CSUC_lowHigh g gL) ) n) <= (fun n0 : nat => UC_integral (TotalizeFunc (CRcarrier R) (fn n0) (CSUC_fullDomain (fn n0) (fnL n0))) (CSUC_low (fn n0) (fnL n0)) (CSUC_high (fn n0) (fnL n0)) (CSUC_cont_mod (fn n0) (fnL n0)) (fst (CSUC_adapt (fn n0) (fnL n0))) (CSUC_lowHigh (fn n0) (fnL n0))) n)). { intro n. rewrite CRabs_right. apply CSUC_extend_pos. apply H. apply UC_integral_pos. intros. specialize (H n). destruct (fnL n), (fn n); simpl. apply H. } destruct (series_cv_maj _ _ sIfn H0 icv) as [sIfnTrunc [scv smaj]]. assert (sIfnTrunc < UC_integral (TotalizeFunc (CRcarrier R) g (CSUC_fullDomain g gL)) (CSUC_low g gL) (CSUC_high g gL) (CSUC_cont_mod g gL) (fst (CSUC_adapt g gL)) (CSUC_lowHigh g gL) ) as majInt. { apply (CRle_lt_trans _ sIfn). apply smaj. exact imaj. } destruct (DestructCSUCposPoint R (TotalizeFunc (CRcarrier R) g (CSUC_fullDomain _ gL)) (fun n => TotalizeFunc (CRcarrier R) (fn n) (CSUC_fullDomain _ (fnL n))) fnPos (fun n => CSUC_cont_mod _ (fnL n)) (fun n => fst (CSUC_adapt _ (fnL n))) (CSUC_cont_mod _ gL) (CSUC_low _ gL) (CSUC_high _ gL) (CSUC_lowHigh _ gL) (CSUC_adapt _ gL) (existT _ sIfnTrunc (pair scv majInt))) as [l lcv]. exists (Build_CommonPointFunSeq _ _ g fn l (CSUC_fullDomain g gL l) (fun n => CSUC_fullDomain (fn n) (fnL n) l)). unfold cpx, cpxF, cpxFn. simpl in lcv. split. exists Logic.I. unfold PartializeFunc, partialApply. apply CSUCTrapezePlateau. apply lcv. apply lcv. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets