proposition: Lemma IntegralCSUC_bounded : forall {R : ConstructiveReals} (g : PartialFunction (CRcarrier R)) (gCS : Is_CSUC_func g) (A : CRcarrier R), (forall x:CRcarrier R, TotalizeFunc (CRcarrier R) g (CSUC_fullDomain g gCS) x <= A) -> IntegralCSUC g gCS <= (A* (CSUC_high g gCS - CSUC_low g gCS)).
proof: Proof. intros. rewrite CRmult_comm. unfold Qminus. rewrite <- (UC_integral_constant _ _ _ A _ (UC_constant A) (CSUC_lowHigh g gCS)). unfold IntegralCSUC. apply (UC_integral_nonneg (TotalizeFunc (CRcarrier R) g (CSUC_fullDomain g gCS)) (fun _ => A)). intros. apply H. intros. reflexivity. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets