proposition: Lemma mutual_infoE : mutual_info PQ = `H P - cond_entropy PQ.
proof: Proof. rewrite mutual_infoE0. transitivity (\sum_(a in A) \sum_(b in B) PQ (a, b) * log (\Pr_PQ [ [set a] | [set b] ] / P a)). apply eq_bigr => a _; apply eq_bigr => b _. rewrite /jcPr setX1 2!Pr_set1 /= -/Q. have [->|H0] := eqVneq (PQ (a, b)) 0; first by rewrite !mul0R. by congr (_ * log _); rewrite divRM 1?mulRAC //; [ exact: dom_by_fdist_fstN H0 | exact: dom_by_fdist_sndN H0]. transitivity (- (\sum_(a in A) \sum_(b in B) PQ (a, b) * log (P a)) + \sum_(a in A) \sum_(b in B) PQ (a, b) * log (\Pr_PQ [ [set a] | [set b] ])). rewrite big_morph_oppR -big_split; apply/eq_bigr => a _ /=. rewrite big_morph_oppR -big_split; apply/eq_bigr => b _ /=. rewrite addRC -mulRN -mulRDr addR_opp. have [->|H0] := eqVneq (PQ (a, b)) 0; first by rewrite !mul0R. congr (_ * _); rewrite logDiv //. - by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1. - by apply/RltP; rewrite -fdist_gt0; exact: dom_by_fdist_fstN H0. rewrite -subR_opp; congr (_ - _). - rewrite /entropy; congr (- _); apply/eq_bigr => a _. by rewrite -big_distrl /= -fdist_fstE. - rewrite /cond_entropy exchange_big. rewrite big_morph_oppR; apply eq_bigr=> b _ /=. rewrite mulRN; congr (- _). rewrite big_distrr /=; apply eq_bigr=> a _ /=. rewrite mulRA; congr (_ * _); rewrite -/Q. by rewrite -[in LHS]Pr_set1 -setX1 jproduct_rule Pr_set1 -/Q mulRC. 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