proposition: Lemma dmc_cdiv_cond_entropy : W ``(y | x) = exp2 (- INR n * (D(V || W | P) + `H(V | P))).
proof: Proof. rewrite dmc_cdiv_cond_entropy_aux cond_entropy_chanE2. rewrite /cdiv /entropy -big_split /=. rewrite (big_morph _ (morph_mulRDr _) (mulR0 _)). rewrite (big_morph _ morph_exp2_plus exp2_0). apply eq_bigr => a _. rewrite big_morph_oppR. rewrite /div /= -mulRDr mulRA -big_split /=. rewrite (big_morph _ (morph_mulRDr _) (mulR0 _)). rewrite (big_morph _ morph_exp2_plus exp2_0). apply eq_bigr => b _. case/boolP : (type.d P a == 0) => [/eqP|] Pa0. move: Hy; rewrite in_set => /forallP/(_ a)/forallP/(_ b)/eqP => ->. move: (HV); rewrite in_set => /cond_type_equiv/(_ _ Hx a). move: Hx; rewrite in_set => /forallP/(_ a)/eqP; rewrite {}Pa0 => HPa sumB. move: HPa; rewrite -sumB => /esym; rewrite mulR_eq0 => -[/eqP|/eqP]; last first. by move/invR_eq0'; rewrite INR_eq0' (negbTE Hn). rewrite INR_eq0' sum_nat_eq0 => /forall_inP/(_ b erefl)/eqP => H; apply/eqP. by rewrite H pow_O !(mulR0,mul0R) exp2_0. case/boolP : (W a b == 0) => [/eqP |] Wab0. move: (dominatesE (W0_V0 Pa0) Wab0) => nullV. suff -> : N(a, b| tuple_of_row x, tuple_of_row y) = O. by rewrite nullV 2!mul0R oppR0 addR0 mulR0 exp2_0. move: Hy; rewrite in_set => /forallP/(_ a)/forallP/(_ b)/eqP => ->. by rewrite jtype_0_jtypef. rewrite -{1}(@logK (W a b)); last first. apply/RltP. by rewrite -fdist_gt0. case/boolP : (V a b == 0) => [/eqP|] Vab0. suff -> : N( a, b | [seq x ``_ i | i <- enum 'I_n], [seq y ``_ i | i <- enum 'I_n]) = O. by rewrite pow_O Vab0 !(mulR0,mul0R,addR0,add0R,oppR0,exp2_0). move: Hy; rewrite in_set => /forallP/(_ a)/forallP/(_ b)/eqP => ->. by rewrite jtype_0_jtypef. rewrite -exp2_pow; congr exp2. rewrite -mulRN -mulRDr mulRA addR_opp -logDiv; last 2 first. apply/divR_gt0. apply/RltP. by rewrite -fdist_gt0//. apply/RltP. by rewrite -fdist_gt0//. apply/RltP. by rewrite -fdist_gt0//. rewrite /Rdiv (mulRAC _ (/ _)) mulRV // mul1R logV -?fdist_gt0 //; last first. apply/RltP. by rewrite -fdist_gt0//. rewrite mulRN 3!mulNR oppRK; congr (_ * log _). move: Hy; rewrite in_set => /forallP/(_ a)/forallP/(_ b)/eqP => ->. move: (HV); rewrite in_set => /cond_type_equiv => /(_ _ Hx a) sumB. move: Hx; rewrite in_set => /forallP/(_ a)/eqP => HPa. rewrite (JType.c_f V) /=. case: ifPn => [/eqP|] HP. - rewrite HPa -sumB HP div0R mulR0 mul0R. move/eqP : HP; rewrite sum_nat_eq0 => /forallP/(_ b). by rewrite implyTb => /eqP ->. - rewrite HPa -sumB (mulRCA (INR n)) mulRV ?INR_eq0' // mulR1. by rewrite mulRCA mulRV ?mulR1 // INR_eq0'. 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