proposition: Lemma n0_eps3 : 2 * (epsilon / (3 * (1 + log (INR #|X|)))) / INR n < epsilon / 3.
proof: Proof. move: (fdist_supp_lg_add_1_neq_0 P) => ?. rewrite mulRC /Rdiv -?mulRA; apply: (Rmult_lt_compat_l _ _ _ eps_pos); rewrite ?mulRA (mulRC _ 2). apply: (Rmult_lt_reg_l 3); first exact: Rplus_lt_pos. rewrite Rinv_mult // ?mulRA (mulRC 3 2) Rinv_r_simpl_l //. apply: (Rmult_lt_reg_l (INR n)); first exact/ltR0n. rewrite mulRC -mulRA (mulRC _ (INR n)) ?mulRA Rinv_r_simpl_l; last first. by apply/eqP; rewrite INR_eq0'. rewrite Rinv_r_simpl_l //. apply: (Rle_lt_trans _ _ _ (proj1 (ceilP _))). rewrite -INR_Zabs_nat. - apply: (lt_INR _ _). move : n0_Le_n; rewrite /n0 gtn_max. by case/andP => /ltP. - apply: le_IZR;apply: (Rle_trans _ (2 * / (1 + log (INR #|X|)))); last exact: (proj1 (ceilP _)). apply: Rmult_le_pos; first exact: ltRW. apply: Rlt_le; apply: Rinv_0_lt_compat. apply: Rplus_lt_le_0_compat => //. rewrite -(Log_1 2). apply: Log_increasing_le => //. exact: fdist_support_LB. 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