proposition: Lemma LocalizeIntegralSeries : forall (x y z t : CRcarrier R) (infint : CRcarrier R) (lexy : x <= y) (lezt : z <= t), x <= z -> t <= y -> series_cv (fun k : nat => UC_integral (fn k) x y (fnMod k) (fnCont k) lexy) infint -> { sLoc : CRcarrier R & series_cv (fun k : nat => UC_integral (fn k) z t (fnMod k) (fnCont k) lezt) sLoc }.
proof: Proof. intros. destruct (series_cv_maj (fun k : nat => UC_integral (fn k) z t (fnMod k) (fnCont k) lezt) (fun k : nat => UC_integral (fn k) x0 y0 (fnMod k) (fnCont k) lexy0) infint). - intros. rewrite CRabs_right. apply (UC_integral_extend_nonneg (fn n) (fnMod n)). exact H. exact H0. apply fnPos. apply UC_integral_pos. intros. apply fnPos. - exact H1. - exists x1. apply p. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets