proposition: Lemma dmc_exp_cdiv_cond_entropy : W ``(y | x) = exp_cdiv P V W * exp2 (- INR n * `H(V | P)).
proof: Proof. rewrite /exp_cdiv. case : ifP => Hcase. - rewrite -ExpD -mulRDr. apply dmc_cdiv_cond_entropy => //. move=> a Pa; apply/dominatesP => b /eqP Wab. by move: Hcase => /forallP/(_ a)/implyP/(_ Pa)/forallP/(_ b)/implyP/(_ Wab)/eqP. - rewrite mul0R. move: Hcase => /negbT; rewrite negb_forall; case/existsP => a. rewrite negb_imply. case/andP => Pa. rewrite negb_forall_in ; move/existsP ; case => b. case/andP=> Wab H. rewrite dmc_cdiv_cond_entropy_aux. rewrite pair_big /= (bigD1 (a, b)) //=. rewrite mulR_eq0; left. move/eqP in Wab; rewrite Wab. apply pow_i. apply/ltP. rewrite lt0n. move: Htb ; rewrite in_set => /forallP/(_ a)/forallP/(_ b)/eqP ->. move: H => /=. rewrite (JType.c_f V) /=. move: (Vctyp). rewrite in_set. move/cond_type_equiv => /(_ _ Hta a) ->. move: Hta; rewrite in_set => /forallP/(_ a)/eqP => HPa. case: ifPn => Nax; last first. by apply: contra => /eqP ->; rewrite div0R. exfalso. move/eqP : Pa; apply. by rewrite HPa (eqP Nax) div0R. 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