proposition: Lemma Jensen (P : {fdist A}) (X : {RV P -> R}) : (forall x, X x \in D) -> f (`E X) <= `E (f `o X).
proof: Proof. move=> H. rewrite {2}/Ex; erewrite eq_bigr; last by move=> a _; rewrite mulRC. rewrite {1}/Ex; erewrite eq_bigr; last by move=> a _; rewrite mulRC. exact: jensen_dist H. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(boolp Rstruct) Reals ssrR Reals_ext ssr_ext realType_ext ssralg_ext logb fdist proba convex