proposition: Lemma Rabs_xlnx a (Ha : 0 <= a <= exp(-2)) x y : 0 <= x <= 1 -> 0 <= y <= 1 -> `| x - y | <= a -> `| xlnx x - xlnx y | <= - xlnx a.
proof: Proof. move=> [Hx1 Hx2] [Hy1 Hy2] H. case : (Rtotal_order x y) ; last case ; move => Hcase. - have Haux : y = x + `| x - y |. by rewrite distRC gtR0_norm ?subR_gt0 // subRKC. rewrite Haux -normRN oppRD oppRK addRC. apply (@leR_trans (- xlnx `| x - y |)). apply xlnx_delta_bound. - split. - exact/Rabs_pos_lt/eqP/ltR_eqF/subR_lt0. - by apply (@leR_trans a) => //; apply Ha. - by split => //; rewrite leR_subr_addr -Haux. rewrite leR_oppr oppRK. apply xlnx_decreasing_0_Rinv_e => //. - split; first exact: normR_ge0. apply (@leR_trans a) => //. apply (@leR_trans (exp (- 2))); first by apply Ha. apply/ltRW/exp_increasing; lra. - split; first by apply Ha. apply (@leR_trans (exp (-2))); first by apply Ha. apply/ltRW/exp_increasing; lra. - subst x ; rewrite subRR normR0 leR_oppr oppR0. case/orP : (orbN (0 == a)); last move=> anot0. move=> /eqP <-; rewrite xlnx_0. by apply/RleP; rewrite lexx. apply/ltRW/xlnx_neg; split. - by apply/RltP; rewrite lt0r eq_sym anot0; exact/RleP/(proj1 Ha). - exact: (leR_ltR_trans (proj2 Ha) ltRinve21). - apply Rgt_lt in Hcase. have Haux : x = y + `| x - y | by rewrite gtR0_norm ?subR_gt0 // subRKC. rewrite distRC in H Haux. rewrite Haux. apply (@leR_trans (- xlnx `| y - x |)). apply xlnx_delta_bound. - split. - exact/Rabs_pos_lt/eqP/ltR_eqF/subR_lt0. - by apply (@leR_trans a) => //; apply Ha. - split => //. by rewrite leR_subr_addr -Haux. rewrite leR_oppr oppRK. apply xlnx_decreasing_0_Rinv_e => //. + split; first exact: normR_ge0. apply (@leR_trans a) => //. apply (@leR_trans (exp (-2))); first by apply Ha. apply/ltRW/exp_increasing; lra. - split; first by apply Ha. apply (@leR_trans (exp (-2))); first by apply Ha. apply/ltRW/exp_increasing; lra. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex