proposition: Lemma aep_bound_ge0 e (_ : 0 < e) : 0 <= aep_bound e.
proof: Proof. apply divR_ge0; [exact: aep_sigma2_ge0 | exact/pow_lt]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext bigop_ext ssralg_ext logb fdist proba entropy