proposition: Lemma ContinuousCorrect : forall (x:IR) Hx, I x -> (IRasCR (f x Hx) == g (IRasCR x))%CR.
proof: Proof. intros x Hx H. set (J:=compact_in_interval I HI x H). apply ball_eq. intros e epos. assert (HJ:compact_ J) by apply compact_compact_in_interval. destruct Hf as [Hf1 Hf0]. clear Hf. assert (X:Continuous_I (Lend_leEq_Rend J HJ) f). apply Hf0. eapply included_trans;[|apply included_compact_in_interval]. unfold J; apply iprop_compact_in_interval_inc1. clear Hf0. destruct X as [_ X]. assert (He : [0][<](inj_Q IR (proj1_sig ((1#2)*exist _ _ epos)%Qpos))). stepl (inj_Q IR (nring 0)); [| now apply (inj_Q_nring IR 0)]. apply inj_Q_less. apply Qpos_ispos. destruct (X _ He) as [d0 Hd0 Hf]. clear X. set (d1:=mu g ((1#2)*exist _ _ epos)). set (Hab := (Lend_leEq_Rend J HJ)) in *. set (a:= (@Lend J HJ)) in *. set (b:= (@Rend J HJ)) in *. assert (HJ':included (Compact Hab) I). eapply included_trans. unfold Hab, a, b, J; apply iprop_compact_in_interval_inc1. apply included_compact_in_interval. assert (Hab0: a[<]b). apply proper_compact_in_interval'. assert (HJx:(Compact Hab) x). apply iprop_compact_in_interval'. clearbody Hab a b. clear J HJ. pose (d:=match d1 with | Qpos2QposInf q => Min (inj_Q IR (proj1_sig q)) d0 | QposInfinity => d0 end). assert (H0d : [0][<]d). destruct d1; try assumption. apply less_Min; try assumption. stepl (inj_Q IR [0]). apply inj_Q_less. apply Qpos_ispos. apply (inj_Q_nring IR 0). destruct (Q_dense_in_compact Hab0 HJx _ H0d) as [q Hq0 Hq1]. setoid_replace e with (proj1_sig ((1#2)*exist _ _ epos+(1#2)*exist _ _ epos))%Qpos by (simpl; ring). assert (Hfq : Dom f (inj_Q IR q)). apply Hf1. apply HJ'. assumption. apply ball_triangle with (IRasCR (f (inj_Q IR q) Hfq)). rewrite <- CRAbsSmall_ball. stepr (IRasCR (f x Hx[-]f (inj_Q IR q) Hfq)); [| now (simpl; apply IR_minus_as_CR)]. stepl (IRasCR (inj_Q IR (proj1_sig ((1 # 2) * exist _ _ epos)%Qpos))); [| now (simpl; apply IR_inj_Q_as_CR)]. rewrite <- IR_AbsSmall_as_CR. apply AbsIR_imp_AbsSmall. apply Hf; try assumption. eapply leEq_transitive. apply AbsSmall_imp_AbsIR. apply Hq1. destruct d1. apply Min_leEq_rht. apply leEq_reflexive. rewrite <- Hg;[|apply HJ';assumption]. apply uc_prf. fold d1. destruct d1; try constructor. simpl. rewrite <- IR_inj_Q_as_CR. rewrite <- CRAbsSmall_ball. stepr (IRasCR (inj_Q IR q[-]x)); [| now (simpl; apply IR_minus_as_CR)]. stepl (IRasCR (inj_Q IR (proj1_sig q0))); [| now (simpl; apply IR_inj_Q_as_CR)]. rewrite <- IR_AbsSmall_as_CR. apply AbsSmall_minus. eapply AbsSmall_leEq_trans;[|apply Hq1]. apply Min_leEq_lft. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.Q_in_CReals CoRN.ftc.MoreIntervals CoRN.reals.fast.CRIR CoRN.tactics.CornTac CoRN.model.metric2.Qmetric CoRN.model.totalorder.QposMinMax