proposition: Lemma increasing_xlnx_delta eps (Heps : 0< eps < 1) : forall x y : R, 0 <= x <= 1 - eps -> 0 <= y <= 1 - eps -> x < y -> xlnx_delta eps x < xlnx_delta eps y.
proof: Proof. apply derive_sincreasing_interv. - move=> x /= [Hx1 Hx2] ; rewrite /xlnx_delta. apply derivable_pt_minus. - apply (derivable_pt_comp (fun x => x + eps) xlnx). apply derivable_pt_plus ; first by apply derivable_pt_id. by apply derivable_pt_const. apply derivable_pt_xlnx. apply addR_gt0 => //; by apply Heps. - exact: derivable_pt_xlnx. - move=> x /= [Hx1 Hx2] ; rewrite /xlnx_delta. apply continuity_pt_minus. - apply (continuity_pt_comp (fun x => x + eps) xlnx); last by apply continue_xlnx. apply continuity_pt_plus ; first by apply derivable_continuous_pt, derivable_pt_id. by apply continuity_pt_const. - by apply continue_xlnx. - apply subR_gt0; by case: Heps. - move=> t prd Ht. rewrite (proof_derive_irrelevance _ (derivable_xlnx_delta Heps Ht)) //. rewrite derive_pt_xlnx_delta. apply/subR_gt0/ln_increasing; first by apply Ht. rewrite -{1}(addR0 t). by apply ltR_add2l, Heps. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex