proposition: Lemma InfiniteDiagApply : forall {R : ConstructiveReals } (X : Set) (fnk : nat -> nat -> @PartialFunction R X) (x : X) (xD : Domain (XinfiniteSumAbs (diagSeq fnk)) x), series_cv (diagSeq (fun n k : nat => CRabs _ (partialApply (fnk n k) x (domainInfiniteSumAbsIncReverse (fnk n) x (domainInfiniteSumAbsDiag X fnk n x xD) k)))) (let (xn,a) := xD in let (lim,_) := CR_complete R _ a in lim).
proof: Proof. intros. destruct xD as [xn cv]. destruct (CR_complete R (CRsum (fun k : nat => CRabs _ (partialApply (diagSeq fnk k) x (xn k)))) cv). apply (series_cv_eq (fun k : nat => CRabs _ (partialApply (diagSeq fnk k) x (xn k)))). 2: apply c. intro n. transitivity (let (n0,k) := diagPlaneInv n in CRabs _ (partialApply (diagSeq fnk (diagPlane n0 k)) x (xn (diagPlane n0 k)))). - destruct (diagPlaneInv n) eqn:desN. apply CRabs_morph. apply partialApplyEq. unfold diagSeq. rewrite diagPlaneInject. rewrite desN. reflexivity. - assert (forall unk vnk : nat -> nat -> CRcarrier R, (forall n k : nat, unk n k == vnk n k) -> forall n:nat, diagSeq unk n == diagSeq vnk n). { intros. unfold diagSeq. destruct (diagPlaneInv n0). apply H. } apply H. clear n. intros. apply CRabs_morph. apply partialApplyEq. unfold diagSeq. rewrite diagPlaneInject. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions