Probability of Trivial-SigmaField (E) means :Def1: for A be Event of E holds it.A = prob(A); existence proof deffunc F(Element of bool E)=In(prob($1),REAL); consider EP be Function of Trivial-SigmaField (E),REAL such that A1: for x be Element of Trivial-SigmaField (E) holds EP.x=F(x) from FUNCT_2:sch 4; A2: for A,B being Event of Trivial-SigmaField (E) st A misses B holds EP.(A \/ B) = EP.A + EP.B proof let A,B being Event of Trivial-SigmaField (E); assume A3: A misses B; A4: EP.B = F(B) by A1 .= prob B; thus EP.(A \/ B) = F(A \/ B) by A1 .=prob(A \/ B) .=((prob A) + (prob B)) - (prob (A /\ B)) by RPR_1:20 .=prob (A) + prob (B) - 0 by A3,RPR_1:16 .= F(A) + prob (B) .= (EP.A) + prob (B) by A1 .= (EP.A) + ((EP.B) qua Real) by A4 .= (EP.A) + (EP.B); end; A5: for A being Event of Trivial-SigmaField (E) holds 0 <= EP.A proof let A being Event of Trivial-SigmaField (E); EP.A = F(A) by A1 .=prob(A); hence thesis; end; A6: for ASeq being SetSequence of Trivial-SigmaField (E) st ASeq is non-ascending holds EP * ASeq is convergent & lim (EP * ASeq) = EP.( Intersection ASeq) proof let ASeq being SetSequence of Trivial-SigmaField (E); assume ASeq is non-ascending; then consider N be Nat such that A7: for m be Nat st N<=m holds Intersection ASeq = ASeq.m by Th15; now let m be Nat; assume A8: N <= m; m in NAT by ORDINAL1:def 12; then m in dom ASeq by FUNCT_2:def 1; hence (EP * ASeq).m = EP.(ASeq.m) by FUNCT_1:13 .= EP.(Intersection ASeq) by A7,A8; end; hence thesis by PROB_1:1; end; EP.E =F([#]E) by A1 .=prob([#]E) .= 1 by RPR_1:15; then reconsider EP as Probability of Trivial-SigmaField (E) by A5,A2,A6,PROB_1:def 8; take EP; let A be Event of E; thus EP.A = F(A) by A1 .= prob(A); end; uniqueness proof let F,G be Probability of Trivial-SigmaField (E); assume A9: for A be Event of E holds F.A =prob(A); assume A10: for A be Event of E holds G.A =prob(A); now let x be object; assume x in Trivial-SigmaField (E); then reconsider A=x as Event of E; thus F.x =prob(A) by A9 .=G.x by A10; end; hence thesis by FUNCT_2:12; end; end; :: Real-Valued-Random-Variable definition let Omega,Sigma; mode Real-Valued-Random-Variable of Sigma -> Function of Omega,REAL means :Def2: it is_measurable_on [#]Sigma; correctness proof reconsider X = [#]Sigma as Element of Sigma; chi(X,Omega) is real-valued by MESFUNC2:28; then dom chi(X,Omega) =Omega & rng chi(X,Omega) c= REAL by FUNCT_3:def 3 ,VALUED_0:def 3; then reconsider f= chi(X,Omega) as Function of Omega,REAL by FUNCT_2:2; R_EAL f = chi(X,Omega) & chi(X,Omega) is_measurable_on X by MESFUNC2:29; then f is_measurable_on X; hence thesis; end; end; reserve f,g for Real-Valued-Random-Variable of Sigma; theorem Th18: f+g is Real-Valued-Random-Variable of Sigma proof f is_measurable_on [#]Sigma & g is_measurable_on [#]Sigma by Def2; hence thesis by Def2,MESFUNC6:26; end; definition let Omega,Sigma,f,g; redefine func f+ g -> Real-Valued-Random-Variable of Sigma; correctness by Th18; end; theorem Th19: f-g is Real-Valued-Random-Variable of Sigma proof A1: f is_measurable_on [#]Sigma by Def2; set Y = [#]Sigma; A3: g is_measurable_on Y by Def2; dom g = Y by FUNCT_2:def 1; hence thesis by A1,A3,Def2,MESFUNC6:29; end; definition let Omega,Sigma,f,g; redefine func f-g -> Real-Valued-Random-Variable of Sigma; correctness by Th19; end; theorem Th20: for r be Real holds r(#)f is Real-Valued-Random-Variable of Sigma proof let r be Real; set X = [#]Sigma; A2: f is_measurable_on X by Def2; dom f = X by FUNCT_2:def 1; hence thesis by A2,Def2,MESFUNC6:21; end; definition let Omega,Sigma,f; let r be Real; redefine func r(#)f -> Real-Valued-Random-Variable of Sigma; correctness by Th20; end; theorem Th21: 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; A1: 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 object; assume A2: x in dom ((R_EAL f )(#) (R_EAL g)); hence ((R_EAL f)(#)(R_EAL g)).x =((R_EAL f ).x) * ((R_EAL g).x) by MESFUNC1:def 5 .= (f.x) * ((g.x) qua Real) by EXTREAL1:1 .= (f (#) g).x by A1,A2,VALUED_1:def 4; end; hence thesis by A1,FUNCT_1:2; end; theorem Th22: f(#)g is Real-Valued-Random-Variable of Sigma proof set X = [#]Sigma; A2: f is_measurable_on X by Def2; A3: R_EAL f is_measurable_on X by A2; dom(R_EAL f)=X & dom(R_EAL g)=X by FUNCT_2:def 1; then A4: dom(R_EAL f) /\ dom(R_EAL g)=X; g is_measurable_on [#]Sigma by Def2; then R_EAL g is_measurable_on X; then (R_EAL f)(#)(R_EAL g) is_measurable_on X by A3,A4,MESFUNC7:15; then R_EAL(f(#)g) is_measurable_on X by Th21; then f(#)g is_measurable_on X; hence thesis by Def2; end; definition let Omega,Sigma,f,g; redefine func f(#)g -> Real-Valued-Random-Variable of Sigma; correctness by Th22; end; theorem Th23: for r be Real st 0 <= r & f is nonnegative holds (f to_power r) is Real-Valued-Random-Variable of Sigma proof let r be Real; assume A1: 0 <= r & f is nonnegative; A2: dom f = Omega by FUNCT_2:def 1; rng (f to_power r) c= REAL & dom (f to_power r) = dom f by MESFUN6C:def 4; then A3: (f to_power r) is Function of Omega,REAL by A2,FUNCT_2:2; A5: f is_measurable_on [#]Sigma by Def2; dom f = [#]Sigma by FUNCT_2:def 1; hence thesis by A1,A5,A3,Def2,MESFUN6C:29; end; Lm12: 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 object; assume x in dom (abs f); then (abs f).x = |.f.x qua Complex.| by VALUED_1:def 11; hence 0 <= (abs f).x by COMPLEX1:46; end; hence abs f is nonnegative by MESFUNC6:52; end; theorem Th24: abs f is Real-Valued-Random-Variable of Sigma proof A2: f is_measurable_on [#]Sigma by Def2; dom f = [#]Sigma & R_EAL f is_measurable_on [#]Sigma by A2,FUNCT_2:def 1; then |.R_EAL f.| is_measurable_on [#]Sigma by MESFUNC2:27; then R_EAL abs(f) is_measurable_on [#]Sigma by MESFUNC6:1; then abs(f) is_measurable_on [#]Sigma; hence thesis by Def2; end; definition let Omega,Sigma,f; redefine func abs f -> Real-Valued-Random-Variable of Sigma; correctness by Th24; end; theorem for r be Real st 0 <= r holds (abs(f) to_power r) is Real-Valued-Random-Variable of Sigma proof let r be Real; assume A1: 0 <= r; abs f is nonnegative by Lm12; hence thesis by A1,Th23; end; :: Definition of the Expectations definition let Omega,Sigma,f,P; pred f is_integrable_on P means f is_integrable_on P2M(P); end; definition let Omega,Sigma,P; let f be Real-Valued-Random-Variable of Sigma; assume A1: f is_integrable_on P; func expect (f,P) -> Real equals :Def4: Integral(P2M(P),f); correctness proof f is_integrable_on P2M(P) by A1; then -infty < Integral(P2M(P),f) & Integral(P2M(P),f) < +infty by MESFUNC6:90; then Integral(P2M(P),f) in REAL by XXREAL_0:48; hence thesis; end; end; theorem Th26: f is_integrable_on P & g is_integrable_on P implies expect (f+g, P) = expect (f,P) + expect (g,P) proof set h=f+g; assume A1: f is_integrable_on P & g is_integrable_on P; then A2: Integral(P2M(P),f) =expect (f,P) & Integral(P2M(P),g) =expect (g,P) by Def4 ; A3: f is_integrable_on P2M(P) & g is_integrable_on P2M(P) by A1; then consider E be Element of Sigma such that A4: E = dom f /\ dom g and A5: Integral(P2M(P),f+g) =Integral(P2M(P),f|E)+Integral(P2M(P),g|E) by MESFUNC6:101; A6: dom f = Omega & dom g=Omega by FUNCT_2:def 1; h is_integrable_on P2M(P) by A3,MESFUNC6:100; then h is_integrable_on P; hence expect (h,P) = Integral(P2M(P),f+g) by Def4 .=Integral(P2M(P),f) +Integral(P2M(P),g) by A4,A5,A6 .= expect (f,P)+expect (g,P) by A2,SUPINF_2:1; end; theorem Th27: for r being Real holds f is_integrable_on P implies expect (r(#)f,P) = r* expect (f,P) proof let r be Real; set h=r(#)f; assume A1: f is_integrable_on P; then A2: Integral(P2M(P),f) =expect (f,P) by Def4; A3: f is_integrable_on P2M(P) by A1; then h is_integrable_on P2M(P) by MESFUNC6:102; then h is_integrable_on P; hence expect (h,P) =Integral(P2M(P),r(#)f) by Def4 .=( r)*Integral(P2M(P),f) by A3,MESFUNC6:102 .= r* expect (f,P) by A2,EXTREAL1:1; 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 that A1: f is_integrable_on P and A2: g is_integrable_on P; g is_integrable_on P2M(P) by A2; then (-1)(#)g is_integrable_on P2M(P) by MESFUNC6:102; then (-jj )(#)g is_integrable_on P; hence expect (f-g,P) = expect (f,P) + expect ((-jj)(#)g,P) by A1,Th26 .= expect (f,P) + (-1)*expect (g,P) by A2,Th27 .= 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); consider X be Element of Trivial-SigmaField (Omega) such that A1: dom f = X & f is_measurable_on X by Th8; A2: f is_measurable_on X & dom f = Omega by FUNCT_2:def 1,A1; X = [#]Sigma by A1,A2; hence thesis by Def2,A1; end; theorem Th30: 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); A1: jj in REAL by XREAL_0:def 1; dom X = Omega by FUNCT_2:def 1; then M.(dom X) = jj by PROB_1:def 8; then M.(dom X) < +infty by XXREAL_0:9,A1; then X is_integrable_on M by Lm5,Th6; hence thesis; end; theorem Th31: 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 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}; then Integral(P2M(P),X) = Sum F by Th12; hence thesis by Def4,Th30; 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); X is_integrable_on P & 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 Th13,Th30; hence thesis by Def4; end; theorem Th33: 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); X is_integrable_on P & 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 Th13,Th30; hence thesis by Def4; 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 A1: len G = card (Omega) and A2: s is one-to-one & rng s = Omega and A3: len s = card (Omega) and A4: for n being Nat st n in dom G holds G.n = X.(s.n); set P= Trivial-Probability (Omega); deffunc GF(Nat) = In(X.(s.$1) * P.{s.$1},REAL); consider F being FinSequence of REAL such that A5: len F = len G & for j being Nat st j in dom F holds F.j = GF(j) from FINSEQ_2:sch 1; A6: dom F = dom G by A5,FINSEQ_3:29; reconsider cG = (1/card (Omega))(#)G as FinSequence of REAL by RVSUM_1:145; A7: dom F = dom cG by A6,VALUED_1:def 5; A8: for n being Nat st n in dom cG holds cG.n = F.n proof let n be Nat; assume A9: n in dom cG; dom s = Seg len s by FINSEQ_1:def 3 .= dom F by A1,A3,A5,FINSEQ_1:def 3; then s.n in Omega by A9,PARTFUN1:4,A7; then reconsider A={s.n} as Singleton of Omega by RPR_1:4; A10: P.{s.n} = prob(A) by Def1 .=1/card (Omega) by RPR_1:14; thus cG.n = (1/card (Omega))*G.n by VALUED_1:6 .= (1/card (Omega))*(X.(s.n)) by A4,A6,A9,A7 .= GF(n) by A10 .= F.n by A5,A9,A7; end; A11: for n being Nat st n in dom cG holds cG.n = X.(s.n) * P.{s.n} proof let n be Nat; assume A12: n in dom cG; dom s = Seg len s by FINSEQ_1:def 3 .= dom F by A1,A3,A5,FINSEQ_1:def 3; then s.n in Omega by A12,PARTFUN1:4,A7; then reconsider A={s.n} as Singleton of Omega by RPR_1:4; A13: P.{s.n} = prob(A) by Def1 .=1/card (Omega) by RPR_1:14; thus cG.n = (1/card (Omega))*G.n by VALUED_1:6 .= (1/card (Omega))*(X.(s.n)) by A4,A6,A12,A7 .= GF(n) by A13 .= X.(s.n) * P.{s.n}; end; dom F = dom ((1/card (Omega))(#)G) by A6,VALUED_1:def 5; then A14: (1/card (Omega))(#)G = F by FINSEQ_1:13,A8; A15: len cG = card (Omega) by A1,A5,A14; A16: s is one-to-one by A2; rng s = Omega & len s = card (Omega) by A2,A3; then expect(X,P) = Sum cG by Th31,A15,A16,A11; then expect(X,P) = Sum cG .= Sum(G) /card (Omega) by RVSUM_1:87; hence thesis; end; theorem for Omega be non empty finite set, X be Real-Valued-Random-Variable of Trivial-SigmaField (Omega) 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 A1: len F = card (Omega) and A2: s is one-to-one & rng s = Omega and A3: len s = card (Omega) and A4: for n being Nat st n in dom F holds F.n = X.(s.n) * P.{s.n} and A5: expect(X,P) = Sum F by Th33; deffunc GF(Nat) = In(X.(s.$1),REAL); consider G being FinSequence of REAL such that A6: len G = len F & for j being Nat st j in dom G holds G.j = GF(j) from FINSEQ_2:sch 1; A7: dom F = dom G by A6,FINSEQ_3:29; A8: now let n be Nat; assume A9: n in dom F; dom s= Seg len s by FINSEQ_1:def 3 .= dom F by A1,A3,FINSEQ_1:def 3; then s.n in Omega by A9,PARTFUN1:4; then reconsider A={s.n} as Singleton of Omega by RPR_1:4; A10: P.{s.n} = prob(A) by Def1 .=1/card (Omega) by RPR_1:14; thus ((1/card (Omega))(#)G).n = (1/card (Omega))*G.n by VALUED_1:6 .= (1/card (Omega))*GF(n) by A6,A7,A9 .= (1/card (Omega))*X.(s.n) .= X.(s.n) * P.{s.n} by A10 .= F.n by A4,A9; end; take G,s; dom F = dom ((1/card (Omega))(#)G) by A7,VALUED_1:def 5; then A11:(1/card (Omega))(#)G = F by A8,FINSEQ_1:13; thus len G = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) by A1,A2,A3,A6; thus for n being Nat st n in dom G holds G.n = X.(s.n) proof let n be Nat; assume n in dom G; then G.n = GF(n) by A6; hence thesis; end; thus thesis by A5,RVSUM_1:87,A11; 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 A3: X is_integrable_on P; set PM=P2M(P); set K={t where t is Element of Omega : r <= X.t }; set S = [#]Sigma; A5: X is_measurable_on S by Def2; now let t be object; assume t in S /\ great_eq_dom(X,r); then t in great_eq_dom(X,r) by XBOOLE_0:def 4; then t in dom X & r <= X.t by MESFUNC1:def 14; hence t in K; end; then A6: S /\ great_eq_dom(X,r) c= K; A7: dom X = S by FUNCT_2:def 1; now let x be object; assume x in K; then A8: ex t be Element of Omega st x=t & r <= X.t; then x in great_eq_dom(X,r) by A7,MESFUNC1:def 14; hence x in S /\ great_eq_dom(X,r) by A8,XBOOLE_0:def 4; end; then K c= S /\ great_eq_dom(X,r); then S /\ great_eq_dom(X,r) = K by A6; then reconsider K as Element of Sigma by A5,A7,MESFUNC6:13; Integral(PM,X|K) <= Integral(PM,X|S) by A2,A5,A7,MESFUNC6:87; then A9: Integral(PM,X|K) <= Integral(PM,X); expect (X,P)=Integral(PM,X) by A3,Def4; then reconsider IX=Integral(PM,X) as Element of REAL by XREAL_0:def 1; reconsider PMK=PM.K as Element of REAL by XXREAL_0:14; A10: 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; A11: jj in REAL by XREAL_0:def 1; PM.K <= jj by PROB_1:35; then A12: PM.K < +infty by XXREAL_0:2,9,A11; X is_integrable_on P2M(P) by A3; then (r)*(PM.K) <= Integral(PM,X|K) by A7,A12,A10,Th2; then r*PMK <= Integral(PM,X|K) by EXTREAL1:1; then r*PMK <= Integral(PM,X) by A9,XXREAL_0:2; then (r*PMK)/r <= IX /r by A1,XREAL_1:72; then PMK <= IX /r by A1,XCMPLX_1:89; hence thesis by A3,Def4; end;