proposition: Lemma chain_rule : joint_entropy PQ = `H P + cond_entropy QP.
proof: Proof. rewrite /joint_entropy {1}/entropy. transitivity (- (\sum_(a in A) \sum_(b in B) PQ (a, b) * log (P a * \Pr_QP [ [set b] | [set a] ]))). congr (- _); rewrite pair_big /=; apply eq_bigr => -[a b] _ /=. congr (_ * log _); have [H0|H0] := eqVneq (P a) 0. - by rewrite (dom_by_fdist_fst _ H0) H0 mul0R. - rewrite -(Pr_set1 P a) /P -(fdistX2 PQ) mulRC -jproduct_rule setX1. by rewrite Pr_set1 fdistXE. 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_QP [ [set b] | [set a] ]))). rewrite -oppRB; congr (- _); rewrite -addR_opp oppRK -big_split /=. apply eq_bigr => a _; rewrite -big_split /=; apply eq_bigr => b _. have [->|H0] := eqVneq (PQ (a, b)) 0; first by rewrite !mul0R addR0. rewrite -mulRDr; congr (_ * _); rewrite mulRC logM //. by rewrite -Pr_jcPr_gt0 setX1 Pr_set1 fdistXE; apply/RltP; rewrite -fdist_gt0. by apply/RltP; rewrite -fdist_gt0; exact: dom_by_fdist_fstN H0. rewrite [in X in _ + X = _]big_morph_oppR; congr (_ + _). - rewrite /entropy; congr (- _); apply eq_bigr => a _. by rewrite -big_distrl /= -fdist_fstE. - rewrite cond_entropyE big_morph_oppR. by apply eq_bigr => a _; congr (- _); apply eq_bigr => b _; rewrite !fdistXE. 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