proposition: Lemma IntegrableXpointwiseLimit : forall {IS : IntegrationSpace} (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnInt : forall n:nat, IntegrableFunction (fn n)) (sumAbsInt : CRcarrier (RealT (ElemFunc IS))), series_cv (fun n:nat => Integral (IntegrableAbs (IntegrableMinus (fnInt (S n)) (fnInt n)))) sumAbsInt -> { i : IntegrableFunction (XpointwiseLimit fn) & CR_cv _ (fun n => Integral (fnInt n)) (Integral i) }.
proof: Proof. intros. destruct (IntegrableFunctionsComplete IS _ (IntegrableDiscrDeriv IS fn fnInt) (sumAbsInt + Integral (IntegrableAbs (IntegrableDiscrDeriv IS fn fnInt O)))) as [rep repcv]. - apply (series_cv_shift (fun k : nat => Integral (IntegrableAbs (IntegrableDiscrDeriv IS fn fnInt k))) O sumAbsInt). simpl. apply (series_cv_eq (fun n : nat => Integral (IntegrableAbs (IntegrableMinus (fnInt (S n)) (fnInt n))))). 2: exact H. intro n. apply IntegralExtensional. intros. apply DomainProp. - destruct repcv. assert (PartialRestriction (XinfiniteSumAbs (IntFn rep)) (XpointwiseLimit fn)) as res. { apply (PartialRestriction_trans _ _ _ _ p). apply DiscrDerivInfiniteSum. } exists (IntegrableFunctionExtensional _ _ res (existT _ rep (PartialRestriction_refl _ _))). apply (CR_cv_eq (fun n : nat => Integral (fnInt n))) in s. + apply (CR_cv_proper _ _ _ s). clear s. rewrite IntegralRestrict. reflexivity. + induction n. apply IntegralExtensional. intros. apply DomainProp. simpl. rewrite IHn. clear IHn. rewrite <- (CRplus_0_l (Integral (fnInt (S n)))). rewrite <- (CRplus_opp_r (Integral (fnInt n))), CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRplus_comm. pose proof (IntegralMinus (fn (S n))). unfold CRminus in H0. rewrite <- H0. clear H0. apply IntegralExtensional. intros. apply DomainProp. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions