proposition: Lemma StepApproxAbove : forall {R : ConstructiveReals} {X : Set} (f : PartialFunction X) (t : CRcarrier R) (tPos : 0 < t) (x : X) (xnD : nat -> Domain f x * Domain f x) (l : CRcarrier R), 0 < l -> CR_cv R (fun n : nat => partialApply (StepApprox f (t * CR_of_Q R (1 - (1 # Pos.of_nat (2 * S n)))) t (snd (StepApproxBetween t tPos n))) x (xnD n)) l -> t <= partialApply f x (fst (xnD O)).
proof: Proof. intros. intro abs. destruct (CR_cv_open_below _ _ _ (StepApproxCv t) abs) as [n nmaj]. assert (CR_cv R (fun n : nat => partialApply (StepApprox f (t * CR_of_Q R (1 - (1 # Pos.of_nat (2 * S n)))) t (snd (StepApproxBetween t tPos n))) x (xnD n)) 0). intro p. exists n. intros. unfold StepApprox. rewrite applyXscale. setoid_replace (partialApply (Xminus (XminConst f t) (XminConst f (t * CR_of_Q R (1 - (1 # Pos.of_nat (2 * S i)))))) x (xnD i)) with (CR_of_Q R 0). rewrite CRmult_0_r. unfold CRminus. rewrite CRplus_opp_r, CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. destruct (xnD i). rewrite (applyXminus (XminConst f t) (XminConst f (t * CR_of_Q R (1 - (1 # Pos.of_nat (2 * S i))))) x). rewrite applyXminConst, applyXminConst. rewrite CRmin_left, CRmin_left. unfold CRminus. rewrite (DomainProp f x d d0), CRplus_opp_r. reflexivity. specialize (nmaj i H1). rewrite (DomainProp f x d0 (fst (xnD 0%nat))). apply CRlt_asym, nmaj. specialize (nmaj i H1). rewrite (DomainProp f x d (fst (xnD 0%nat))). apply CRlt_asym, (CRlt_trans _ _ _ nmaj). apply StepApproxBetween, tPos. rewrite <- (CR_cv_unique _ _ _ H1 H0) in H. exact (CRlt_asym 0 0 H H). Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia