proposition: Lemma mutual_information_concave : concave_function (fun P : choice_of_Type {fdist A} => mutual_info (P `X W)).
proof: Proof. suff : concave_function (fun P : choice_of_Type {fdist A} => let PQ := fdistX (P `X W) in `H PQ`1 - cond_entropy PQ). set f := fun _ => _. set g := fun _ => _. suff -> : f = g by []. by rewrite boolp.funeqE => d; rewrite {}/f {}/g /= -mutual_infoE -mutual_info_sym. apply: R_concave_functionB. have /RNconvex_function concave_H := entropy_concave B_not_empty. apply: R_concave_functionN => p q t /=. rewrite /convex_function_at 3!fdistX1. apply: leR_trans (concave_H (p `X W)`2 (q `X W)`2 t). under eq_bigr do rewrite fdist_prod2_conv. by apply/RleP; rewrite lexx. suff : affine (fun x : choice_of_Type {fdist A} => cond_entropy (fdistX (x `X W))). by move=> /affine_functionP[]. move=> t p q. rewrite /= avgRE /cond_entropy /cond_entropy1. rewrite 2!big_distrr -big_split /=; apply eq_bigr => a _. rewrite !fdistX2 !fdist_fstE !mulRN -oppRD; congr (- _). rewrite !big_distrr -big_split /=; apply eq_bigr => b _. rewrite !big_distrl !big_distrr -big_split /=; apply eq_bigr => b0 _. rewrite !fdist_prodE /= fdist_convE /= !(mulRA (Prob.p t)) !(mulRA (Prob.p t).~). rewrite -!(RmultE,RplusE). have [Hp|/eqP Hp] := eqVneq (Prob.p t * p a) 0. rewrite Hp ?(add0R,mul0R). have [->|/eqP Hq] := eqVneq ((Prob.p t).~ * q a) 0. by rewrite ?(mul0R). rewrite jcPr_fdistX_prod /=; last first. by rewrite fdist_convE -RplusE -!RmultE Hp add0R. by rewrite jcPr_fdistX_prod //=; move: Hq; rewrite mulR_neq0 => -[]. have [Hq|Hq] := eqVneq ((Prob.p t).~ * q a) 0. rewrite Hq !(mul0R,addR0). rewrite jcPr_fdistX_prod; last first. by rewrite fdist_convE -RplusE -!RmultE Hq addR0. by rewrite jcPr_fdistX_prod //=; move: Hp; rewrite mulR_neq0 => -[]. rewrite jcPr_fdistX_prod; last first. by rewrite /= fdist_convE paddR_eq0; [tauto|exact/mulR_ge0|exact/mulR_ge0]. rewrite jcPr_fdistX_prod; last by move: Hp; rewrite mulR_neq0 => -[]. rewrite jcPr_fdistX_prod //=; last by move/eqP: Hq; rewrite mulR_neq0 => -[]. move/eqP in Hq. rewrite /onem -RminusE (_ : 1%mcR = 1)//. rewrite /onem -RminusE (_ : 1%mcR = 1)// in Hq. by rewrite -!mulRDl. 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