proposition: Lemma n0_eps4 : 2 * / INR n < epsilon / 4.
proof: Proof. move: n0_Le_n; rewrite /n0 !gtn_max; case/andP=> _; case/andP=> Hyp _. apply: (Rmult_lt_reg_l 4); first by lra. rewrite /Rdiv (mulRC epsilon (/ 4)) mulRA mulRA ?mulRV; last first. by rewrite gtR_eqF //; lra. rewrite (_ : 4 * 2 = 8) ?mul1R; last by lra. apply: (Rmult_lt_reg_l (INR n)); first exact/ltR0n. rewrite mulRA (mulRC _ 8) Rinv_r_simpl_l; last by apply/eqP; rewrite INR_eq0'. apply: (Rmult_lt_reg_l ( / epsilon)); first by apply: Rinv_0_lt_compat. rewrite mulRC (mulRC (/ epsilon) (INR n * epsilon)) Rinv_r_simpl_l; last by apply: nesym; apply: Rlt_not_eq=>//. apply: (Rle_lt_trans _ (IZR (ceil (8 * / epsilon))) _ (proj1 (ceilP _))). rewrite -INR_Zabs_nat. - by apply: lt_INR; apply/ltP. - apply: le_IZR;apply: (Rle_trans _ (8 * / epsilon)); last by apply: (proj1 (ceilP _)). by apply: Rle_mult_inv_pos; [lra | apply 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