proposition: Lemma IntegralCSUC_ext : forall {R : ConstructiveReals} (g h : PartialFunction (CRcarrier R)) (gCS : Is_CSUC_func g) (hCS : Is_CSUC_func h), (forall x:CRcarrier R, TotalizeFunc (CRcarrier R) g (CSUC_fullDomain g gCS) x == TotalizeFunc (CRcarrier R) h (CSUC_fullDomain h hCS) x) -> IntegralCSUC g gCS == IntegralCSUC h hCS.
proof: Proof. intros. pose proof (CSUC_connect_support (TotalizeFunc (CRcarrier R) g (CSUC_fullDomain g gCS)) (CSUC_low g gCS) (CSUC_high g gCS) (CSUC_cont_mod g gCS)). pose proof (CSUC_connect_support (TotalizeFunc (CRcarrier R) h (CSUC_fullDomain h hCS)) (CSUC_low h hCS) (CSUC_high h hCS) (CSUC_cont_mod h hCS)). unfold IntegralCSUC; destruct gCS, hCS, g, h; simpl; simpl in H, H0, H1. unfold TotalizeFunc. assert (CRmin CSUC_low0 CSUC_low1 <= CRmax CSUC_high0 CSUC_high1). { apply (CRle_trans _ CSUC_low0). apply CRmin_l. apply (CRle_trans _ CSUC_high0). apply CSUC_lowHigh0. apply CRmax_l. } transitivity (UC_integral (fun x2 : CRcarrier R => partialApply x2 (CSUC_fullDomain0 x2)) (CRmin CSUC_low0 CSUC_low1) (CRmax CSUC_high0 CSUC_high1) CSUC_cont_mod0 (fst CSUC_adapt0) H2). - apply (UC_integral_extend_zero _ CSUC_cont_mod0). apply CRmin_l. apply CRmax_l. intros. apply H0. apply CSUC_adapt0. left. apply H3. intros. apply H0. apply CSUC_adapt0. right. apply H3. - transitivity (UC_integral (fun x2 : CRcarrier R => partialApply0 x2 (CSUC_fullDomain1 x2)) (CRmin CSUC_low0 CSUC_low1) (CRmax CSUC_high0 CSUC_high1) CSUC_cont_mod1 (fst CSUC_adapt1) H2). apply UC_integral_extens. intros. apply H. symmetry. apply (UC_integral_extend_zero _ CSUC_cont_mod1). apply CRmin_r. apply CRmax_r. intros. apply H1. apply CSUC_adapt1. left. apply H3. intros. apply H1. apply CSUC_adapt1. right. apply H3. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets