proposition: Lemma apply_le_HN_logE_loge : `H P <= `E X + log ((exp 1) * `E X).
proof: Proof. apply: (leR_trans apply_max_HPN). rewrite leR_add2l mulRC /log (LogM _ (EX_gt0 P f_uniq) (exp_pos 1)). exact: le_entroPN_logeEX f_uniq. 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