proposition: Lemma convex_function_comp (f : {convex T -> U}) (g : {convex U -> V}) : (forall a b t, f (a <|t|> b) <= f a <|t|> f b -> g (f (a <|t|> b)) <= g (f a <|t|> f b)) -> convex_function (g \o f).
proof: Proof. move=> fg a b t; have := convex_functionP g (f a) (f b) t. by move=> Hg; apply/(leconv_trans _ Hg)/fg/convex_functionP. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist