proposition: Lemma jensen_dist (r : A -> R) (X : {fdist A}) : (forall a, r a \in D) -> f (\sum_(a in A) X a * r a) <= \sum_(a in A) X a * f (r a).
proof: Proof. move=> HDr. apply (@proj1 _ (\sum_(a in fdist_supp X) X a * r a \in D)). rewrite [in X in _ <= X]sum_fdist_supp [in X in X <= _]sum_fdist_supp /=. apply: (@fdist_ind _ A (fun X => f (\sum_(a in fdist_supp X) X a * r a) <= \sum_(a in fdist_supp X) X a * f (r a) /\ _)) => //. move=> n IH {}X b cardA Hb. case/boolP : (X b == 1) => [/eqP|]Xb1. move/eqP : (Xb1); rewrite fdist1E1 => /eqP ->. by rewrite supp_fdist1 !big_set1 fdist1xx !mul1R. have HXb1: (X b).~ != 0 by rewrite onem_neq0. set d := fdistD1 Xb1. have HsumD1 q: \sum_(a in fdist_supp d) d a * q a = /(X b).~ * \sum_(a in fdist_supp d) X a * q a. rewrite (eq_bigr (fun a => /(X b).~ * (X a * q a))); last first. move=> i; rewrite inE fdistD1E. case: ifP => Hi; first by rewrite eqxx. by rewrite mulRCA mulRA -divRE RdivE. by rewrite -big_distrr. have {HsumD1}HsumXD1 q: \sum_(a in fdist_supp X) X a * q a = X b * q b + (X b).~ * (\sum_(a in fdist_supp d) d a * q a). rewrite HsumD1 mulRA mulRV // mul1R (bigD1 b) ?inE //=. rewrite (eq_bigl (fun a : A => a \in fdist_supp d)) //= => i. rewrite !inE /=. case HXi: (X i == 0) => //=. by rewrite (fdistD1_0 _ (eqP HXi)) eqxx. by rewrite fdistD1_eq0 // ?HXi // eq_sym. rewrite 2!{}HsumXD1. have /IH {IH}[IH HDd] : #|fdist_supp d| = n. by rewrite card_supp_fdistD1 // cardA. split; last first. move/asboolP: (convex_setP D). move/(_ (r b) (\sum_(a in fdist_supp d) d a * r a) (probfdist X b)). by rewrite classical_sets.in_setE; apply; rewrite -classical_sets.in_setE. move/leR_trans: (convex_f (probfdist X b) (HDr b) HDd); apply => /=. by rewrite leR_add2l; apply leR_wpmul2l => //; apply/onem_ge0. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(boolp Rstruct) Reals ssrR Reals_ext ssr_ext realType_ext ssralg_ext logb fdist proba convex