proposition: Lemma le_eps eps : 0 <> n%:R -> 1 <= n%:R * log #|A|%:R -> 0 < eps -> log ((m eps)%:R * alp) * / (m eps)%:R * / n%:R <= eps.
proof: Proof. move=> nnon0 eps_pos cardA_non1. pose x := m' eps. pose Y := eps * INR n * ln 2. have npos : 0 < INR n. by case/Rdichotomy : nnon0 => //; rewrite (_ : 0 = INR 0)// => /INR_lt/ltP. have xpos : 0 < x. rewrite (_ : 0 = INR 0)//; apply: lt_INR; apply/leP. apply: (@leq_trans (m'' eps)); last exact: leq_maxr. by apply: (@leq_trans 1); last exact: leq_maxr. have mpos': (0 < floor (exp x))%Z. apply/lt_IZR/(@ltR_trans (exp x - 1)); last exact: (proj1 (floorP _)). rewrite -(@ltR_add2r 1) addRC /Rminus -addRA Rplus_opp_l 2!addR0 -exp_0. exact: exp_increasing. have le_1_alp : 1 <= alp. rewrite /alp -(mulR1 1). apply/leR_pmul => //. rewrite mulR1; apply: (@leR_trans 2); last exact: leR2e. by rewrite (_ : 1 = 1%:R) // (_ : 2 = 2%:R) // leR_nat. rewrite card_mx -natRexp mul1n log_pow //. rewrite (_ : 0 = INR 0) //; apply/lt_INR/ltP/fdist_card_neq0. exact: P. have alppos : 0 < alp by exact: (@ltR_leR_trans 1). have Ypos : 0 < Y by apply/mulR_gt0 => //; apply/mulR_gt0. apply: (Rmult_le_reg_r (INR (m eps) * INR n)). by apply: mulR_gt0 => //; apply/mpos. rewrite -mulRA (mulRC (/ INR n) _ ) -mulRA -mulRA -Rinv_r_sym; last exact: nesym. rewrite mulR1 mulVR ?mulR1; last exact/gtR_eqF/mpos/eqP/ltR_eqF. apply: (@leR_trans ((x ^ 2 / 2 - 1) * eps * (INR n))); last first. rewrite -mulRA mulRC -mulRA; apply: leR_wpmul2l; first exact: ltRW. rewrite mulRC; apply: leR_wpmul2r; first exact/ltRW. apply: (@leR_trans (exp x - 1)). rewrite leR_subl_addr subRK (_ : 2 = INR 2 `!)//; exact/(exp_lb 2)/pos_INR. rewrite INR_Zabs_nat; last exact/le_IZR/ltRW/IZR_lt. exact/ltRW/(proj1 (floorP _)). rewrite INR_Zabs_nat; last exact/le_IZR/Rlt_le/IZR_lt. rewrite {1}/log LogM//; last exact: IZR_lt. rewrite -/(log _). rewrite -(leR_pmul2r ln2_gt0). rewrite mulRDl /Log/Rdiv -(mulRA (ln alp)) (mulVR _ ln2_neq0). rewrite mulR1 -(mulRA _ (/ ln 2) _) (mulVR _ ln2_neq0). apply: (@leR_trans (x + ln alp)). rewrite leR_add2r ?mulR1 -(ln_exp x). apply: ln_increasing_le; last exact: (proj2 (floorP _)). apply: (@ltR_trans (exp x - 1)); last exact: proj1 (floorP _). rewrite subR_gt0 -exp_0; exact: exp_increasing. apply: (@leR_trans (2 * x - (eps * INR n * ln 2))). rewrite double /Rminus -addRA leR_add2l addR_opp leR_subr_addr (mulRC eps). apply: (@leR_trans (IZR (ceil (ln alp + n%:R * eps * ln 2)))); first exact: proj1 (ceilP _). rewrite -INR_Zabs_nat; first exact/le_INR/leP/leq_maxl. apply: le_IZR. apply: (@leR_trans (ln alp + Y)); last first. by rewrite /Y (mulRC eps); exact: proj1 (ceilP _). apply/addR_ge0; last exact/ltRW. by rewrite -(ln_exp 0) exp_0; exact: ln_increasing_le. rewrite -(mulRA _ eps) -(mulRA _ (eps * INR n)). rewrite mulRBl mul1R leR_add2r. apply: (Rmult_le_reg_r (/ Y * 2 * / x)). by apply/mulR_gt0; [apply/mulR_gt0 => //; exact/invR_gt0|exact/invR_gt0]. rewrite mulRC -mulRA (mulRC (/ x)) -mulRA -mulRA mulRV; last exact/gtR_eqF. rewrite mulR1 mulRC mulRA mulRA (mulRC _ (/x)) /= mulR1 mulRA (mulRC _ 2). rewrite -(mulRA _ Y) mulRV ?mulR1; last exact/gtR_eqF. rewrite (mulRC 2) !mulRA -(mulRA _ _ 2) !mulVR // ?(mul1R,mulR1); last 2 first. exact/eqP. exact/gtR_eqF. apply: (@leR_trans (m'' eps)%:R); last exact/le_INR/leP/leq_maxr. apply: (@leR_trans (m''' eps)%:R); last exact/le_INR/leP/leq_maxl. rewrite INR_Zabs_nat. apply: (@leR_trans ((4 * / (INR n * eps * ln 2)))); last exact: proj1 (ceilP _). by rewrite (mulRC n%:R); apply/RleP; rewrite lexx. apply: le_IZR. apply: (@leR_trans ((4 * / (INR n * eps * ln 2)))); last exact: proj1 (ceilP _). apply: Rle_mult_inv_pos; first exact: ltRW (@mulR_gt0 2 2 _ _). by rewrite (mulRC n%:R). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy divergence log_sum source_code