proposition: Lemma wlln epsilon : 0 < epsilon -> `Pr[ (Rabs `o ((X `/ n.+1) `-cst miu)) >= epsilon ] <= sigma2 / (n.+1%:R * epsilon ^ 2).
proof: Proof. move=> e0. rewrite divRM ?INR_eq0' //; last exact/gtR_eqF/expR_gt0. have <- : `V (X `/ n.+1) = sigma2 / n.+1%:R. by rewrite -(Var_average X_Xs V_Xs) Var_scale //; field; exact/INR_eq0. have <- : `E (X `/ n.+1) = miu. rewrite E_scalel_RV (E_sum_n X_Xs). rewrite div1R mulRC eqR_divr_mulr ?INR_eq0' // (eq_bigr (fun=> miu)) //. by rewrite big_const /= iter_addR cardE /= size_enum_ord mulRC. move/leR_trans: (chebyshev_inequality (X `/ n.+1) e0); apply. by apply/RleP; rewrite lexx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist