proposition: Lemma IcontinuousWeave : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fn : nat -> PartialFunction (X (ElemFunc IS))) (gn : nat -> PartialFunction (X (ElemFunc IS))) (fL : (L (ElemFunc IS)) f) (fnL : forall n:nat, (L (ElemFunc IS)) (fn n)) (gnL : forall n:nat, (L (ElemFunc IS)) (gn n)), (forall n:nat, nonNegFunc (fn n)) -> (forall n:nat, nonNegFunc (gn n)) -> series_cv_two_lim_lt (fun n => I IS (fn n) (fnL n)) (fun n => I IS (gn n) (gnL n)) (I IS f fL) -> { x : @CommonPointFunTwoSeq _ _ f fn gn & series_cv_two_lim_lt (fun n => partialApply (fn n) _ (cpxFn2 x n)) (fun n => partialApply (gn n) _ (cpxGn2 x n)) (partialApply f _ (cpxF2 x)) }.
proof: Proof. intros. assert (forall n:nat, L (ElemFunc IS) (weaveSequences _ fn gn n)) as wL. { apply weaveSequencesL; assumption. } destruct (Icontinuous IS f (weaveSequences _ fn gn) fL wL). - intro n. unfold weaveSequences. destruct (Nat.even n). apply H. apply H0. - destruct H1, x. simpl in p. destruct p, p. exists (c+c0). split. 2: exact c1. apply (series_cv_eq (weaveSequences _ (fun n => I IS (fn n) (fnL n)) (fun n => I IS (gn n) (gnL n)))). intro n. unfold weaveSequences. generalize (wL n). intros. unfold weaveSequences in l. destruct (Nat.even n). apply IExtensional. intros. apply DomainProp. apply IExtensional. intros. apply DomainProp. apply weaveInfiniteSums; assumption. - destruct x; simpl in s. destruct s, p. assert (forall k:nat, Domain (fn k) cpx) as cpxDf. { intro k. exact (domainWeaveEvenInc _ _ _ k cpx (cpxFn (k*2)%nat)). } assert (forall k:nat, Domain (gn k) cpx) as cpxDg. { intro k. exact (domainWeaveOddInc _ _ _ k cpx (cpxFn (1+k*2)%nat)). } apply (series_cv_eq _ (weaveSequences _ (fun n => partialApply _ cpx (cpxDf n)) (fun n => partialApply _ cpx (cpxDg n)))) in s. assert ({ l : CRcarrier _ & series_cv (fun n => partialApply _ cpx (cpxDg n)) l}). { apply (halfWeavedSumOdd (fun n => partialApply _ cpx (cpxDf n)) _ x). intro k. apply H. intro k. apply H0. exact s. } destruct H2. assert ({ l : CRcarrier _ & series_cv (fun k => partialApply _ cpx (cpxDf k)) l}). { apply (halfWeavedSumEven _ (fun k => partialApply _ cpx (cpxDg k)) x). intro k. apply H. intro k. apply H0. exact s. } destruct H2. exists (Build_CommonPointFunTwoSeq _ _ _ _ _ cpx cpxF cpxDf cpxDg). simpl. exists (x1,x0). split. split. exact s1. exact s0. simpl. setoid_replace (x1+x0) with x. exact c. apply (series_cv_unique (weaveSequences _ (fun n : nat => partialApply (fn n) cpx (cpxDf n)) (fun n : nat => partialApply (gn n) cpx (cpxDg n)))). 2: exact s. apply weaveInfiniteSums; assumption. intro k. rewrite (partialApplyWeave _ fn gn k cpx (cpxDf (k/2)%nat) (cpxDg (k/2)%nat) (cpxFn k)). unfold weaveSequences. destruct (Nat.even k); reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions