proposition: Lemma applyTelescopicOpInfSum : forall {R : ConstructiveReals} (X : Set) (fn : nat -> PartialFunction X) (op : CRcarrier R -> CRcarrier R) (opEq : forall x y : CRcarrier R, x == y -> op x == op y) (contract : forall x y : CRcarrier R, CRabs _ (op x - op y) <= CRabs _ (x - y)) (x : X) (pF : forall n:nat, Domain (fn n) x) (pXT : forall n:nat, Domain (telescopicOp X fn op opEq n) x) (s : CRcarrier R), series_cv (fun n : nat => partialApply (fn n) x (pF n)) s -> series_cv (fun n : nat => partialApply (telescopicOp X fn op opEq n) x (pXT n)) (op s).
proof: Proof. intros. intros p. specialize (H p) as [N H0]. exists N. intros n H. specialize (H0 n H). assert (forall (p:nat) (u : nat -> CRcarrier R), CRsum u (S p) == CRsum u p + u (S p)) as sum_shift. { intros. reflexivity. } assert (forall p0:nat, CRsum (fun k : nat => partialApply (telescopicOp X fn op opEq k) x (pXT k)) p0 == op (CRsum (fun k : nat => partialApply (fn k) x (pF k)) p0)). { induction p0. - simpl. apply opEq. apply DomainProp. - rewrite sum_shift. rewrite IHp0. rewrite (applyTelescopicOp X fn op opEq p0 x pF). unfold CRminus. rewrite CRplus_comm, CRplus_assoc, CRplus_opp_l. rewrite CRplus_0_r. reflexivity. } rewrite H1. apply (CRle_trans _ (CRabs _ (CRsum (fun n : nat => partialApply (fn n) x (pF n)) n - s))). apply contract. assumption. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase