proposition: Lemma le_aepbound_n : aep_bound P epsilon' <= INR n.
proof: Proof. rewrite /aep_bound . apply: (Rle_trans _ _ _ (proj1 (ceilP _))). rewrite -INR_Zabs_nat. apply: ltRW; apply: lt_INR. move: n0_Le_n. rewrite /n0 !gtn_max. case/andP=> _. case/andP=> _ H2. by apply/ltP. apply: le_IZR; apply: (Rle_trans _ (aep_sigma2 P / epsilon' ^ 3)); last by apply: (proj1 (ceilP _)). apply: Rmult_le_pos; first by apply: aep_sigma2_ge0. by apply: Rlt_le; apply: Rinv_0_lt_compat; apply: (pow_lt _ _ eps'_pos). 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