proposition: Lemma cdiv0P : D(V || W | P) = 0 <-> (P `X V) = (P `X W).
proof: Proof. rewrite cdiv_is_div_joint_dist; exact/div0P/joint_dominates. Qed.
imports: mathcomp(all_ssreflect ssralg finset matrix) Reals mathcomp(Rstruct) ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb ln_facts num_occ fdist entropy channel divergence types jtypes proba jfdist_cond