let Omega be non empty set ; :: thesis: for r being Real
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P holds
P . { t where t is Element of Omega : r <= X . t } <= (expect X,P) / r
let r be Real; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P holds
P . { t where t is Element of Omega : r <= X . t } <= (expect X,P) / r
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P holds
P . { t where t is Element of Omega : r <= X . t } <= (expect X,P) / r
let P be Probability of Sigma; :: thesis: for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P holds
P . { t where t is Element of Omega : r <= X . t } <= (expect X,P) / r
let X be Real-Valued-Random-Variable of Sigma; :: thesis: ( 0 < r & X is nonnegative & X is_integrable_on P implies P . { t where t is Element of Omega : r <= X . t } <= (expect X,P) / r )
assume that
A1: 0 < r and
A2: X is nonnegative and
A30: X is_integrable_on P ; :: thesis: P . { t where t is Element of Omega : r <= X . t } <= (expect X,P) / r
A3: X is_integrable_on P2M P by A30, defintf;
consider S being Element of Sigma such that
A4: ( S = Omega & X is_measurable_on S ) by def1;
A5: dom X = S by FUNCT_2:def 1, A4;
set K = { t where t is Element of Omega : r <= X . t } ;
S /\ (great_eq_dom X,r) = { t where t is Element of Omega : r <= X . t }

proof

now

let t be set ; :: thesis: ( t in S /\ (great_eq_dom X,r) implies t in { t where t is Element of Omega : r <= X . t } )
assume P0: t in S /\ (great_eq_dom X,r) ; :: thesis: t in { t where t is Element of Omega : r <= X . t }
t in great_eq_dom X,r by P0, XBOOLE_0:def 4;
then ( t in dom X & r <= X . t ) by MESFUNC1:def 15;
hence t in { t where t is Element of Omega : r <= X . t } ; :: thesis: verum

end;

then A7: S /\ (great_eq_dom X,r) c= { t where t is Element of Omega : r <= X . t } by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in { t where t is Element of Omega : r <= X . t } implies x in S /\ (great_eq_dom X,r) )
assume x in { t where t is Element of Omega : r <= X . t } ; :: thesis: x in S /\ (great_eq_dom X,r)
then P0: ex t being Element of Omega st
( x = t & r <= X . t ) ;
x in great_eq_dom X,r by A4, A5, P0, MESFUNC1:def 15;
hence x in S /\ (great_eq_dom X,r) by P0, A4, XBOOLE_0:def 4; :: thesis: verum

end;

then { t where t is Element of Omega : r <= X . t } c= S /\ (great_eq_dom X,r) by TARSKI:def 3;
hence S /\ (great_eq_dom X,r) = { t where t is Element of Omega : r <= X . t } by XBOOLE_0:def 10, A7; :: thesis: verum

end;

then reconsider K = { t where t is Element of Omega : r <= X . t } as Element of Sigma by A5, A4, MESFUNC6:13;
set PM = P2M P;
expect X,P = Integral (P2M P),X by def2, A30;
then reconsider IX = Integral (P2M P),X as Element of REAL ;
(P2M P) . K <= 1 by PROB_1:71;
then Q1: (P2M P) . K < +infty by XXREAL_0:9, XXREAL_0:2;
reconsider PMK = (P2M P) . K as Element of REAL by XXREAL_0:14;
Q2: for t being Element of Omega st t in K holds
r <= X . t

proof

let t be Element of Omega; :: thesis: ( t in K implies r <= X . t )
assume t in K ; :: thesis: r <= X . t
then ex s being Element of Omega st
( s = t & r <= X . s ) ;
hence r <= X . t ; :: thesis: verum

end;

(R_EAL r) * ((P2M P) . K) <= Integral (P2M P),(X | K) by LMMarkov2, A3, Q1, Q2, A4, A5;
then P1: r * PMK <= Integral (P2M P),(X | K) by EXTREAL1:13;
Integral (P2M P),(X | K) <= Integral (P2M P),(X | S) by A2, A4, A5, MESFUNC6:87;
then P2: Integral (P2M P),(X | K) <= Integral (P2M P),X by A4, FUNCT_2:40;
r * PMK <= Integral (P2M P),X by P1, P2, XXREAL_0:2;
then (r * PMK) / r <= IX / r by A1, XREAL_1:74;
then PMK <= IX / r by A1, XCMPLX_1:90;
hence P . { t where t is Element of Omega : r <= X . t } <= (expect X,P) / r by def2, A30; :: thesis: verum