proposition: Lemma is_UniformlyContinuousD_Q : forall g : Q_as_MetricSpace -> Q, (forall (q : Q) (Hq : Dom f (inj_Q IR q)), I (inj_Q IR q) -> (inj_Q IR (g q) [=] (f (inj_Q IR q) Hq))) -> forall c : Q, (forall (x : Q) (Hx : Dom f' (inj_Q IR x)), I (inj_Q IR x) -> AbsIR (f' (inj_Q IR x) Hx)[<=]inj_Q IR (c:Q)) -> @is_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace (fun x : Q_as_MetricSpace => g (clamp x)) (Qscale_modulus c).
proof: Proof. intros g Hg c Hc. intros e a b Hab. rewrite <- ball_Cunit. generalize e a b Hab; clear e a b Hab. change (is_UniformlyContinuousFunction (fun x : Q_as_MetricSpace => ((fun y => '(g y)) (clamp x)))%CR (Qscale_modulus c)). apply is_UniformlyContinuousD. intros q Hq H. rewrite <- IR_inj_Q_as_CR. apply IRasCR_wd. apply Hg. assumption. intros x Hx HI. rstepr ([0][+]inj_Q IR c). apply shift_leEq_plus. apply approach_zero_weak. intros e He. assert (X:Derivative_I (proper_compact_in_interval' I properI x HI (compact_compact_in_interval I properI x HI)) f f'). apply (included_imp_Derivative) with I properI; try assumption. eapply included_trans. apply iprop_compact_in_interval_inc1. apply included_compact_in_interval. set (LI' := (Lend (compact_compact_in_interval I properI x HI))). set (RI' := (Rend (compact_compact_in_interval I properI x HI))). set (I':=(less_leEq IR LI' RI' (proper_compact_in_interval' I properI x HI (compact_compact_in_interval I properI x HI)))). assert (X':Continuous_I I' (FAbs f')). apply Continuous_I_abs. apply (deriv_imp_contin'_I _ _ _ _ _ (less_leEq _ _ _ (proper_compact_in_interval' I properI x HI (compact_compact_in_interval I properI x HI))) X). clear X. destruct (contin_prop _ _ _ _ X' _ (pos_div_two _ _ He)) as [d Hd Hd0]. destruct (iprop_compact_in_interval' _ properI x HI _ I') as [c0 c1]. assert (Z:~((LI'[<]x or x[<]RI')->False)). intro H. fold LI' in c0. fold RI' in c1. apply (leEq_less_or_equal _ _ _ c0). intros [H0|H0];[tauto|]. apply (leEq_less_or_equal _ _ _ c1). intros [H1|H1];[tauto|]. generalize (proper_compact_in_interval' I properI x HI (compact_compact_in_interval I properI x HI)). change (Not (LI'[<]RI')). rewrite <- leEq_def. rewrite -> H0, <- H1. apply leEq_reflexive. rewrite -> leEq_def. intros Z0. apply Z. intros Z'. revert Z0. change (Not (e[<]AbsIR (f' x Hx)[-]inj_Q IR c)). rewrite <- leEq_def. clear Z. assert (J:Max LI' (x[-]d)[<]Min RI' (x[+]d)). destruct Z' as [Z'|Z']. apply less_leEq_trans with x. apply Max_less; auto. rstepr (x[-][0]). apply minus_resp_less_rht. auto. apply leEq_Min; auto with *. rstepl (x[+][0]). apply plus_resp_leEq_lft. apply less_leEq. auto with *. apply leEq_less_trans with x. apply Max_leEq; auto. rstepr (x[-][0]). apply minus_resp_leEq_rht. apply less_leEq. auto. apply less_Min; auto with *. rstepl (x[+][0]). apply plus_resp_less_lft. auto with *. destruct (Q_dense_in_CReals' _ _ _ J) as [q Hq0 Hq1]. rstepr (e[/]TwoNZ [+] e[/]TwoNZ). assert (HI0 : Compact I' (inj_Q IR q)). split; apply less_leEq. eapply leEq_less_trans;[|apply Hq0]. apply lft_leEq_Max. eapply less_leEq_trans;[apply Hq1|]. apply Min_leEq_lft. assert (Hq:Dom f' (inj_Q IR q)). apply (Derivative_imp_inc' _ _ _ _ Hf). apply (included_compact_in_interval _ properI x HI). apply (iprop_compact_in_interval_inc1 _ _ _ _ _ I'). auto. rstepl ((AbsIR (f' x Hx)[-]AbsIR (f' _ Hq))[+](AbsIR (f' _ Hq)[-]inj_Q IR c)). apply plus_resp_leEq_both. eapply leEq_transitive. apply leEq_AbsIR. assert (Z : Dom (FAbs f') x). split;auto. assert (Y : Dom (FAbs f') (inj_Q IR q)). split;auto. rewrite <- (FAbs_char _ _ Z). rewrite <- (FAbs_char _ _ Y). apply Hd0; auto. apply iprop_compact_in_interval'. apply AbsSmall_imp_AbsIR. split. apply shift_leEq_minus'. rstepl (inj_Q IR q[-]d). apply shift_minus_leEq. apply less_leEq. eapply less_leEq_trans;[apply Hq1|]. apply Min_leEq_rht. apply shift_minus_leEq. apply shift_leEq_plus'. apply less_leEq. eapply leEq_less_trans;[|apply Hq0]. apply rht_leEq_Max. eapply leEq_transitive;[|apply nonneg_div_two;apply less_leEq; auto]. clear - Hc HI0. apply shift_minus_leEq. rstepr (inj_Q IR c). apply Hc. apply (included_compact_in_interval _ properI x HI). apply (iprop_compact_in_interval_inc1 _ properI x HI _ I'). auto. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.Q_in_CReals CoRN.reals.fast.CRIR CoRN.ftc.Rolle CoRN.tactics.CornTac CoRN.model.metric2.Qmetric CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax