proposition: Lemma CSUC_extend_pos : forall {R : ConstructiveReals} (f : PartialFunction (CRcarrier R)) (fL : Is_CSUC_func f) (a b : CRcarrier R) (leab : a <= b), nonNegFunc f -> UC_integral (TotalizeFunc (CRcarrier R) f (CSUC_fullDomain f fL)) a b (CSUC_cont_mod f fL) (fst (CSUC_adapt f fL)) leab <= IntegralCSUC f fL.
proof: Proof. intros. unfold IntegralCSUC, TotalizeFunc. pose proof (CSUC_connect_support (TotalizeFunc (CRcarrier R) f (CSUC_fullDomain f fL)) (CSUC_low f fL) (CSUC_high f fL) (CSUC_cont_mod f fL)). destruct fL, f; simpl; simpl in H0. assert (CRmin a CSUC_low0 <= CRmax b CSUC_high0). { apply (CRle_trans _ a). apply CRmin_l. apply (CRle_trans _ b _ leab). apply CRmax_l. } apply (CRle_trans _ (UC_integral (fun x1 : CRcarrier R => partialApply x1 (CSUC_fullDomain0 x1)) (CRmin a CSUC_low0) (CRmax b CSUC_high0) CSUC_cont_mod0 (fst CSUC_adapt0) H1)). apply (UC_integral_extend_nonneg _ CSUC_cont_mod0). apply CRmin_l. apply CRmax_l. intros. apply H. assert (forall x y:CRcarrier R, x == y -> x <= y). { intros. rewrite H2. apply CRle_refl. } apply H2. symmetry. apply (UC_integral_extend_zero _ CSUC_cont_mod0). apply CRmin_r. apply CRmax_r. intros. apply H0. apply CSUC_adapt0. left. apply H3. intros. apply H0. apply CSUC_adapt0. right. apply H3. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets