proposition: Lemma continue_xlnx : continuity xlnx.
proof: Proof. rewrite /continuity => r. rewrite /continuity_pt /continue_in /limit1_in /limit_in => eps eps_pos /=. case (total_order_T 0 r) ; first case ; move=> Hcase. - have : continuity_pt (fun x => x * ln x) r. apply continuity_pt_mult. by apply derivable_continuous_pt, derivable_id. by apply derivable_continuous_pt, derivable_pt_ln. rewrite /continuity_pt /continue_in /limit1_in /limit_in => /(_ eps eps_pos). case => /= k [k_pos Hk]. exists (Rmin k r); split; first exact/Rlt_gt/Rmin_pos. - move=> x ; rewrite /D_x ; move => [[_ Hx1] Hx2]. rewrite /xlnx. have -> : (0 < x)%mcR. apply/RltP. rewrite -(addR0 x) -{1}(subRR r) addRA addRAC. apply (@leR_ltR_trans ((x + - r) + `| x + - r |)). rewrite addRC -leR_subl_addr sub0R -normRN; exact: Rle_abs. rewrite /R_dist in Hx2. by apply/ltR_add2l/(@ltR_leR_trans (Rmin k r)) => //; exact: geR_minr. have -> : (0 < r)%mcR by apply/RltP. apply Hk. split => //. exact/(ltR_leR_trans Hx2)/geR_minl. - subst r. exists (exp (- 2 * / eps)). split ; first exact: exp_pos. move=> x; rewrite /R_dist subR0; case=> Hx1 Hx2. rewrite /xlnx ltxx. case: ifPn => /RltP Hcase. + rewrite (geR0_norm _ (ltRW Hcase)) in Hx2. rewrite subR0 -{1}(exp_ln _ Hcase). set X := ln x. have X_neg : X < 0. apply (@ltR_trans (-2 * / eps)). by apply exp_lt_inv; subst X; rewrite exp_ln. rewrite mulNR. exact/oppR_lt0/divR_gt0. apply: (@ltR_leR_trans (2 * / (- X))). * rewrite ltR0_norm; last first. rewrite -(mulR0 (exp X)) ltR_pmul2l => //; exact: exp_pos. rewrite -mulRN. apply (@ltR_pmul2r (/ - X)); first exact/invR_gt0/oppR_gt0. rewrite -mulRA mulRV ?mulR1; last by rewrite oppR_eq0; apply/ltR_eqF. rewrite -(invRK 2) -mulRA. rewrite ( _ : forall r, r * r = r ^ 2); last by move=> ?; rewrite /pow mulR1. rewrite expRV; last exact/eqP/not_eq_sym/eqP/ltR_eqF/oppR_gt0. rewrite -invRM; last 2 first. by rewrite invR_neq0' //; exact/gtR_eqF. by rewrite expR_eq0 oppR_eq0; exact/ltR_eqF. rewrite -(invRK (exp X)). apply ltR_inv => //. exact/invR_gt0/exp_pos. by apply/mulR_gt0; [lra | apply expR_gt0; lra]. rewrite -exp_Ropp mulRC (_ : 2 = INR 2`!) //. exact/exp_strict_lb/oppR_gt0. * apply (@leR_pmul2r (/ 2)); first exact/invR_gt0. rewrite mulRC mulRA mulVR ?mul1R //; last exact/gtR_eqF. rewrite -(invRK eps) -invRM //; last 2 first. exact/gtR_eqF/invR_gt0. exact/eqP. apply leR_inv => //. - by apply/mulR_gt0 => //; exact: invR_gt0. - rewrite leR_oppr mulRC -mulNR. by apply/exp_le_inv/ltRW; subst X; rewrite exp_ln. + by rewrite subRR normR0. - exists (- r); split; first exact/oppR_gt0. move=> x [[_ Hx1] Hx2]. rewrite /R_dist /xlnx. have -> : (0 < x)%mcR = false. apply/RltP/leRNgt. rewrite -(addR0 x) -{1}(subRR r) addRA addRAC. apply (@leR_trans ((x + - r) - `| x + - r |)). apply/leR_add2l/ltRW; by rewrite ltR_oppr. exact/Rle_minus/Rle_abs. have -> : (0 < r)%mcR = false by apply/negbTE; rewrite -leNgt; apply/RleP/ltRW. by rewrite subRR normR0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex