proposition: Lemma DiscrDerivInfiniteSum : forall {R : ConstructiveReals} (X : Set) (fn : nat -> @PartialFunction R X), PartialRestriction (XinfiniteSumAbs (DiscrDeriv X fn)) (XpointwiseLimit fn).
proof: Proof. split. - intros x H. simpl. destruct H as [xn xcv]. exists (DiscrDerivDomainIncReverse X fn x xn). assert (CR_cauchy _ (CRsum (fun n : nat => CRabs _ (partialApply (DiscrDeriv X fn n) x (xn n))))). { intro p. specialize (xcv p) as [n nmaj]. exists n. simpl. exact nmaj. } clear xcv. apply series_cv_abs in H. destruct H as [l xcv]. apply (Rcv_cauchy_mod _ l). apply (CR_cv_eq _ (CRsum (fun n : nat => partialApply (DiscrDeriv X fn n) x (xn n)))). 2: exact xcv. intro n. apply DiscrDerivApply. - intros. apply applyInfiniteSumAbs. destruct xG as [xn xcv]. apply (CR_cv_eq _ (fun n : nat => partialApply (fn n) x (xn n))). intro n. symmetry. apply DiscrDerivApply. clear xD. simpl. destruct (CR_complete R (fun n : nat => partialApply (fn n) x (xn n)) xcv). exact c. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions