proposition: Lemma chain_rule_mutual_info : mutual_info PQR = mutual_info (fdist_proj13 PQR) + cond_mutual_info (fdistX (fdistA PQR)).
proof: Proof. rewrite mutual_infoE. have := chain_rule (PQR`1); rewrite /joint_entropy => ->. rewrite (chain_rule_corollary PQR). rewrite -addR_opp oppRD addRCA 2!addRA -(addRA (- _ + _)) addR_opp; congr (_ + _). rewrite mutual_infoE addRC; congr (_ - _). by rewrite fdist_proj13_fst fdistA1. rewrite /cond_mutual_info; congr (cond_entropy _ - _). by rewrite /fdist_proj13 -/(fdistC13 _) fdistA_C13_snd. rewrite /cond_entropy. rewrite (eq_bigr (fun a => (fdistA (fdistC12 PQR))`2 (a.1, a.2) * cond_entropy1 (fdistA (fdistC12 PQR)) (a.1, a.2))); last by case. rewrite -(pair_bigA _ (fun a1 a2 => (fdistA (fdistC12 PQR))`2 (a1, a2) * cond_entropy1 (fdistA (fdistC12 PQR)) (a1, a2))). rewrite exchange_big pair_big; apply eq_bigr => -[c a] _ /=; congr (_ * _). rewrite !fdist_sndE; apply eq_bigr => b _. by rewrite !(fdistXE,fdistAE,fdistC12E). rewrite /cond_entropy1; congr (- _). by under eq_bigr do rewrite -setX1 jcPr_fdistA_C12 setX1. Qed.
imports: mathcomp(all_ssreflect all_algebra fingroup perm matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext bigop_ext logb ln_facts fdist jfdist_cond proba binary_entropy_function divergence