proposition: Lemma cond_entropy_fdistA : cond_entropy (fdistA PQR) = cond_entropy (fdistA (fdistAC PQR)).
proof: Proof. rewrite /cond_entropy /=. rewrite (eq_bigr (fun a => (fdistA PQR)`2 (a.1, a.2) * cond_entropy1 (fdistA PQR) (a.1, a.2))); last by case. rewrite -(pair_bigA _ (fun a1 a2 => (fdistA PQR)`2 (a1, a2) * cond_entropy1 (fdistA PQR) (a1, a2))) /=. rewrite exchange_big pair_big /=; apply eq_bigr => -[c b] _ /=; congr (_ * _). by rewrite fdistA_AC_snd fdistXE. by rewrite cond_entropy1_fdistAC. 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