proposition: Lemma applyTelescopicOpMaj : 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))) (zeroFix : op 0 == 0) (n : nat) (x : X) (pF : Domain (fn n) x) (pXT : Domain (telescopicOp X fn op opEq n) x), CRabs _ (partialApply (telescopicOp X fn op opEq n) x pXT) <= CRabs _ (partialApply (fn n) x pF).
proof: Proof. intros. unfold telescopicOp. unfold telescopicOp in pXT. destruct n. - destruct (fn O); simpl. rewrite <- (CRplus_0_r (partialApply x pF)). rewrite <- CRopp_0. rewrite <- (DomainProp x pXT pF). setoid_replace (op (partialApply x pXT)) with (op (partialApply x pXT) - op 0). apply contract. rewrite zeroFix. unfold CRminus. rewrite CRopp_0, CRplus_0_r. reflexivity. - simpl in pXT. destruct pXT. rewrite (applyXminus (Xop X (Xsum fn (S n)) op opEq) (Xop X (Xsum fn n) op opEq)). simpl. apply (CRle_trans _ _ _ (contract _ _)). destruct p. simpl. destruct (Xsum fn n), (fn (S n)); simpl. rewrite (DomainProp x d0 d), (DomainProp0 x pF d1). apply (CRle_trans _ (CRabs _ ((partialApply x d + partialApply0 x d1) - partialApply x d))). apply CRle_refl. rewrite CRplus_comm. unfold CRminus. rewrite CRplus_assoc. rewrite CRplus_opp_r. rewrite CRplus_0_r. apply CRle_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase