proposition: Lemma applyInfiniteSumAbsDiag : forall {R : ConstructiveReals } (X : Set) (fnk : nat -> nat -> @PartialFunction R X) (x : X) (xD : Domain (XinfiniteSumAbs (diagSeq fnk)) x), series_cv (fun n:nat => let (ln,a) := domainInfiniteSumAbsDiag X fnk n x xD in let (lim,_) := CR_complete R _ a in lim) (let (xn,a) := xD in let (lim,_) := CR_complete R _ a in lim).
proof: Proof. intros. destruct (DiagSeqInfiniteSum (fun n k => CRabs _ (partialApply (fnk n k) x (domainInfiniteSumAbsIncReverse _ x (domainInfiniteSumAbsDiag X fnk n x xD) k))) (fun n : nat => let (ln, a) := domainInfiniteSumAbsDiag X fnk n x xD in let (lim, _) := CR_complete R (CRsum (fun n0 : nat => CRabs _ (partialApply (fnk n n0) x (ln n0)))) a in lim) (let (xn,a) := xD in let (lim,_) := CR_complete R _ a in lim)). - apply (series_cv_eq (diagSeq (fun n k : nat => CRabs _ (partialApply (fnk n k) x (domainInfiniteSumAbsIncReverse (fnk n) x (domainInfiniteSumAbsDiag X fnk n x xD) k))))). intro n. unfold diagSeq. destruct (diagPlaneInv n). symmetry. rewrite CRabs_right. reflexivity. apply CRabs_pos. apply InfiniteDiagApply. - intro n. destruct (domainInfiniteSumAbsDiag X fnk n); simpl. destruct (CR_complete R (CRsum (fun k : nat => CRabs _ (partialApply (fnk n k) x (x0 k)))) c). exact c0. - destruct p, p. apply (CR_cv_proper _ _ _ s). symmetry. apply (series_cv_unique _ _ _ (InfiniteDiagApply _ _ x xD) s0). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions