proposition: Lemma CompleteRepresentationDoubleSum : forall (IS : IntegrationSpace) (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnInt : forall n:nat, IntegrableFunction (fn n)), let (intRepresN, _) := CompleteRepresentation IS fn fnInt in forall (x : X (ElemFunc IS)) (xD : Domain (XinfiniteSumAbs (diagSeq (fun n k : nat => IntFn (intRepresN n) k))) x) (pxF : forall n : nat, Domain (fn n) x), series_cv (fun n : nat => partialApply (fn n) x (pxF n)) (partialApply (XinfiniteSumAbs (diagSeq (fun n k : nat => IntFn (intRepresN n) k))) x xD).
proof: Proof. intros. destruct (CompleteRepresentation IS fn fnInt) as [cfnInt represN]. intros. destruct (DiagSeqInfiniteSum (fun n k => partialApply _ _ (domainInfiniteSumAbsIncReverse _ x (domainInfiniteSumAbsDiag _ _ n x xD) k)) (fun n : nat => partialApply (fn n) x (pxF n)) (let (xn,a) := xD in let (l,_) := CR_complete _ _ a in l)). - apply InfiniteDiagApply. - intro n. apply represApply. apply represN. - setoid_replace (partialApply (XinfiniteSumAbs (diagSeq (fun n k : nat => IntFn (cfnInt n) k))) x xD) with x0. apply p. destruct p,p. apply (series_cv_unique (diagSeq (fun n k : nat => partialApply (IntFn (cfnInt n) k) x (domainInfiniteSumAbsIncReverse (fun k0 : nat => IntFn (cfnInt n) k0) x (domainInfiniteSumAbsDiag (X (ElemFunc IS)) (fun n0 k0 : nat => IntFn (cfnInt n0) k0) n x xD) k)))). 2: exact s0. apply (series_cv_eq (fun k : nat => partialApply (diagSeq (fun n k0 : nat => IntFn (cfnInt n) k0) k) x (let (xn,_) := xD in xn k))). + intro n. transitivity (let (n0,k) := diagPlaneInv n in partialApply (IntFn (cfnInt n0) k) x (domainInfiniteSumAbsIncReverse (fun k0 : nat => IntFn (cfnInt n0) k0) x (domainInfiniteSumAbsDiag (X (ElemFunc IS)) (fun n1 k0 : nat => IntFn (cfnInt n1) k0) n0 x xD) k)). 2: reflexivity. destruct (diagPlaneInv n) eqn:desN. apply partialApplyEq. unfold diagSeq. rewrite desN. reflexivity. + destruct xD as [xn cv]; simpl. apply series_cv_abs_cv. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions