Probability of Trivial-SigmaField (E) means :defTP: for A be Event of E holds it.A = prob(A); existence by LME10; uniqueness proof let F,G be Probability of Trivial-SigmaField (E); assume A1: for A be Event of E holds F.A =prob(A); assume A2: for A be Event of E holds G.A =prob(A); now let x be set; assume x in Trivial-SigmaField (E); then reconsider A=x as Event of E; thus F.x =prob(A) by A1.=G.x by A2; end; hence thesis by FUNCT_2:18; end; end; :: Real-Valued-Random-Variable definition let Omega,Sigma; mode Real-Valued-Random-Variable of Sigma -> Function of Omega,REAL means :def1: ex X be Element of Sigma st X = Omega & it is_measurable_on X; correctness proof reconsider X = Omega as Element of Sigma by MEASURE1:21; Q1: dom chi(X,Omega) =Omega by FUNCT_3:def 3; chi(X,Omega) is real-valued by MESFUNC2:31;then rng chi(X,Omega) c= REAL by VALUED_0:def 3; then reconsider f= chi(X,Omega) as Function of Omega,REAL by Q1,FUNCT_2:4; P2: R_EAL f = chi(X,Omega); chi(X,Omega) is_measurable_on X by MESFUNC2:32; then f is_measurable_on X by P2,MESFUNC6:def 6; hence thesis; end; end; reserve f,g,h for Real-Valued-Random-Variable of Sigma; theorem FPG: f+g is Real-Valued-Random-Variable of Sigma proof consider X be Element of Sigma such that P1: X=Omega & f is_measurable_on X by def1; consider Y be Element of Sigma such that P2: Y=Omega & g is_measurable_on Y by def1; thus thesis by def1,P1,P2,MESFUNC6:26; end; definition let Omega,Sigma,f,g; redefine func f+ g -> Real-Valued-Random-Variable of Sigma; correctness by FPG; end; theorem FMG: f-g is Real-Valued-Random-Variable of Sigma proof consider X be Element of Sigma such that P1: X=Omega & f is_measurable_on X by def1; consider Y be Element of Sigma such that P2: Y=Omega & g is_measurable_on Y by def1; dom g = Y by FUNCT_2:def 1,P2; hence thesis by def1,P1,P2,MESFUNC6:29; end; definition let Omega,Sigma,f,g; redefine func f-g -> Real-Valued-Random-Variable of Sigma; correctness by FMG; end; theorem RF: for r be Real holds r(#)f is Real-Valued-Random-Variable of Sigma proof let r be Real; consider X be Element of Sigma such that P1: X=Omega & f is_measurable_on X by def1; dom f = X by FUNCT_2:def 1,P1; hence thesis by def1,P1,MESFUNC6:21; end; definition let Omega,Sigma,f; let r be Real; redefine func r(#)f -> Real-Valued-Random-Variable of Sigma; correctness by RF; end; theorem Cor1: for f,g be PartFunc of Omega,REAL holds (R_EAL f)(#)(R_EAL g) = R_EAL (f(#)g) proof let f,g be PartFunc of Omega,REAL; P1: dom ((R_EAL f)(#) (R_EAL g)) =dom ( R_EAL f ) /\ dom ( R_EAL g ) by MESFUNC1:def 5 .=dom (f (#)g ) by VALUED_1:def 4; now let x be set; assume AS: x in dom ((R_EAL f )(#) (R_EAL g)); thus ((R_EAL f)(#)(R_EAL g)).x =((R_EAL f ).x) * ((R_EAL g).x) by AS,MESFUNC1:def 5 .= (f.x) * (g.x) by EXTREAL1:13 .= (f (#) g).x by VALUED_1:def 4,AS,P1; end; hence thesis by FUNCT_1:9,P1; end; theorem FXG: f(#)g is Real-Valued-Random-Variable of Sigma proof consider X be Element of Sigma such that P1: X = Omega & f is_measurable_on X by def1; consider Y be Element of Sigma such that P2: Y = Omega & g is_measurable_on Y by def1; P3:R_EAL f is_measurable_on X & R_EAL g is_measurable_on X by P1,P2,MESFUNC6:def 6; dom(R_EAL f)=X& dom(R_EAL g)=X by P1,FUNCT_2:def 1; then dom(R_EAL f) /\ dom(R_EAL g)=X; then (R_EAL f)(#)(R_EAL g) is_measurable_on X by P3,MESFUNC7:15;then R_EAL(f(#)g) is_measurable_on X by Cor1;then f(#)g is_measurable_on X by MESFUNC6:def 6; hence thesis by P1,def1; end; definition let Omega,Sigma,f,g; redefine func f(#)g -> Real-Valued-Random-Variable of Sigma; correctness by FXG; end; theorem AF0: for r be real number st 0 <= r & f is nonnegative holds (f to_power r) is Real-Valued-Random-Variable of Sigma proof let r be real number; assume AS:0 <= r & f is nonnegative; consider X be Element of Sigma such that P1: X=Omega & f is_measurable_on X by def1; P4: rng (f to_power r) c= REAL; P3: dom (f to_power r) = dom f by MESFUN6C:def 6; dom f = Omega by FUNCT_2:def 1;then P2: (f to_power r) is Function of Omega,REAL by P3,P4,FUNCT_2:4; dom f = X by FUNCT_2:def 1,P1; hence thesis by def1,P1,P2,AS,MESFUN6C:29; end; Lem02: for X be non empty set,f be PartFunc of X,REAL holds abs f is nonnegative proof let X be non empty set,f be PartFunc of X,REAL; now let x be set; assume x in dom (abs f);then (abs f).x = abs(f.x) by VALUED_1:def 11; hence 0 <= (abs f).x by COMPLEX1:132; end; hence abs f is nonnegative by MESFUNC6:52; end; theorem AF1: abs f is Real-Valued-Random-Variable of Sigma proof consider X be Element of Sigma such that P1: X=Omega & f is_measurable_on X by def1; P3: dom f = X by FUNCT_2:def 1,P1; R_EAL f is_measurable_on X by P1,MESFUNC6:def 6; then |.R_EAL f.| is_measurable_on X by P3,MESFUNC2:29; then R_EAL abs(f) is_measurable_on X by MESFUNC6:1; then abs(f) is_measurable_on X by MESFUNC6:def 6; hence thesis by def1,P1; end; definition let Omega,Sigma,f; redefine func abs f -> Real-Valued-Random-Variable of Sigma; correctness by AF1; end; theorem for r be real number st 0 <= r holds (abs(f) to_power r) is Real-Valued-Random-Variable of Sigma proof let r be real number; assume AS:0 <= r; abs f is nonnegative by Lem02; hence thesis by AS,AF0; end; :: Definition of the Expectations definition let Omega,Sigma,f,P; pred f is_integrable_on P means :defintf: f is_integrable_on P2M(P); end; definition let Omega,Sigma,P; let f be Real-Valued-Random-Variable of Sigma; assume AS0: f is_integrable_on P; func expect (f,P) -> Element of REAL equals :def2: Integral(P2M(P),f); correctness proof f is_integrable_on P2M(P) by AS0,defintf;then -infty < Integral(P2M(P),f) & Integral(P2M(P),f) < +infty by MESFUNC6:90; hence thesis by XXREAL_0:48; end; end; theorem EXPFG: f is_integrable_on P & g is_integrable_on P implies expect (f+g,P) = expect (f,P) + expect (g,P) proof assume AS0: f is_integrable_on P & g is_integrable_on P;then AS: f is_integrable_on P2M(P) & g is_integrable_on P2M(P) by defintf; set h=f+g; consider E be Element of Sigma such that P1: E = dom f /\ dom g & Integral(P2M(P),f+g) =Integral(P2M(P),f|E)+Integral(P2M(P),g|E) by AS,MESFUNC6:101; P2: dom f = Omega & dom g=Omega by FUNCT_2:def 1; P5: f|E = f by P2,P1,FUNCT_2:40; P7: Integral(P2M(P),f) =expect (f,P) by def2,AS0; P8: Integral(P2M(P),g) =expect (g,P) by def2,AS0; h is_integrable_on P2M(P) by AS,MESFUNC6:100; then h is_integrable_on P by defintf; hence expect (h,P) = Integral(P2M(P),f+g) by def2 .=Integral(P2M(P),f) +Integral(P2M(P),g) by P2,P1,FUNCT_2:40,P5 .= expect (f,P)+expect (g,P) by P7,P8,SUPINF_2:1; end; theorem EXPRF: f is_integrable_on P implies expect (r(#)f,P) = r* expect (f,P) proof set h=r(#)f; assume AS0: f is_integrable_on P;then AS: f is_integrable_on P2M(P) by defintf; P7: Integral(P2M(P),f) =expect (f,P) by AS0,def2; h is_integrable_on P2M(P) by AS,MESFUNC6:102; then h is_integrable_on P by defintf; hence expect (h,P) =Integral(P2M(P),r(#)f) by def2 .=(R_EAL r)*Integral(P2M(P),f) by AS,MESFUNC6:102 .= r* expect (f,P) by P7,EXTREAL1:13; end; theorem f is_integrable_on P & g is_integrable_on P implies expect (f-g,P) = expect (f,P) - expect (g,P) proof assume AS0: f is_integrable_on P & g is_integrable_on P;then g is_integrable_on P2M(P) by defintf;then (-1)(#)g is_integrable_on P2M(P) by MESFUNC6:102;then P1: (-1)(#)g is_integrable_on P by defintf; thus expect (f-g,P) = expect (f,P) + expect ((-1)(#)g,P) by P1,AS0,EXPFG .= expect (f,P) + (-1)*expect (g,P) by AS0,EXPRF .= expect (f,P) - expect (g,P); end; theorem for Omega be non empty finite set, f be Function of Omega,REAL holds f is Real-Valued-Random-Variable of Trivial-SigmaField (Omega) proof let Omega be non empty finite set, f be Function of Omega,REAL; set Sigma= Trivial-SigmaField (Omega); P1: ex X be Element of Sigma st dom f = X & f is_measurable_on X by Lm7; dom f = Omega by FUNCT_2:def 1; hence thesis by P1,def1; end; theorem LMTX3: for Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), X be Real-Valued-Random-Variable of Trivial-SigmaField (Omega) holds X is_integrable_on P proof let Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), X be Real-Valued-Random-Variable of Trivial-SigmaField (Omega); set M= P2M(P); dom X = Omega by FUNCT_2:def 1; then M.(dom X) = 1 by PROB_1:def 13; then dom X <> {} & M.(dom X) < +infty by XXREAL_0:9; then X is_integrable_on M by Lm9A0,Lm6; hence thesis by defintf; end; theorem LMTX4: for Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), X be Real-Valued-Random-Variable of Trivial-SigmaField (Omega), F being FinSequence of REAL, s being FinSequence of Omega st len F = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in dom F holds F.n = X.(s.n) * P.{s.n}) holds expect(X,P) = Sum F proof let Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), X be Real-Valued-Random-Variable of Trivial-SigmaField (Omega), F being FinSequence of REAL, s being FinSequence of Omega; assume that AS: len F = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in dom F holds F.n = X.(s.n) * P.{s.n}); set M = P2M(P); Integral(P2M(P),X) = Sum F by LMTX1,AS; hence thesis by def2,LMTX3; end; theorem for Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), X be Real-Valued-Random-Variable of Trivial-SigmaField (Omega) ex F being FinSequence of REAL, s being FinSequence of Omega st len F = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in dom F holds F.n = X.(s.n) * P.{s.n}) & expect(X,P) = Sum F proof let Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), X be Real-Valued-Random-Variable of Trivial-SigmaField (Omega); set M= P2M(P); P1: X is_integrable_on P by LMTX3; ex F being FinSequence of REAL, s being FinSequence of Omega st len F = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in dom F holds F.n = X.(s.n) * P.{s.n}) & Integral(P2M(P),X) = Sum F by LMTX2; hence thesis by def2,P1; end; theorem LMTX5: for Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), X be Real-Valued-Random-Variable of Trivial-SigmaField (Omega) ex F being FinSequence of REAL, s being FinSequence of Omega st len F = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in dom F holds F.n = X.(s.n) * P.{s.n}) & expect(X,P) = Sum F proof let Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), X be Real-Valued-Random-Variable of Trivial-SigmaField (Omega); set M= P2M(P); P1: X is_integrable_on P by LMTX3; ex F being FinSequence of REAL, s being FinSequence of Omega st len F = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in dom F holds F.n = X.(s.n) * P.{s.n}) & Integral(P2M(P),X) = Sum F by LMTX2; hence thesis by def2,P1; end; theorem for Omega be non empty finite set, X be Real-Valued-Random-Variable of Trivial-SigmaField (Omega), G being FinSequence of REAL, s being FinSequence of Omega st len G = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in dom G holds G.n = X.(s.n) ) holds expect(X,Trivial-Probability (Omega)) = (Sum G) / card (Omega) proof let Omega be non empty finite set, X be Real-Valued-Random-Variable of Trivial-SigmaField (Omega), G being FinSequence of REAL, s being FinSequence of Omega; assume that AS0: len G = card (Omega) and AS0a: s is one-to-one and AS0b: rng s = Omega & len s = card (Omega) and AS0c:(for n being Nat st n in dom G holds G.n = X.(s.n) ); set P= Trivial-Probability (Omega); deffunc GF(Nat) = X.(s.$1) * P.{s.$1}; consider F being FinSequence of REAL such that P2:len F = len G & for j being Nat st j in dom F holds F.j = GF(j) from FINSEQ_2:sch 1; P4: dom F = dom G by FINSEQ_3:31,P2;then P7: dom F = dom ((1/card (Omega))(#)G) by VALUED_1:def 5; now let n be Nat; assume AS1:n in dom F; dom s = Seg len s by FINSEQ_1:def 3 .= dom F by FINSEQ_1:def 3,AS0,AS0b,P2; then s.n in Omega by PARTFUN1:27,AS1; then reconsider A={s.n} as El_ev of Omega by RPR_1:7; P3: P.{s.n} = prob(A) by defTP .=1/card (Omega) by RPR_1:38; thus ((1/card (Omega))(#)G).n = (1/card (Omega))*G.n by VALUED_1:6 .= (1/card (Omega))*X.(s.n) by P4,AS1,AS0c .= F.n by P3,P2,AS1; end; then (1/card (Omega))(#)G = F by FINSEQ_1:17,P7; then expect(X,P) = Sum ((1/card (Omega))(#)G) by LMTX4,P2,AS0,AS0a,AS0b .= Sum(G) /card (Omega) by RVSUM_1:117; hence thesis; end; theorem for Omega be non empty finite set, X be Real-Valued-Random-Variable of Trivial-SigmaField (Omega) holds ex G being FinSequence of REAL, s being FinSequence of Omega st len G = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in dom G holds G.n = X.(s.n) ) & expect(X,Trivial-Probability (Omega)) = (Sum G) / card (Omega) proof let Omega be non empty finite set, X be Real-Valued-Random-Variable of Trivial-SigmaField (Omega); set P= Trivial-Probability (Omega); consider F being FinSequence of REAL, s being FinSequence of Omega such that P1: len F = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in dom F holds F.n = X.(s.n) * P.{s.n}) & expect(X,P) = Sum F by LMTX5; deffunc GF(Nat) = X.(s.$1); consider G being FinSequence of REAL such that P2:len G = len F & for j being Nat st j in dom G holds G.j = GF(j) from FINSEQ_2:sch 1; take G; P4: dom F = dom G by FINSEQ_3:31,P2;then P7: dom F = dom ((1/card (Omega))(#)G) by VALUED_1:def 5; now let n be Nat; assume AS0:n in dom F; dom s= Seg len s by FINSEQ_1:def 3 .= dom F by FINSEQ_1:def 3,P1; then s.n in Omega by PARTFUN1:27,AS0; then reconsider A={s.n} as El_ev of Omega by RPR_1:7; P3: P.{s.n} = prob(A) by defTP .=1/card (Omega) by RPR_1:38; thus ((1/card (Omega))(#)G).n = (1/card (Omega))*G.n by VALUED_1:6 .= (1/card (Omega))*X.(s.n) by P2,P4,AS0 .= F.n by AS0,P1 ,P3; end;then (1/card (Omega))(#)G = F by FINSEQ_1:17,P7; hence thesis by P1,P2,RVSUM_1:117; end; :: Markov's Theorem theorem for X be 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 proof let X be Real-Valued-Random-Variable of Sigma; assume that A1: 0 < r and A2:X is nonnegative and A30:X is_integrable_on P; A3: X is_integrable_on P2M(P) by A30,defintf; consider S be 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) = K proof now let t be set; assume P0:t in S /\ great_eq_dom(X,r); 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 K; end;then A7: S /\ great_eq_dom(X,r) c= K by TARSKI:def 3; now let x be set; assume x in K;then P0: ex t be 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; end; then K c= S /\ great_eq_dom(X,r) by TARSKI:def 3; hence thesis by XBOOLE_0:def 10,A7; end;then reconsider K as Element of Sigma by A5,A4,MESFUNC6:13; set PM=P2M(P); expect (X,P)=Integral(PM,X) by def2,A30; then reconsider IX=Integral(PM,X) as Element of REAL; PM.K <=1 by PROB_1:71;then Q1: PM.K < +infty by XXREAL_0:9,XXREAL_0:2; reconsider PMK=PM.K as Element of REAL by XXREAL_0:14; Q2: for t be Element of Omega st t in K holds r <= X.t proof let t be Element of Omega; assume t in K;then ex s be Element of Omega st s=t & r <= X.s; hence thesis; end; (R_EAL r)*(PM.K) <= Integral(PM,X|K) by LMMarkov2,A3,Q1,Q2,A4,A5;then P1: r*PMK <= Integral(PM,X|K) by EXTREAL1:13; Integral(PM,X|K) <= Integral(PM,X|S) by A2,A4,A5,MESFUNC6:87;then P2: Integral(PM,X|K) <= Integral(PM,X) by A4,FUNCT_2:40; r*PMK <= Integral(PM,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 thesis by def2,A30; end;