proposition: Lemma ln_concave_at_gt0 x y (t : {prob R}) : x < y -> 0 < x -> 0 < y -> concave_function_at ln x y t.
proof: Proof. move=> xy x0 y0; apply RNconcave_function_at. set Df := fun x => - / x. move: t. have HDf : pderivable (fun x => - ln x) (fun x0 => x <= x0 <= y). rewrite (_ : (fun x => - ln x) = comp Ropp ln); last by rewrite boolp.funeqE. move=> r xry; apply derivable_pt_comp; last exact: derivable_pt_Ropp. apply/derivable_pt_ln/(@ltR_leR_trans x) => //; by case: xry. set DDf := fun x => / x^2. have HDDf : pderivable Df (fun x0 : R => x <= x0 <= y). rewrite /Df (_ : (fun x => - / x) = comp Ropp Rinv); last first. by rewrite boolp.funeqE. move=> r xry; apply derivable_pt_comp; last exact/derivable_pt_Ropp. rewrite (_ : Rinv = inv_fct (fun x => x)); last by rewrite boolp.funeqE. apply derivable_pt_inv; last exact: derivable_pt_id. by apply/eqP/gtR_eqF/(@ltR_leR_trans x) => //; case: xry. apply: (@second_derivative_convexf_pt _ _ _ HDf Df _ HDDf DDf) => //. - move=> r xry; rewrite /Df. have r0 : 0 < r by apply (@ltR_leR_trans x) => //; case: xry. transitivity (derive_pt (comp Ropp ln) _ (derivable_pt_comp ln Ropp _ (derivable_pt_ln r0) (derivable_pt_Ropp _))). by rewrite derive_pt_comp /= mulN1R. exact: proof_derive_irrelevance. - move=> r xry; rewrite /DDf /Df. have /eqP r0 : r != 0 by apply/gtR_eqF/(@ltR_leR_trans x) => //; case: xry. transitivity (derive_pt (comp Ropp Rinv) _ (derivable_pt_comp Rinv Ropp _ (derivable_pt_inv _ _ r0 (derivable_pt_id _)) (derivable_pt_Ropp _))). rewrite derive_pt_comp [in RHS]/= derive_pt_inv derive_pt_id mulN1R. by rewrite /Rdiv mulNR oppRK mul1R Rsqr_pow2 . exact/proof_derive_irrelevance. - move=> r; rewrite /DDf => -[x11 x12]. rewrite -expRV; last by apply/gtR_eqF/(@ltR_leR_trans x). exact/expR_ge0/ltRW/invR_gt0/(@ltR_leR_trans x). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex