proposition: Lemma StepApproxBelow : 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), l < 1 -> 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 -> partialApply f x (fst (xnD O)) < t.
proof: Proof. intros. destruct (CR_cv_open_above _ _ _ H0 H) as [k kmaj]. specialize (kmaj k (Nat.le_refl k)). unfold StepApprox in kmaj. rewrite applyXscale in kmaj. apply (CRmult_lt_compat_l (t - t * CR_of_Q R (1 - (1 # Pos.of_nat (2 * S k))))) in kmaj. 2: apply CRlt_minus, StepApproxBetween, tPos. destruct (xnD k) as [d d0]. assert (partialApply (XminConst f t) x d < t) as H1. { apply (CRplus_lt_reg_r (- partialApply (XminConst f (t * CR_of_Q R (1 - (1 # Pos.of_nat (2 * S k))))) x d0)). apply (CRle_lt_trans (partialApply (XminConst f t) x d + - partialApply (XminConst f (t * CR_of_Q R (1 - (1 # Pos.of_nat (2 * S k))))) x d0 )) in kmaj. apply (CRlt_le_trans _ _ _ kmaj). rewrite CRmult_1_r. apply CRplus_le_compat_l, CRopp_ge_le_contravar. apply CRmin_r. rewrite <- CRmult_assoc, CRinv_r, CRmult_1_l. rewrite (applyXminus (XminConst f t) (XminConst f (t * CR_of_Q R (1 - (1 # Pos.of_nat (2 * S k)))))). apply CRle_refl. } clear kmaj. apply (CRle_lt_trans _ (partialApply (XminConst f t) x d)). 2: exact H1. apply CRmin_lt_r in H1. rewrite H1. rewrite (DomainProp f x _ d). apply CRle_refl. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia