proposition: Lemma jensen_dist_concave (r : A -> R) (X : {fdist A}) : (forall x, r x \in D) -> \sum_(a in A) X a * f (r a) <= f (\sum_(a in A) X a * r a).
proof: Proof. move=> HDr. rewrite -[X in _ <= X]oppRK leR_oppr. apply/(leR_trans (jensen_dist convex_g X HDr))/Req_le. by rewrite big_morph_oppR; apply eq_bigr => a _; rewrite mulRN. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(boolp Rstruct) Reals ssrR Reals_ext ssr_ext realType_ext ssralg_ext logb fdist proba convex