proposition: Lemma chebyshev (X : {RV P >-> R}) (eps : R) : (0 < eps)%R -> P [set x | (eps <= `| X x - fine ('E_P[X])|)%R ] <= (eps ^- 2)%:E * 'V_P[X].
proof: Proof. move => heps; have [->|hv] := eqVneq 'V_P[X] +oo. by rewrite mulr_infty gtr0_sg ?mul1e// ?leey// invr_gt0// exprn_gt0. have h (Y : {RV P >-> R}) : P [set x | (eps <= `|Y x|)%R] <= (eps ^- 2)%:E * 'E_P[Y ^+ 2]. rewrite -lee_pdivr_mull; last by rewrite invr_gt0// exprn_gt0. rewrite exprnN expfV exprz_inv opprK -exprnP. apply: (@le_trans _ _ ('E_P[(@GRing.exp R ^~ 2%N \o normr) \o Y])). apply: (@markov Y (@GRing.exp R ^~ 2%N)) => //. - by move=> r; apply: sqr_ge0. - move=> x y; rewrite !nnegrE => x0 y0. by rewrite ler_sqr. apply: expectation_le => //. - by apply: measurableT_comp => //; exact: measurableT_comp. - by move=> x /=; apply: sqr_ge0. - by move=> x /=; apply: sqr_ge0. - by apply/aeW => t /=; rewrite real_normK// num_real. have := h [the {mfun T >-> R} of (X \- cst (fine ('E_P[X])))%R]. by move=> /le_trans; apply; rewrite /variance [in leRHS]unlock. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) HB(structures) exp numfun lebesgue_measure lebesgue_integral reals ereal signed topology normedtype sequences esum measure exp numfun lebesgue_measure lebesgue_integral