proposition: Lemma ln_pos_uc_prf (c:Qpos) : @is_UniformlyContinuousFunction Q_as_MetricSpace CR (fun x => rational_ln (ln_uc_prf_pos c x)) (rational_ln_modulus c).
proof: Proof. set (lnf := fun x => match (Qlt_le_dec 0 x) with | left p => rational_ln p | right _ => 0%CR end). apply (is_UniformlyContinuousFunction_wd) with (fun x : Q_as_MetricSpace => lnf (QboundBelow_uc (proj1_sig c) x)) (Qscale_modulus (proj1_sig (Qpos_inv c))). intros x. unfold lnf. destruct (Qlt_le_dec 0 (QboundBelow_uc (proj1_sig c) x)). do 2 rewrite -> rational_ln_correct'. apply IRasCR_wd. algebra. elim (Qle_not_lt _ _ q). apply: ln_uc_prf_pos. intros [[xn xd] xpos]. destruct xn as [|xn|xn]. inversion xpos. 2: inversion xpos. destruct c as [[a b] cpos]. destruct a as [|a|a]. inversion cpos. 2: inversion cpos. apply: Qle_refl. assert (Z:Derivative (closel (inj_Q IR (proj1_sig c))) I Logarithm {1/}FId). apply (Included_imp_Derivative (openl [0]) I). Deriv. intros x Hx. simpl. apply less_leEq_trans with (inj_Q IR (proj1_sig c)); try assumption. stepl (inj_Q IR 0). apply inj_Q_less. simpl; auto with *. apply (inj_Q_nring IR 0). apply (is_UniformlyContinuousD (Some (proj1_sig c)) None I _ _ Z lnf). intros q Hq Hc. unfold lnf. destruct (Qlt_le_dec 0 q). apply rational_ln_correct. elim (Qle_not_lt _ _ q0). apply Qlt_le_trans with (proj1_sig c); auto with *. apply leEq_inj_Q with IR. assumption. intros x Hx Hc. apply AbsSmall_imp_AbsIR. apply leEq_imp_AbsSmall. apply: shift_leEq_div. apply less_leEq_trans with (inj_Q IR (proj1_sig c)); try assumption. stepl (inj_Q IR 0). apply inj_Q_less. simpl; auto with *. apply (inj_Q_nring IR 0). rstepl ([0]:IR). apply less_leEq. apply pos_one. stepr ([1][/]_[//](Greater_imp_ap _ _ _ (Qpos_adaptor (Qpos_ispos c)))). apply: recip_resp_leEq; try assumption. stepl (inj_Q IR 0). apply inj_Q_less. simpl; auto with *. apply (inj_Q_nring IR 0). stepl (((inj_Q IR 1)[/]_[//] Greater_imp_ap IR (inj_Q IR (proj1_sig c)) [0] (Qpos_adaptor (Qpos_ispos c)))). clear. destruct c as [[a b] cpos]. destruct a as [|a|a]. inversion cpos. 2: inversion cpos. unfold Qpos_inv, proj1_sig. change (inj_Q IR (/ (a#b))) with (inj_Q IR (1/(a#b))). apply eq_symmetric. apply inj_Q_div. apply div_wd. rstepr (nring 1:IR). apply (inj_Q_nring IR 1). apply eq_reflexive. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRartanh_slow CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.model.metric2.Qmetric CoRN.tactics.Qauto CoRN.transc.Exponential CoRN.transc.ArTanH CoRN.tactics.CornTac