proposition: Lemma applyTelescopicOp : 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) (n : nat) (x : X) (pF : forall n:nat, Domain (fn n) x) (pXT : forall n:nat, Domain (telescopicOp X fn op opEq n) x), partialApply (telescopicOp X fn op opEq (S n)) x (pXT (S n)) == op (CRsum (fun n=> partialApply (fn n) x (pF n)) (S n)) - op (CRsum (fun n=> partialApply (fn n) x (pF n)) n).
proof: Proof. intros. unfold telescopicOp. destruct (pXT (S n)). rewrite (applyXminus (Xop X (Xsum fn (S n)) op opEq) (Xop X (Xsum fn n) op opEq)). destruct d; simpl. apply CRplus_morph. apply opEq. rewrite (applyXsum fn n x _ pF). rewrite (DomainProp _ x (pF (S n)) d1). reflexivity. apply CRopp_morph, opEq. rewrite (applyXsum fn n x _ pF). reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase