proposition: Lemma concave_ln (t : {i01 R}) (a b : R^o) : 0 < a -> 0 < b -> (ln a : R^o) <| t |> (ln b : R^o) <= ln (a <| t |> b).
proof: Proof. move=> a0 b0; have := convex_expR t (ln a) (ln b). by rewrite !lnK// -(@ler_ln) ?posrE ?expR_gt0 ?conv_gt0// expRK. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex