proposition: Lemma dmc_cdiv_cond_entropy_aux : W ``(y | x) = \prod_(a : A) \prod_(b : B) W a b ^ N(a, b | tuple_of_row x, tuple_of_row y).
proof: Proof. transitivity (\prod_(a : A) \prod_(b : B) \prod_(i < n) if (a == x ``_ i) && (b == y ``_ i) then W `(y ``_ i | x ``_ i) else 1). rewrite pair_big exchange_big /= DMCE. apply eq_bigr => i _. rewrite (bigD1 (x ``_ i, y ``_ i)) //= 2!eqxx andbT. rewrite big1; first by rewrite mulR1. case=> a b /=. rewrite xpair_eqE negb_and. case/orP. - by move/negbTE => ->. - move/negbTE => ->; by rewrite andbF. apply eq_bigr => a _; apply eq_bigr => b _. rewrite num_co_occ_alt -sum1_card. rewrite (@big_morph _ _ (fun x => W a b ^ x) 1 Rmult O addn) //; last first. move=> * /=; by rewrite -pow_add. rewrite [in RHS]big_mkcond. apply eq_bigr => i _. case: ifP. case/andP => /eqP Ha /eqP Hb. by rewrite inE 2!tnth_mktuple -Ha -Hb 2!eqxx /= mulR1. move/negbT. rewrite negb_and inE 2!tnth_mktuple. case/orP => /negbTE. by rewrite eq_sym => ->. by rewrite andbC eq_sym => ->. 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