proposition: Lemma mutual_information_convex : convex_function (fun W : A -> {fdist B} => mutual_info (P `X W)).
proof: Proof. move=> /= p1yx p2yx t. pose p1xy := P `X p1yx. pose p2xy := P `X p2yx. pose p1 := p1xy`2. pose p2 := p2xy`2. pose plambdayx := fun a => p1yx a <| t |> p2yx a. pose plambdaxy := P `X plambdayx. pose plambday := plambdaxy`2. pose qlambdaxy := P `x plambday. pose q1xy := P `x p1. pose q2xy := P `x p2. rewrite /convex_function_at. have -> : mutual_info (P `X (fun x => p1yx x <| t |> p2yx x)) = D(plambdaxy || qlambdaxy). rewrite mutual_infoE0 /div pair_big /=; apply: eq_bigr => -[a b] _ /=. congr (_ * log (_ / _)). by rewrite /qlambdaxy fdist_prodE /= fdist_prod1. have -> : qlambdaxy = q1xy <| t |> q2xy. apply/fdist_ext => -[a b]. rewrite !fdist_prodE !fdist_convE /= /q1xy /q2xy !fdist_prodE /= /p1 /plambday. rewrite !fdist_sndE !big_distrr /= -big_split /=; apply eq_bigr => a0 _. rewrite /plambdaxy /= !fdist_prodE /= /p1xy /plambdayx fdist_convE /=. rewrite -!(RmultE,RplusE). field. have -> : plambdaxy = p1xy <| t |> p2xy. apply/fdist_ext => -[a b]. rewrite !fdist_prodE !fdist_convE /= /p1xy /p2xy !fdist_prodE /=. rewrite -!(RmultE,RplusE). field. have -> : mutual_info (P `X p1yx) = D(p1xy || q1xy). rewrite mutual_infoE0 /div pair_big /=; apply: eq_bigr => -[a b] _ /=. congr (_ * log (_ / _)). by rewrite /q1xy fdist_prodE /= fdist_prod1. have -> : mutual_info (P `X p2yx) = D(p2xy || q2xy). rewrite mutual_infoE0 /div pair_big /=; apply: eq_bigr => -[a b] _ /=. by congr (_ * log (_ / _)); rewrite /q2xy fdist_prodE fdist_prod1. apply: convex_relative_entropy. - apply/dominatesP => -[a b]. rewrite /q1xy /p1xy fdist_prodE /= mulR_eq0 /p1 /p1xy => -[|]. by rewrite fdist_prodE => ->; rewrite /= mul0r. by rewrite fdist_sndE => /psumr_eq0P ->. - apply/dominatesP => -[a b]. rewrite /q1xy /p1xy fdist_prodE /= mulR_eq0. rewrite /p1 /p1xy => -[|]. by rewrite fdist_prodE => ->; rewrite mul0r. by rewrite fdist_sndE => /psumr_eq0P /= ->. 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