proposition: Lemma le_1_EX : 1 <= `E X.
proof: Proof. rewrite (_ : 1 = 1%mcR)// -(FDist.f1 P); apply: leR_sumR => i _. rewrite -{1}(mul1R (P i)). apply leR_wpmul2r; first exact/RleP/FDist.ge0. by move: (Xpos i); rewrite (_ : 1 = 1%:R) //= (_ : 0 = 0%:R) // ltR_nat leR_nat. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy divergence log_sum source_code