proposition: Lemma converse_case2 : n%:R * log #|A|%:R <= @E_leng_cw _ _ P f -> `H (P `^ n) <= @E_leng_cw _ _ P f.
proof: Proof. move=> H; rewrite entropy_TupleFDist; apply: (leR_trans _ H). apply leR_wpmul2l; [exact/leR0n | exact/entropy_max]. 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