proposition: Lemma joint_entropyC : joint_entropy = `H (fdistX P).
proof: Proof. congr (- _) => /=. rewrite (eq_bigr (fun a => P (a.1, a.2) * log (P (a.1, a.2)))); last by case. rewrite -(pair_bigA _ (fun a1 a2 => P (a1, a2) * log (P (a1, a2)))) /=. by rewrite exchange_big pair_big; apply eq_bigr => -[a 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