proposition: Lemma conditional_entropyE : cond_entropy d = 11/8.
proof: Proof. rewrite /cond_entropy /=. rewrite !big_ord_recl big_ord0 !fdist_sndE /=. rewrite !big_ord_recl !big_ord0 !dE /f /=. rewrite /cond_entropy1 /=. rewrite !big_ord_recl !big_ord0 /jcPr /Pr !(big_setX,big_set1) !dE /f /=. rewrite !fdist_sndE /=. rewrite !big_ord_recl !big_ord0 !dE /f !ffunE /=. rewrite !(addR0,add0R,div0R,mul0R). rewrite -!RplusE !addR0. repeat (rewrite logDiv; try lra). rewrite !log1 !sub0R !log4 !log8 !log16 !log32. rewrite [X in log X](_ : _ = 1/4); last lra. rewrite !div1R logV; last lra. rewrite !log4. rewrite [X in log X](_ : _ = 1/4); last lra. rewrite !div1R logV; last lra. rewrite !log4. rewrite [X in log X](_ : _ = 1/4); last lra. rewrite !div1R logV; last lra. rewrite !log4. field. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup finalg matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba jfdist_cond entropy