proposition: Lemma eps'_pos : 0 < epsilon'.
proof: Proof. rewrite /epsilon' /Rdiv -(mulR0 epsilon); apply ltR_pmul2l => //; apply/invR_gt0. apply: Rplus_lt_le_0_compat; first lra. apply: Rmult_le_pos; first lra. rewrite -(Log_1 2). exact: (Log_increasing_le _ _ (fdist_support_LB P)). Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq natbin source_code