proposition: Lemma xlnx_delta_bound eps : 0 < eps <= exp (-2) -> forall x, 0 <= x <= 1 - eps -> `| xlnx_delta eps x | <= - xlnx eps.
proof: Proof. move=> [Heps1 Heps2] x [Hx1 Hx2]. apply/RleP; rewrite ler_norml; apply/andP; split; apply/RleP. - rewrite RoppE opprK (_ : xlnx eps = xlnx_delta eps 0); last first. by rewrite /xlnx_delta add0R xlnx_0 subR0. have [->|xnot0] := eqVneq x 0; first by apply/RleP; rewrite lexx. apply/ltRW/increasing_xlnx_delta => //. + exact: (conj Heps1 (leR_ltR_trans Heps2 ltRinve21)). + split; by [apply (@leR_trans x) |]. + by apply/RltP; rewrite lt0r xnot0/=; exact/RleP. - apply: (@leR_trans (xlnx_delta eps (1 - eps))). have [->|xnot0] := eqVneq x (1 - eps); first by apply/RleP; rewrite lexx. apply/ltRW/increasing_xlnx_delta => //. + exact: (conj Heps1 (leR_ltR_trans Heps2 ltRinve21)). + split; [by apply (@leR_trans x) | ]. by apply/RleP; rewrite lexx. + by apply/RltP; rewrite lt_neqAle xnot0/=; exact/RleP. rewrite /xlnx_delta subRK xlnx_1 sub0R leR_oppr oppRK. by apply: xlnx_ineq; split => //; apply/RleP/ltW/RltP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex