proposition: Lemma cond_entropy1_ge0 a : 0 <= cond_entropy1 a.
proof: Proof. rewrite /cond_entropy1 big_morph_oppR; apply/RleP/sumr_ge0 => b _; rewrite -mulRN. have [->|H0] := eqVneq (\Pr_QP[[set b]|[set a]]) 0. by rewrite mul0R. apply/RleP/mulR_ge0; [exact: jcPr_ge0|]. rewrite -oppR0 -(Log_1 2) /log leR_oppr oppRK. by apply Log_increasing_le => //; [rewrite jcPr_gt0 | exact: jcPr_le1]. Qed.
imports: mathcomp(all_ssreflect all_algebra fingroup perm matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext bigop_ext logb ln_facts fdist jfdist_cond proba binary_entropy_function divergence