proposition: Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R -> P [set x | X x >= a]%R <= mmt_gen_fun X r * (expR (- (r * a)))%:E.
proof: Proof. move=> t0. rewrite /mmt_gen_fun; have -> : expR \o r \o* X = (normr \o normr) \o [the {mfun T >-> R} of expR \o r \o* X]. by apply: funext => t /=; rewrite normr_id ger0_norm ?expR_ge0. rewrite expRN lee_pdivl_mulr ?expR_gt0//. rewrite (le_trans _ (markov _ (expR_gt0 (r * a)) _ _ _))//; last first. exact: (monoW_in (@ger0_le_norm _)). rewrite ger0_norm ?expR_ge0// muleC lee_pmul2l// ?lte_fin ?expR_gt0//. rewrite [X in _ <= P X](_ : _ = [set x | a <= X x]%R)//; apply: eq_set => t/=. by rewrite ger0_norm ?expR_ge0// lee_fin ler_expR mulrC ler_pM2r. 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