proposition: Lemma chain_rule_corollary : cond_entropy PQR = cond_entropy PR + cond_entropy QPR.
proof: Proof. rewrite !cond_entropyE -oppRD; congr (- _). rewrite [in X in _ = _ + X](eq_bigr (fun j => \sum_(i in B) (fdistX QPR) ((j.1, j.2), i) * log \Pr_QPR[[set i] | [set (j.1, j.2)]])); last by case. rewrite -[in RHS](pair_bigA _ (fun j1 j2 => \sum_(i in B) (fdistX QPR ((j1, j2), i) * log \Pr_QPR[[set i] | [set (j1, j2)]]))) /=. rewrite [in X in _ = _ + X]exchange_big /= -big_split; apply eq_bigr => c _ /=. rewrite [in LHS](eq_bigr (fun j => (fdistX PQR) (c, (j.1, j.2)) * log \Pr_PQR[[set (j.1, j.2)] | [set c]])); last by case. rewrite -[in LHS](pair_bigA _ (fun j1 j2 => (fdistX PQR) (c, (j1, j2)) * log \Pr_PQR[[set (j1, j2)] | [set c]])) /=. rewrite -big_split; apply eq_bigr => a _ /=. rewrite fdistXE fdist_proj13E big_distrl /= -big_split; apply eq_bigr => b _ /=. rewrite !(fdistXE,fdistAE,fdistC12E) /= -mulRDr. have [->|H0] := eqVneq (PQR (a, b, c)) 0; first by rewrite !mul0R. rewrite -logM; last 2 first. by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj13_dominN H0. by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1 fdistAE /= fdistC12E. congr (_ * log _). by rewrite -setX1 product_ruleC !setX1 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