proposition: Lemma chebyshev_inequality epsilon : 0 < epsilon -> `Pr[ (Rabs `o (X `-cst `E X)) >= epsilon] <= `V X / epsilon ^ 2.
proof: Proof. move=> He; rewrite leR_pdivl_mulr; last exact/expR_gt0. rewrite mulRC /Var. apply (@leR_trans (\sum_(a in U | (`| X a - `E X | >= epsilon)%mcR) (((X `-cst `E X) `^2) a * P a))); last first. apply leR_sumRl_support with (Q := xpredT) => // a . by apply mulR_ge0 => //; exact: sq_RV_ge0. rewrite /Pr big_distrr. rewrite [_ ^2]lock /= -!lock. apply leR_sumRl => u; rewrite ?inE => Hu //=. - rewrite -!/(_ ^ 2). apply leR_wpmul2r => //. apply (@leR_trans ((X u - `E X) ^ 2)); last by apply/RleP; rewrite lexx. rewrite -(sqR_norm (X u - `E X)). by apply/pow_incr; split => //; [exact/ltRW | exact/RleP]. - by apply mulR_ge0 => //; exact: sq_RV_ge0. 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