proposition: Lemma entropy_ge0 : 0 <= `H.
proof: Proof. rewrite /entropy big_morph_oppR; apply/RleP/sumr_ge0 => i _; apply/RleP. have [->|Hi] := eqVneq (P i) 0; first by rewrite mul0R oppR0. rewrite mulRC -mulNR; apply mulR_ge0 => //; apply: oppR_ge0. rewrite -log1; apply: Log_increasing_le => //. by apply/RltP; rewrite lt0r Hi/=. 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