proposition: Lemma CompleteRepresentationRestrict : forall (IS : IntegrationSpace) (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnInt : forall n:nat, IntegrableFunction (fn n)), let (intRepresN, _) := CompleteRepresentation IS fn fnInt in PartialRestriction (XinfiniteSumAbs (diagSeq (fun n k => IntFn (intRepresN n) k))) (XinfiniteSumAbs fn).
proof: Proof. intros. pose proof (CompleteRepresentationDoubleSum IS fn fnInt) as dsum. destruct (CompleteRepresentation IS fn fnInt) as [intRepresN restrN]. split. intros x xdf. pose (domainInfiniteSumAbsDiag _ (fun n k => IntFn (intRepresN n) k)) as lineInj. destruct (series_cv_maj (fun n : nat => CRabs _ (partialApply (XinfiniteSumAbs (fun k : nat => IntFn (intRepresN n) k)) x (lineInj n x xdf))) (fun n => let (_,a) := lineInj n x xdf in let (l,_) := CR_complete _ _ a in l) (let (_,a) := xdf in let (l,_) := CR_complete _ _ a in l)). - intro n. simpl. rewrite CRabs_right. apply partialInfiniteTriangle. apply CRabs_pos. - apply applyInfiniteSumAbsDiag. - destruct p. apply (domainInfiniteSumAbsInc fn x (fun n:nat => fst (fst (restrN n)) x (lineInj n x xdf)) x0). + apply (series_cv_eq (fun n : nat => CRabs _ (partialApply (XinfiniteSumAbs (fun k : nat => IntFn (intRepresN n) k)) x (lineInj n x xdf)))). 2: exact s. intro n. destruct (restrN n) as [[j a0] maj]. unfold fst. specialize (a0 x (lineInj n x xdf)). apply CRabs_morph. apply a0. - intros. symmetry. apply applyInfiniteSumAbs. apply dsum. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions