proposition: Lemma partialApplyWeaveInfiniteSum : forall {R : ConstructiveReals} (X : Set) (fn gn : nat -> @PartialFunction R X) (x : X) (xD : Domain (XinfiniteSumAbs fn) x) (y : Domain (XinfiniteSumAbs gn) x) (pxDn : forall n:nat, Domain (weaveSequences (PartialFunction X) fn gn n) x), series_cv (fun n : nat => partialApply (weaveSequences (PartialFunction X) fn gn n) x (pxDn n)) (partialApply (XinfiniteSumAbs fn) x xD + partialApply (XinfiniteSumAbs gn) x y).
proof: Proof. intros. apply (series_cv_eq (weaveSequences (CRcarrier R) (fun n => partialApply (fn n) x (domainInfiniteSumAbsIncReverse _ x xD n)) (fun n => partialApply (gn n) x (domainInfiniteSumAbsIncReverse _ x y n)))). intro n. destruct (Nat.even n) eqn:nEven. - pose proof (Nat.even_spec n) as [H2 _]. destruct (H2 nEven) as [m H3]. subst n. rewrite Nat.mul_comm. rewrite <- (partialApplyWeaveEven X fn gn m x (domainInfiniteSumAbsIncReverse _ x xD m)). + rewrite weaveSequencesEven. reflexivity. - pose proof (Nat.odd_spec n) as [H2 _]. destruct H2 as [m H3]. unfold Nat.odd. rewrite nEven. trivial. subst n. rewrite Nat.add_comm. rewrite Nat.mul_comm. rewrite <- (partialApplyWeaveOdd X fn gn m x (domainInfiniteSumAbsIncReverse _ x y m)). + rewrite weaveSequencesOdd. reflexivity. - apply weaveInfiniteSums. apply applyInfiniteSumAbs. reflexivity. apply applyInfiniteSumAbs. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase