proposition: Lemma cond_mutual_infoE : cond_mutual_info PQR = \sum_(x in {: A * B * C}) PQR x * 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]])).
proof: Proof. rewrite /cond_mutual_info 2!cond_entropyE /= subR_opp big_morph_oppR. rewrite (eq_bigr (fun a => \sum_(b in A) (fdistX (fdistA PQR)) (a.1, a.2, b) * log \Pr_(fdistA PQR)[[set b] | [set (a.1, a.2)]])); last by case. rewrite -(pair_bigA _ (fun a1 a2 => \sum_(b in A) (fdistX (fdistA PQR)) ((a1, a2), b) * log \Pr_(fdistA PQR)[[set b] | [set (a1, a2)]])). rewrite exchange_big -big_split /=. 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_morph_oppR /= exchange_big -big_split /=. rewrite (eq_bigr (fun i => PQR ((i.1, i.2), c) * log (\Pr_PQR[[set (i.1, i.2)] | [set c]] / (\Pr_(fdist_proj13 PQR)[[set i.1] | [set c]] * \Pr_(fdist_proj23 PQR)[[set i.2] | [set c]])))); last by case. rewrite -(pair_bigA _ (fun i1 i2 => PQR (i1, i2, c) * log (\Pr_PQR[[set (i1, i2)] | [set c]] / (\Pr_(fdist_proj13 PQR)[[set i1] | [set c]] * \Pr_(fdist_proj23 PQR)[[set i2] | [set c]])))). apply eq_bigr => a _ /=. rewrite fdistXE fdist_proj13E big_distrl /= big_morph_oppR -big_split. apply eq_bigr => b _ /=. rewrite fdistXE fdistAE /= -mulRN -mulRDr. have [->|H0] := eqVneq (PQR (a, b, c)) 0; first by rewrite !mul0R. congr (_ * _). rewrite addRC addR_opp -logDiv; last 2 first. by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdistA_dominN H0. by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj13_dominN H0. congr (log _). rewrite divRM; last 2 first. by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj13_dominN H0. by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj23_dominN H0. rewrite {2}/Rdiv -mulRA mulRCA {1}/Rdiv [in LHS]mulRC; congr (_ * _). rewrite -[in X in _ = X * _]setX1 jproduct_rule_cond setX1 -mulRA mulRV ?mulR1 //. rewrite /jcPr divR_neq0' // ?setX1 !Pr_set1. exact: fdist_proj23_dominN H0. by rewrite fdist_proj23_snd; exact: dom_by_fdist_sndN H0. 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