proposition: Lemma CSUCextendSupport : forall {R : ConstructiveReals} (f : PartialFunction (CRcarrier R)) (fL : Is_CSUC_func f) (a b : CRcarrier R) (aBelow : a <= CSUC_low f fL) (bAbove : CSUC_high f fL <= b) (leab : a <= b), IntegralCSUC f fL == UC_integral (TotalizeFunc (CRcarrier R) f (CSUC_fullDomain f fL)) a b (CSUC_cont_mod f fL) (fst (CSUCextendAdapt f fL a b aBelow bAbove)) leab.
proof: Proof. intros. assert (CSUC_low f fL <= b). { apply (CRle_trans _ (CSUC_high f fL)). apply CSUC_lowHigh. apply bAbove. } rewrite (UC_integral_chasles a (CSUC_low f fL) b _ _ _ aBelow H). rewrite (UC_integral_chasles (CSUC_low f fL) (CSUC_high f fL) b _ _ _ (CSUC_lowHigh f fL) bAbove). rewrite (UC_integral_zero _ a (CSUC_low f fL)). rewrite (UC_integral_zero _ (CSUC_high f fL) b). rewrite CRplus_0_l, CRplus_0_r. apply (UC_integral_extens (TotalizeFunc (CRcarrier R) f (CSUC_fullDomain f fL)) (TotalizeFunc (CRcarrier R) f (CSUC_fullDomain f fL)) (CSUC_low f fL) (CSUC_high f fL)). - intros. reflexivity. - intros. apply (CSUC_connect_support _ (CSUC_low f fL) (CSUC_high f fL) (CSUC_cont_mod f fL)). apply fL. right. apply H0. - intros. apply (CSUC_connect_support _ (CSUC_low f fL) (CSUC_high f fL) (CSUC_cont_mod f fL)). apply fL. left. apply H0. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets