proposition: Lemma le_entroPN_logeEX : `H PN <= log (`E X) + log (exp 1).
proof: Proof. move/Rle_lt_or_eq_dec : le_1_EX => [?|eq_EX_1]; last first. rewrite -eq_EX_1 /log Log_1 add0R. by move/esym/entroPN_0 : eq_EX_1 ->; apply: log_exp1_Rle_0. have EX_1 : 0 < `E X - 1 by rewrite subR_gt0. have /eqP neq_EX1_0 : (`E X + -1) != 0 by exact/gtR_eqF. apply: (@leR_trans (`E X * log (`E X ) - (`E X - 1) * log((`E X ) -1))). exact: le_entroPN_logeEX'. rewrite -{1}(Rplus_minus 1 (`E X)) mulRDl mul1R /Rminus -addRA leR_add2l. rewrite -mulRN -mulRDr -(mul1R (log (exp 1))) -{3}(subRKC (`E X) 1) -oppRB. rewrite (addR_opp (log (`E X))) -logDiv //; last exact EX_gt0. by apply: div_diff_ub; [exact/ltRW | by move=> EX0; exfalso; move: EX0; apply/eqP/gtR_eqF/EX_gt0 | exact/ltRW/EX_gt0]. 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