proposition: Lemma CSUCIntegralAdditive : forall {R : ConstructiveReals} (f g : PartialFunction (CRcarrier R)) (fL : Is_CSUC_func f) (gL : Is_CSUC_func g), IntegralCSUC (Xplus f g) (CSUC_func_plus_stable f g fL gL) == IntegralCSUC f fL + IntegralCSUC g gL.
proof: Proof. intros. pose (CRmin (CSUC_low f fL) (CSUC_low g gL)) as c. pose (CRmax (CSUC_high f fL) (CSUC_high g gL)) as d. assert (c <= d). { apply (CRle_trans _ (CSUC_low f fL)). apply CRmin_l. apply (CRle_trans _ (CSUC_high f fL)). apply (CSUC_lowHigh f fL). apply CRmax_l. } rewrite (CSUCextendSupport f fL c d (CRmin_l _ _) (CRmax_l _ _) H). rewrite (CSUCextendSupport g gL c d (CRmin_r _ _) (CRmax_r _ _) H). transitivity (UC_integral (fun x => TotalizeFunc (CRcarrier R) f (CSUC_fullDomain f fL) x + TotalizeFunc (CRcarrier R) g (CSUC_fullDomain g gL) x) (CSUC_low (Xplus f g) (CSUC_func_plus_stable f g fL gL)) (CSUC_high (Xplus f g) (CSUC_func_plus_stable f g fL gL)) _ (UC_plus _ _ _ _ (fst (CSUC_adapt f fL)) (fst (CSUC_adapt g gL))) (CSUC_lowHigh (Xplus f g) (CSUC_func_plus_stable f g fL gL))). unfold IntegralCSUC. apply (UC_integral_extens (TotalizeFunc (CRcarrier R) (Xplus f g) (CSUC_fullDomain (Xplus f g) (CSUC_func_plus_stable f g fL gL))) (fun x : CRcarrier R => TotalizeFunc (CRcarrier R) f (CSUC_fullDomain f fL) x + TotalizeFunc (CRcarrier R) g (CSUC_fullDomain g gL) x)). - intros. destruct f,g,fL,gL; reflexivity. - destruct f,g,fL,gL; apply UC_integral_plus. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets