proposition: Lemma cond_mutual_infoE2 : cond_mutual_info PQR = \sum_(z in C) R z * cdiv1 PQR z.
proof: Proof. rewrite cond_mutual_infoE. rewrite (eq_bigr (fun x => PQR (x.1, x.2) * log (\Pr_PQR[[set x.1] | [set x.2]] / (\Pr_(fdist_proj13 PQR)[[set x.1.1] | [set x.2]] * \Pr_(fdist_proj23 PQR)[[set x.1.2] | [set x.2]])))); last by case. rewrite -(pair_bigA _ (fun x1 x2 => PQR (x1, x2) * log (\Pr_PQR[[set x1] | [set x2]] / (\Pr_(fdist_proj13 PQR)[[set x1.1] | [set x2]] * \Pr_(fdist_proj23 PQR)[[set x1.2] | [set x2]])))). rewrite exchange_big; apply eq_bigr => c _ /=. rewrite big_distrr /=; apply eq_bigr => -[a b] _ /=; rewrite mulRA; congr (_ * _). rewrite mulRC. move: (jproduct_rule PQR [set (a, b)] [set c]); rewrite -/R Pr_set1 => <-. by rewrite setX1 Pr_set1. 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