proposition: Lemma sqrt_uc_prf : @is_UniformlyContinuousFunction Q_as_MetricSpace CR rational_sqrt sqrt_modulus.
proof: Proof. intros e a. cut (forall a b, (0 <= a) -> (0 <= b) -> ball_ex (X:=Q_as_MetricSpace) (sqrt_modulus e) a b -> ball (m:=CR) (proj1_sig e) (rational_sqrt a) (rational_sqrt b)). intros X b Hab. destruct (Qle_total 0 a) as [Ha|Ha]. destruct (Qle_total 0 b) as [Hb|Hb]. apply X; assumption. unfold rational_sqrt at 2. destruct (Qlt_le_dec_fast 0 b) as [Z|_]. elim (Qle_not_lt _ _ Hb Z). change 0%CR with (rational_sqrt 0). apply X; try assumption. apply Qle_refl. destruct Hab. split; simpl in *. rewrite -> Qle_minus_iff in *. replace RHS with ((a + - 0) + proj1_sig (e*e)%Qpos) by simpl; ring. Qauto_nonneg. rewrite -> Qle_minus_iff in *. replace RHS with (proj1_sig (e*e)%Qpos + - (a - b) + (0 + - b)) by simpl; ring. Qauto_nonneg. unfold rational_sqrt at 1. destruct (Qlt_le_dec_fast 0 a) as [Z0|_]. elim (Qle_not_lt _ _ Ha Z0). change 0%CR with (rational_sqrt 0). destruct (Qle_total 0 b) as [Hb|Hb]. apply X; try assumption. apply Qle_refl. destruct Hab. split; simpl in *. rewrite -> Qle_minus_iff in *. replace RHS with ((a - b) + - - proj1_sig (e*e)%Qpos + (0 + - a)) by simpl; ring. Qauto_nonneg. rewrite -> Qle_minus_iff in *. replace RHS with (proj1_sig (e*e)%Qpos + (b + - 0)) by simpl; ring. Qauto_nonneg. unfold rational_sqrt at 2. destruct (Qlt_le_dec_fast 0 b) as [Z0|_]. elim (Qle_not_lt _ _ Hb Z0). change 0%CR with (rational_sqrt 0). apply ball_refl. apply Qpos_nonneg. clear a. intros a b Ha Hb Hab. assert (Z:[0][<=]inj_Q IR a). stepl (inj_Q IR 0); [| now apply (inj_Q_nring IR 0)]. apply inj_Q_leEq. assumption. rewrite -> (rational_sqrt_correct _ Z). assert (Z0:[0][<=]inj_Q IR b). stepl (inj_Q IR 0); [| now apply (inj_Q_nring IR 0)]. apply inj_Q_leEq. assumption. rewrite -> (rational_sqrt_correct _ Z0). rewrite <- CRAbsSmall_ball. cut (AbsSmall (R:=CRasCOrdField) (IRasCR (inj_Q IR (proj1_sig e)))%CR (IRasCR (sqrt (inj_Q IR a) Z[-](sqrt (inj_Q IR b) Z0)))). intros [A B]. unfold cg_minus. split; (simpl; rewrite <- (IR_inj_Q_as_CR (proj1_sig e)); rewrite <- (IR_opp_as_CR (sqrt _ Z0)); rewrite <- (IR_plus_as_CR); assumption). rewrite <- IR_AbsSmall_as_CR. assert (Z1:AbsSmall (inj_Q IR (proj1_sig e*proj1_sig e)) ((inj_Q IR a)[-](inj_Q IR b))). destruct Hab. split. stepl (inj_Q IR (-(proj1_sig e*proj1_sig e))); [| now apply (inj_Q_inv IR)]. stepr (inj_Q IR (a - b)); [| now apply (inj_Q_minus IR)]. apply inj_Q_leEq. assumption. stepl (inj_Q IR (a - b)); [| now apply (inj_Q_minus IR)]. apply inj_Q_leEq. assumption. clear Hab. set (e':=(inj_Q IR (proj1_sig e))). set (a':=(sqrt (inj_Q IR a) Z)). set (b':=(sqrt (inj_Q IR b) Z0)). assert (He:[0][<]e'). stepl (inj_Q IR 0); [| now apply (inj_Q_nring IR 0)]. apply inj_Q_less. simpl; auto with *. split. refine (mult_cancel_leEq _ _ _ (e'[+]a'[+]b') _ _). rstepl ([0][+][0][+][0]:IR). do 2 (apply plus_resp_less_leEq; try apply sqrt_nonneg). assumption. rstepl (([--](e'[*]e'))[+](e')[*]([--]a'[-]b')). rstepr ((a'[^]2[-]b'[^]2)[+](e')[*](a'[-]b')). apply plus_resp_leEq_both. stepr (inj_Q IR a[-]inj_Q IR b). stepl ([--](inj_Q IR (proj1_sig e*proj1_sig e))). destruct Z1; assumption. unfold e'. csetoid_rewrite_rev (inj_Q_mult IR (proj1_sig e) (proj1_sig e)). apply eq_reflexive. unfold a', b'. unfold cg_minus. csetoid_rewrite (sqrt_sqr (inj_Q IR a) Z). csetoid_rewrite (sqrt_sqr (inj_Q IR b) Z0). apply eq_reflexive. apply mult_resp_leEq_lft;[|apply less_leEq;assumption]. apply minus_resp_leEq. apply shift_leEq_rht. rstepr (Two[*]a'). apply mult_resp_nonneg. apply less_leEq; apply pos_two. apply sqrt_nonneg. refine (mult_cancel_leEq _ _ _ (e'[+]a'[+]b') _ _). rstepl ([0][+][0][+][0]:IR). do 2 (apply plus_resp_less_leEq; try apply sqrt_nonneg). assumption. rstepr (((e'[*]e'))[+](e')[*](a'[+]b')). rstepl ((a'[^]2[-]b'[^]2)[+](e')[*](a'[-]b')). apply plus_resp_leEq_both. stepl (inj_Q IR a[-]inj_Q IR b). stepr (inj_Q IR (proj1_sig e*proj1_sig e)). destruct Z1; assumption. unfold e'. csetoid_rewrite_rev (inj_Q_mult IR (proj1_sig e) (proj1_sig e)). apply eq_reflexive. unfold a', b'. unfold cg_minus. csetoid_rewrite (sqrt_sqr (inj_Q IR a) Z). csetoid_rewrite (sqrt_sqr (inj_Q IR b) Z0). apply eq_reflexive. apply mult_resp_leEq_lft;[|apply less_leEq;assumption]. unfold cg_minus. apply plus_resp_leEq_lft. apply shift_leEq_rht. rstepr (Two[*]b'). apply mult_resp_nonneg. apply less_leEq; apply pos_two. apply sqrt_nonneg. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.Q_in_CReals CoRN.reals.fast.CRpower CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.NRootIR CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.reals.fast.Compress Coq.NArith.Ndigits CoRN.reals.fast.PowerBound CoRN.transc.RealPowers CoRN.reals.fast.ContinuousCorrect CoRN.tactics.Qauto CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra