proposition: Lemma entropy_concave : concave_function (fun P : choice_of_Type {fdist A} => `H P).
proof: Proof. apply RNconcave_function => p q t; rewrite /convex_function_at. rewrite !(entropy_log_div _ cardApredS) /= /leconv /= [in X in _ <= X]avgRE. rewrite oppRD oppRK 2!mulRN mulRDr mulRN mulRDr mulRN oppRD oppRK oppRD oppRK. rewrite addRCA !addRA -2!mulRN -mulRDl (addRC _ (Prob.p t)). rewrite !RplusE onemKC mul1R -!RplusE -addRA leR_add2l. have := convex_relative_entropy t (dom_by_uniform p cardApredS) (dom_by_uniform q cardApredS). by rewrite convmm. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(mathcomp_extra Rstruct reals) Reals Ranalysis_ext Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist jfdist_cond entropy convex binary_entropy_function log_sum divergence