:: Probability on Finite Set and Real Valued Random Variables :: by Hiroyuki Okazaki and Yasunari Shidama :: :: Received March 17, 2009 :: Copyright (c) 2009 Association of Mizar Users environ vocabularies RANDOM_1, PARTFUN1, MEASURE1, FINSEQ_1, RELAT_1, ABSVALUE, FUNCT_1, ORDINAL2, LATTICES, RPR_1, SUBSET_1, CARD_1, COMPLEX1, SEQ_1, SEQ_2, MEASURE6, BOOLE, ARYTM, ARYTM_1, POWER, MESFUNC1, TARSKI, ARYTM_3, RLVECT_1, GROUP_1, PROB_1, INTEGRA1, MESFUNC2, MESFUNC3, MESFUNC5, SUPINF_1, SUPINF_2, FUNCT_3, RFUNCT_3, VALUED_0, PROB_4, FINSET_1, UPROOTS; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FINSET_1, CARD_1, NUMBERS, XREAL_0, XXREAL_0, REAL_1, COMPLEX1, XXREAL_2, FUNCT_1, RELSET_1, PARTFUN1, VALUED_1, FINSEQ_1, RFUNCT_3, FUNCT_2, NAT_1, SUPINF_2, SEQ_1, SEQ_2, RPR_1, PROB_1, PROB_4, MEASURE1, EXTREAL1, MESFUNC1, MESFUNC3, CONVFUN1, MEASURE6, MESFUNC5, MESFUNC6, MESFUNC2, RVSUM_1, UPROOTS, MESFUN6C; constructors REAL_1, RPR_1, NAT_3, EXTREAL1, SEQ_1, POWER, RVSUM_1, MESFUNC6, MESFUNC3, MESFUNC5, MEASURE6, MESFUNC2, CONVFUN1, BINOP_2, PARTFUN3, INTEGRA2, PROB_4, SUPINF_1, UPROOTS, MESFUN6C, MESFUNC1, DOMAIN_1, RELSET_1; registrations SUBSET_1, NAT_1, XREAL_0, XXREAL_0, TOPREAL6, MEMBERED, ORDINAL1, FINSEQ_1, MEASURE1, FUNCT_2, RELAT_1, SEQ_4, FINSET_1, NUMBERS, XCMPLX_0, VALUED_0, VALUED_1, UPROOTS; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions TARSKI, RPR_1, SUBSET_1, FINSEQ_1, MESFUNC1, MEASURE6, MESFUNC5, MESFUNC6, XCMPLX_0, PROB_1, PROB_4, VALUED_1, XBOOLE_0, XXREAL_3; theorems ABSVALUE, TARSKI, PARTFUN1, FUNCT_1, NUMBERS, SUPINF_2, EXTREAL1, RPR_1, MESFUNC1, FINSEQ_1, XBOOLE_0, SEQM_3, RVSUM_1, XBOOLE_1, XCMPLX_1, MESFUNC2, MESFUNC3, XREAL_1, COMPLEX1, XXREAL_0, RFUNCT_3, MESFUNC5, PROB_1, NAT_1, RELAT_1, FUNCT_3, ZFMISC_1, FUNCT_2, MEASURE1, INTEGRA5, MESFUNC4, MESFUNC6, ORDINAL1, SEQ_2, CARD_FIN, MESFUNC7, VALUED_0, VALUED_1, UPROOTS, ABCMIZ_1, RCOMP_1, MESFUN6C, FINSEQ_3, XXREAL_3; schemes FINSEQ_1, FUNCT_2, FINSEQ_2; begin theorem LMMarkov1: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, E be Element of S, a be Real st f is_integrable_on M & E c= dom f & M.E < +infty & (for x be Element of X st x in E holds a <= f.x) holds (R_EAL a)*(M.E) <= Integral(M,f|E) proof let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, E be Element of S, a be Real; assume that A1: f is_integrable_on M and A2: E c= dom f and A3: M.E < +infty and A4: for x be Element of X st x in E holds a <= f.x; set C = chi(E,X); A5: f|E is_integrable_on M by A1,MESFUNC5:103; chi(E,X) is_integrable_on M by A3,MESFUNC7:24; then A6: C|E is_integrable_on M by MESFUNC5:103; then A7: a(#)(C|E) is_integrable_on M by MESFUNC5:116; for x be Element of X st x in dom(a(#)(C|E)) holds (a(#)(C|E)).x <= (f|E).x proof let x be Element of X; assume A8: x in dom(a(#)(C|E));then A9: x in dom(C|E) by MESFUNC1:def 6; then x in dom C /\ E by RELAT_1:90;then A10: x in dom chi(E,X) & x in E by XBOOLE_0:def 4; then a <= f.x by A4;then A11: a <= (f|E).x by A10,FUNCT_1:72; (a(#)(C|E)).x = R_EAL a * (C|E).x by A8,MESFUNC1:def 6 .= R_EAL a * C.x by A9,FUNCT_1:70 .= R_EAL a * 1.by A10,FUNCT_3:def 3; hence thesis by A11,XXREAL_3:92; end; then (f|E) - (a(#)(C|E)) is nonnegative by MESFUNC7:1; then consider E1 be Element of S such that A12: E1 = dom(f|E) /\ dom(a(#)(C|E)) & Integral(M,(a(#)(C|E))|E1) <= Integral(M,(f|E)|E1) by A5,A7,MESFUNC7:3; dom(f|E) = dom f /\ E by RELAT_1:90; then A13: dom(f|E) = E by A2,XBOOLE_1:28; dom(a(#)(C|E)) = dom(C|E) by MESFUNC1:def 6; then dom(a(#)(C|E)) = dom C /\ E by RELAT_1:90; then dom(a(#)(C|E)) = X /\ E by FUNCT_3:def 3; then A14: dom(a(#)(C|E)) = E by XBOOLE_1:28; A20: (a(#)(C|E))|E1 = a(#)(C|E) & (f|E)|E1 = f|E by A12,A13,A14,RELAT_1:98; E = E/\E; then Integral(M,C|E) = M.E by A3,MESFUNC7:25; hence thesis by A6,A12,A20,MESFUNC5:116; end; theorem LMMarkov2: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,REAL, E be Element of S, a be Real st f is_integrable_on M & E c= dom f & M.E < +infty & (for x be Element of X st x in E holds a <= f.x) holds (R_EAL a)*M.E <= Integral(M,f|E) proof let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,REAL, E be Element of S, a be Real; assume f is_integrable_on M; then R_EAL f is_integrable_on M by MESFUNC6:def 9; hence thesis by LMMarkov1; end; theorem LMMarkov3: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, E be Element of S, a be Real st f is_integrable_on M & E c= dom f & M.E < +infty & (for x be Element of X st x in E holds f.x <= a) holds Integral(M,f|E) <= (R_EAL a)*M.E proof let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, E be Element of S, a be Real; assume that A1: f is_integrable_on M and A2: E c= dom f and A3: M.E < +infty and A4: for x be Element of X st x in E holds f.x <=a; set C = chi(E,X); A5: f|E is_integrable_on M by A1,MESFUNC5:103; chi(E,X) is_integrable_on M by A3,MESFUNC7:24; then A6: C|E is_integrable_on M by MESFUNC5:103; then A7: a(#)(C|E) is_integrable_on M by MESFUNC5:116; dom(f|E) = dom f /\ E by RELAT_1:90; then A13: dom(f|E) = E by A2,XBOOLE_1:28; dom(a(#)(C|E)) = dom(C|E) by MESFUNC1:def 6; then dom(a(#)(C|E)) = dom C /\ E by RELAT_1:90; then dom(a(#)(C|E)) = X /\ E by FUNCT_3:def 3; then A14: dom(a(#)(C|E)) = E by XBOOLE_1:28; for x be Element of X st x in dom(f|E) holds (f|E).x <= (a(#)(C|E)).x proof let x be Element of X; assume A8: x in dom(f|E); then A16: x in dom(C|E) by A13,A14,MESFUNC1:def 6; then x in dom C /\ E by RELAT_1:90; then A10: x in dom chi(E,X) & x in E by XBOOLE_0:def 4; then f.x <= a by A4; then A11: (f|E).x <=a by A10,FUNCT_1:72; (a(#)(C|E)).x = R_EAL a * (C|E).x by A13,A14,A8,MESFUNC1:def 6 .= R_EAL a * C.x by A16,FUNCT_1:70 .= R_EAL a * 1.by A10,FUNCT_3:def 3; hence thesis by A11,XXREAL_3:92; end; then (a(#)(C|E))-(f|E) is nonnegative by MESFUNC7:1; then consider E1 be Element of S such that A12: E1 = dom(f|E) /\ dom(a(#)(C|E)) & Integral(M,(f|E)|E1) <= Integral(M,(a(#)(C|E))|E1) by A5,A7,MESFUNC7:3; dom(f|E) = dom f /\ E by RELAT_1:90; then A13: dom(f|E) = E by A2,XBOOLE_1:28; dom(a(#)(C|E)) = dom(C|E) by MESFUNC1:def 6; then dom(a(#)(C|E)) = dom C /\ E by RELAT_1:90; then dom(a(#)(C|E)) = X /\ E by FUNCT_3:def 3; then A14: dom(a(#)(C|E)) = E by XBOOLE_1:28; A20: (a(#)(C|E))|E1 = a(#)(C|E) & (f|E)|E1 = f|E by A12,A13,A14,RELAT_1:98; E = E/\E; then Integral(M,C|E) = M.E by A3,MESFUNC7:25; hence thesis by A6,A12,A20,MESFUNC5:116; end; theorem for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,REAL, E be Element of S, a be Real st f is_integrable_on M & E c= dom f & M.E < +infty & (for x be Element of X st x in E holds f.x <= a) holds Integral(M,f|E) <=(R_EAL a)*M.E proof let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,REAL, E be Element of S, a be Real; assume f is_integrable_on M; then R_EAL f is_integrable_on M by MESFUNC6:def 9; hence thesis by LMMarkov3; end; :: Integral of real valued simple functions MES43: for X be non empty set,S be SigmaField of X,f be PartFunc of X,REAL, M be sigma_Measure of S,F be Finite_Sep_Sequence of S, a be FinSequence of REAL, x be FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & dom f = union rng F & dom F = dom a & (for n be Nat st n in dom F for x be set st x in F.n holds f.x=a.n) & dom x = dom F & (for n be Nat st n in dom x holds x.n=R_EAL(a.n)*(M*F).n) holds Integral(M,f)=Sum(x) proof let X be non empty set,S be SigmaField of X,f be PartFunc of X,REAL, M be sigma_Measure of S, F be Finite_Sep_Sequence of S, a be FinSequence of REAL, x be FinSequence of ExtREAL; assume that A1: f is_simple_func_in S & dom f <> {} and A2: f is nonnegative and A3: dom f = union rng F & dom F = dom a & (for n be Nat st n in dom F for x be set st x in F.n holds f.x=a.n ) & dom x = dom F and A4: for n be Nat st n in dom x holds x.n = R_EAL(a.n)*(M*F).n; B1: R_EAL f is_simple_func_in S & dom(R_EAL f) <> {} by A1,MESFUNC6:49; B2: for x be set st x in dom(R_EAL f) holds 0 <=(R_EAL f).x by MESFUNC6:51,A2; reconsider a0=a as FinSequence of ExtREAL by MESFUNC3:11; B3: F,a0 are_Re-presentation_of R_EAL f by MESFUNC3:def 1,A3; B5: for n be Nat st n in dom x holds x.n = a0.n*(M*F).n proof let n be Nat; assume n in dom x;then x.n=R_EAL(a.n)*(M*F).n by A4; hence thesis; end; thus Integral(M,f) = integral'(M,R_EAL f) by A2,A1,MESFUNC6:83 .= integral(X,S,M,R_EAL f) by A1,MESFUNC5:def 14 .= Sum(x) by A3,B1,B2,B3,B5,MESFUNC4:3; end; MES33: for X be non empty set,S be SigmaField of X, f be PartFunc of X,REAL st f is_simple_func_in S holds ex F be Finite_Sep_Sequence of S,a be FinSequence of REAL st dom f = union rng F & dom F= dom a & (for n be Nat st n in dom F for x be set st x in F.n holds f.x = a.n) proof let X be non empty set; let S be SigmaField of X; let f be PartFunc of X,REAL; assume f is_simple_func_in S;then consider F be Finite_Sep_Sequence of S such that A1: dom f = union rng F and A2: for n being Nat,x,y being Element of X st n in dom F & x in F.n & y in F.n holds f.x = f.y by MESFUNC6:def 7; defpred P[Nat,Element of REAL] means for x be set st x in F.$1 holds $2 = f.x; A3: for k be Nat st k in Seg len F ex y be Element of REAL st P[k,y] proof let k be Nat; assume k in Seg len F;then A4: k in dom F by FINSEQ_1:def 3;then A5: F.k in rng F by FUNCT_1:12; per cases; suppose A6: F.k = {}; take y = 0; thus thesis by A6; end; suppose F.k <> {};then consider x1 be set such that A7: x1 in F.k by XBOOLE_0:def 1; take y = f.x1; rng F c= bool X by XBOOLE_1:1; hence thesis by A2,A5,A4,A7; end; end; consider a be FinSequence of REAL such that A10: dom a = Seg len F & for k be Nat st k in Seg len F holds P[k,a.k] from FINSEQ_1:sch 5(A3); A11: for n be Nat st n in dom F for x be set st x in F.n holds a.n = f.x proof let n be Nat; assume n in dom F;then n in Seg len F by FINSEQ_1:def 3; hence thesis by A10; end; take F,a; thus thesis by A1,A10,A11,FINSEQ_1:def 3; end; Lm9C0: for X be non empty set,S be SigmaField of X, f be PartFunc of X,REAL st f is_simple_func_in S holds rng f is bounded proof let X be non empty set,S be SigmaField of X, f be PartFunc of X,REAL; assume f is_simple_func_in S;then consider F be Finite_Sep_Sequence of S,a be FinSequence of REAL such that A1: dom f = union rng F & dom F = dom a & for n be Nat st n in dom F for x be set st x in F.n holds f.x = a.n by MES33; rng f c= rng a proof let y be set; assume y in rng f; then consider x be set such that P01: x in dom(f) & y = f.x by FUNCT_1:def 5; consider z be set such that P02: x in z & z in rng F by A1,P01,TARSKI:def 4; consider n be set such that P03: n in dom F & z= F.n by P02,FUNCT_1:def 5; f.x = a.n by A1,P03,P02; hence y in rng a by P03,A1,FUNCT_1:def 5,P01; end; hence thesis by RCOMP_1:28; end; Lm9B0: for X be non empty set,S be SigmaField of X, M being sigma_Measure of S,f be PartFunc of X,REAL st dom f <> {} & rng f is bounded & M.(dom f) < +infty & ex E be Element of S st E = dom f & f is_measurable_on E holds f is_integrable_on M proof let X be non empty set,S be SigmaField of X, M being sigma_Measure of S,f be PartFunc of X,REAL; assume that A0: dom f <> {} & rng f is bounded and A1: M.(dom f) < +infty and A2: ex E be Element of S st E = dom f & f is_measurable_on E; consider E be Element of S such that A3: E = dom f & f is_measurable_on E by A2; A4: rng(R_EAL f) is non empty Subset of ExtREAL by RELAT_1:65,A0; B1: R_EAL f is_measurable_on E by A3,MESFUNC6:def 6; B2: chi(E,X) is_integrable_on M by A1,A3,MESFUNC7:24; B4: chi(E,X) is real-valued by MESFUNC2:31; B51: dom (R_EAL f) /\ dom(chi(E,X)) = E /\ X by A3,FUNCT_3:def 3; dom (R_EAL f) /\ dom(chi(E,X)) = E by B51,XBOOLE_1:28;then B6: ((R_EAL f)(#)(chi(E,X)) )|E is_integrable_on M by A4,A0,B1,B2,B4,MESFUNC7:17; B7: dom((R_EAL f)(#)(chi(E,X))) = dom (R_EAL f) /\ dom(chi(E,X)) by MESFUNC1:def 5 .= E by B51,XBOOLE_1:28; then B8: dom(( (R_EAL f)(#)(chi(E,X)) )|E) = dom f by A3,RELAT_1:91; now let x be set; assume AA3: x in dom f; P02: ( (R_EAL f)(#)(chi(E,X)) ).x = (R_EAL f).x * (chi(E,X)).x by MESFUNC1:def 5,B7,A3,AA3; ( (R_EAL f)(#)(chi(E,X)) ).x = (R_EAL f).x * R_EAL(1) by P02,A3,AA3,FUNCT_3:def 3 .= f.x by XXREAL_3:92; hence (( (R_EAL f)(#)(chi(E,X)) )|E).x = f.x by B7,RELAT_1:97; end;then ( (R_EAL f)(#)(chi(E,X)) )|E = f by B8,FUNCT_1:9; hence thesis by B6,MESFUNC6:def 9; end; Lm9A0: for X be non empty set,S be SigmaField of X, M being sigma_Measure of S,f be PartFunc of X,REAL st f is_simple_func_in S & dom f <> {} & (dom f) in S & M.(dom f) < +infty holds f is_integrable_on M proof let X be non empty set,S be SigmaField of X, M be sigma_Measure of S,f be PartFunc of X,REAL; assume A1: f is_simple_func_in S; rng f is bounded by Lm9C0,A1; hence thesis by Lm9B0,A1,MESFUNC6:50; end; begin :: Trivial SigmaField and Probability on Finite set reserve Omega for non empty set; reserve m,n,k for Element of NAT; reserve x,y for set; reserve r,r1,r2,r3 for Real; reserve seq,seq1 for Real_Sequence; reserve Sigma for SigmaField of Omega; reserve ASeq,BSeq for SetSequence of Sigma; reserve P,P1,P2 for Probability of Sigma; reserve A,B,C,A1,A2,A3 for Event of Sigma; reserve E for finite non empty set; notation let E be non empty set; synonym Trivial-SigmaField (E) for bool E; end; definition let E be non empty set; redefine func Trivial-SigmaField (E) -> SigmaField of E; correctness by PROB_1:76; end; Lm6A: for Omega be non empty finite set, f be PartFunc of Omega,REAL holds ex F be Finite_Sep_Sequence of Trivial-SigmaField (Omega) st dom f = union (rng F) & dom F = dom canFS dom f & (for k be Nat st k in dom F holds F.k={(canFS dom f).k}) & for n being Nat for x,y being Element of Omega st n in dom F & x in F.n & y in F.n holds f.x = f.y proof let Omega be non empty finite set, f be PartFunc of Omega,REAL; set Sigma =Trivial-SigmaField (Omega); set D=dom f; defpred P[Nat,set] means $2={(canFS(D)).$1 }; set L= len (canFS(D)); P1:for k be Nat st k in Seg L ex x being Element of bool Omega st P[k,x] proof let k be Nat; assume k in Seg L; then k in dom canFS(D) by FINSEQ_1:def 3; then (canFS(D)).k in rng canFS(D) by FUNCT_1:12;then PPPP1: (canFS(D)).k in D; take {(canFS(D)).k }; thus thesis by PPPP1,ZFMISC_1:37; end; consider F being FinSequence of bool Omega such that P2: dom F = Seg L & for k be Nat st k in Seg L holds P[k,F.k] from FINSEQ_1:sch 5(P1); now let i,j be Nat; assume A1: i in dom F & j in dom F & i <> j; A4: i in dom (canFS(D)) & j in dom (canFS(D)) by FINSEQ_1:def 3,A1,P2; AA3: (canFS(D)).i <> (canFS(D)).j by A1,A4,FUNCT_1:def 8; F.i = {(canFS(D)).i } & F.j = {(canFS(D)).j } by A1,P2; hence F.i misses F.j by AA3,ZFMISC_1:17; end; then reconsider F as Finite_Sep_Sequence of Sigma by MESFUNC3:4; take F; PP3: union rng F = rng canFS(D) proof now let x be set; assume x in union rng F; then consider y be set such that A2: x in y & y in rng F by TARSKI:def 4; consider n be set such that A3: n in dom F & y=F.n by A2,FUNCT_1:def 5; reconsider n as Element of NAT by A3; F.n = {(canFS(D)).n } by A3,P2;then A5:x= (canFS(D)).n by A2,A3,TARSKI:def 1; n in dom (canFS(D)) by P2,A3,FINSEQ_1:def 3; hence x in rng canFS(D) by FUNCT_1:def 5,A5; end;then A4:union rng F c= rng canFS(D) by TARSKI:def 3; now let x be set; assume x in rng canFS(D);then consider n be set such that A5: n in dom (canFS(D)) & x=(canFS(D)).n by FUNCT_1:def 5; A4: n in Seg L by A5,FINSEQ_1:def 3; reconsider n as Element of NAT by A5; A3: n in dom F by P2,A5,FINSEQ_1:def 3; x in {(canFS(D)).n} by A5,TARSKI:def 1;then A2: x in F.n by P2,A4; F.n in rng F by A3,FUNCT_1:def 5; hence x in union rng F by A2,TARSKI:def 4; end; then rng canFS(D) c= union rng F by TARSKI:def 3; hence thesis by XBOOLE_0:def 10,A4; end; for n being Nat for x,y being Element of Omega st n in dom F & x in F.n & y in F.n holds f.x = f.y proof let n be Nat; let x,y be Element of Omega; assume AS1: n in dom F & x in F.n & y in F.n; P41: F.n = {(canFS(D)).n} by P2,AS1; hence f.x =f.((canFS(D)).n) by AS1,TARSKI:def 1 .=f.y by P41,AS1,TARSKI:def 1; end; hence thesis by FINSEQ_1:def 3,P2,PP3,FUNCT_2:def 3; end; theorem for Omega be non empty finite set, f be PartFunc of Omega,REAL holds ex F be Finite_Sep_Sequence of Trivial-SigmaField (Omega), s being FinSequence of (dom f) st dom f = union (rng F) & dom F = dom (s) & s is one-to-one & rng s = dom f & len s = card (dom f) & (for k be Nat st k in dom F holds F.k={s.k} ) & for n being Nat for x,y being Element of Omega st n in dom F & x in F.n & y in F.n holds f.x = f.y proof let Omega be non empty finite set, f be PartFunc of Omega,REAL; set Sigma = Trivial-SigmaField (Omega); set D = dom f; consider F be Finite_Sep_Sequence of Sigma such that P1: dom f = union (rng F) & dom F = dom (canFS(D)) & (for k be Nat st k in dom F holds F.k={(canFS(D)).k} ) & for n being Nat for x,y being Element of Omega st n in dom F & x in F.n & y in F.n holds f.x = f.y by Lm6A; set s=canFS(D); dom f = union (rng F) & dom F = dom (s) & s is one-to-one & rng s = dom f & len s = card (dom f) & (for k be Nat st k in dom F holds F.k={s.k}) & for n being Nat for x,y being Element of Omega st n in dom F & x in F.n & y in F.n holds f.x = f.y by P1,FUNCT_2:def 3,UPROOTS:5; hence thesis; end; theorem Lm6: for Omega be non empty finite set, f be PartFunc of Omega,REAL holds f is_simple_func_in Trivial-SigmaField (Omega) & dom f is Element of Trivial-SigmaField (Omega) proof let Omega be non empty finite set, f be PartFunc of Omega,REAL; set Sigma = Trivial-SigmaField (Omega),D = dom f; consider F be Finite_Sep_Sequence of Sigma such that P1: dom f = union (rng F) & dom F = dom (canFS(D)) & (for k be Nat st k in dom F holds F.k={(canFS(D)).k} ) & for n being Nat for x,y being Element of Omega st n in dom F & x in F.n & y in F.n holds f.x = f.y by Lm6A; thus thesis by MESFUNC6:def 7,P1; end; theorem for Omega be non empty finite set, M being sigma_Measure of Trivial-SigmaField (Omega), f be PartFunc of Omega,REAL st dom f <> {} & M.(dom f) < +infty holds f is_integrable_on M by Lm9A0,Lm6; Lm9A2: for Omega be non empty set, Sigma be SigmaField of Omega, M being sigma_Measure of Sigma, A,B be set st A in Sigma & B in Sigma & A c= B & M.B < +infty holds M.A in REAL proof let Omega be non empty set, Sigma be SigmaField of Omega, M be sigma_Measure of Sigma, A,B be set; assume AS: A in Sigma & B in Sigma & A c= B & M.B < +infty; M.A <> -infty & M.A <> +infty by MEASURE1:62,AS,MEASURE1:def 4; hence thesis by XXREAL_0:14; end; LmX1: for Omega be non empty finite set, f be PartFunc of Omega,REAL holds f*canFS dom f is FinSequence of REAL proof let Omega be non empty finite set, f be PartFunc of Omega,REAL; rng canFS dom f c= dom f;then X: f*canFS dom f is FinSequence by FINSEQ_1:20; rng(f*canFS dom f) c= REAL; hence f*canFS dom f is FinSequence of REAL by FINSEQ_1:def 4,X; end; LmX2: for Omega be non empty finite set, f be PartFunc of Omega,REAL holds dom(f*canFS dom f) = dom canFS dom f proof let Omega be non empty finite set, f be PartFunc of Omega,REAL; rng canFS dom f c= dom f; hence dom(f*canFS dom f) = dom canFS dom f by RELAT_1:46; end; theorem Lm7: for Omega be non empty finite set, f be PartFunc of Omega,REAL ex X be Element of Trivial-SigmaField (Omega) st dom f = X & f is_measurable_on X proof let Omega be non empty finite set, f be PartFunc of Omega,REAL; set Sigma = Trivial-SigmaField (Omega); reconsider X = dom f as Element of Sigma; take X; thus thesis by Lm6,MESFUNC6:50; end; Lm9A: for Omega be non empty finite set, M being sigma_Measure of Trivial-SigmaField (Omega), f be Function of Omega,REAL st M.Omega < +infty holds ex x being FinSequence of ExtREAL st len x = card (Omega) & (for n being Nat st n in dom x holds x.n = R_EAL (f.((canFS(Omega)).n)) * M.{(canFS(Omega)).n}) & Integral(M,f) = Sum x proof let Omega be non empty finite set, M being sigma_Measure of Trivial-SigmaField (Omega), f be Function of Omega,REAL; assume AS: M.Omega < +infty; set Sigma= Trivial-SigmaField (Omega),D =dom f; consider F be Finite_Sep_Sequence of Sigma such that P1: dom f = union (rng F) & dom F = dom (canFS(D)) & (for k be Nat st k in dom F holds F.k={(canFS(D)).k} ) & for n being Nat for x,y being Element of Omega st n in dom F & x in F.n & y in F.n holds f.x = f.y by Lm6A; set fp=max+(f); set fm=max-(f); XD0: dom f =Omega by FUNCT_2:def 1; XDp: dom fp=dom f by RFUNCT_3:def 10; XDm:dom fm=dom f by RFUNCT_3:def 11; set Dp = dom fp; consider Fp be Finite_Sep_Sequence of Sigma such that Q1: dom fp = union (rng Fp) & dom Fp = dom (canFS(Dp)) & (for k be Nat st k in dom Fp holds Fp.k={(canFS(Dp)).k} ) & for n being Nat for x,y being Element of Omega st n in dom Fp & x in Fp.n & y in Fp.n holds fp.x = fp.y by Lm6A; set Dm = dom fm; consider Fm be Finite_Sep_Sequence of Sigma such that R1: dom fm = union (rng Fm) & dom Fm = dom (canFS(Dm)) & (for k be Nat st k in dom Fm holds Fm.k={(canFS(Dm)).k} ) & for n being Nat for x,y being Element of Omega st n in dom Fm & x in Fm.n & y in Fm.n holds fm.x = fm.y by Lm6A; FPP: fp is Function of Omega,REAL by XD0,XDp,FUNCT_2:def 1; A1: fp is_simple_func_in Sigma by Lm6; A2: fp is nonnegative by MESFUNC6:61; FMM: fm is Function of Omega,REAL by XD0,XDm,FUNCT_2:def 1; B1: fm is_simple_func_in Sigma by Lm6; B2: fm is nonnegative by MESFUNC6:61; XXX1: Dp=D & Dm=D by RFUNCT_3:def 10,RFUNCT_3:def 11; XXX2: dom Fp=dom F &dom Fm= dom F by R1,Q1,P1,RFUNCT_3:def 10,RFUNCT_3:def 11; set L=len F; reconsider a = f*canFS D as FinSequence of REAL by LmX1; defpred PX[ Nat,set ] means $2=R_EAL (a.$1) *(M*F).$1; A1X: for k being Nat st k in Seg L holds ex x being Element of ExtREAL st PX[k,x]; consider x being FinSequence of ExtREAL such that C30: dom x = Seg L & for k being Nat st k in Seg L holds PX[k,x.k] from FINSEQ_1:sch 5(A1X); C3: dom x = dom F & for n be Nat st n in dom x holds x.n=R_EAL (a.n) *(M*F).n by C30,FINSEQ_1:def 3; take x; reconsider ap = fp*canFS Dp as FinSequence of REAL by LmX1; defpred Pp[ Nat,set ] means $2=R_EAL (ap.$1) *(M*Fp).$1; A1P: for k being Nat st k in Seg L holds ex x being Element of ExtREAL st Pp[k,x]; consider xp being FinSequence of ExtREAL such that A30: dom xp = Seg L & for k being Nat st k in Seg L holds Pp[k,xp.k] from FINSEQ_1:sch 5(A1P); A3: dom xp = dom Fp & for n be Nat st n in dom xp holds xp.n=R_EAL (ap.n) *(M*Fp).n by A30,FINSEQ_1:def 3,XXX2; reconsider am = fm*canFS Dm as FinSequence of REAL by LmX1; defpred Pm[Nat,set] means $2=R_EAL (am.$1) *(M*Fm).$1; B1P: for k being Nat st k in Seg L holds ex x being Element of ExtREAL st Pm[k,x]; consider xm being FinSequence of ExtREAL such that B30: dom xm = Seg L & for k being Nat st k in Seg L holds Pm[k,xm.k] from FINSEQ_1:sch 5(B1P); B3: dom xm = dom Fm & for n be Nat st n in dom xm holds xm.n=R_EAL (am.n) *(M*Fm).n by B30,FINSEQ_1:def 3,XXX2; UU1: dom Fp=dom ap by LmX2,Q1; for n be Nat st n in dom Fp for x be set st x in Fp.n holds fp.x=ap.n proof let n be Nat such that Z: n in dom Fp; let x be set; assume x in Fp.n; then x in {(canFS(Dp)).n} by Z,Q1; then x = (canFS(Dp)).n by TARSKI:def 1; hence fp.x=ap.n by Z,UU1,FUNCT_1:22; end; then A5:Integral(M,fp)=Sum(xp) by MES43,A1,A2,A3,Q1,XDp,UU1; X2:dom fp = Omega by XD0,RFUNCT_3:def 10; K2: fp is_integrable_on M by X2,Lm9A0,Lm6,AS; X3: dom fm = Omega by XD0,RFUNCT_3:def 11; K3: fm is_integrable_on M by X3,Lm9A0,Lm6,AS; M.(dom ((-1)(#)fm)) < +infty by AS,FUNCT_2:def 1,FMM;then K5: (-1)(#)fm is_integrable_on M by FMM,Lm9A0,Lm6; consider E be Element of Sigma such that K6: E = (dom fp) /\ dom ((-1)(#)fm) & Integral(M,fp+(-1)(#)fm) =Integral(M,fp|E)+Integral(M,((-1)(#)fm)|E) by K2,K5,MESFUNC6:101; K8: dom ((-1)(#)fm) =dom fm by VALUED_1:def 5 .=Omega by XDm,FUNCT_2:def 1; K9: E = Omega /\ Omega by XDp,FUNCT_2:def 1,K8,K6 .= Omega; K10: R_EAL(-1)*Integral(M,fm) =(-R_EAL(1)) *Integral(M,fm) by SUPINF_2:3 .= -(R_EAL(1)*Integral(M,fm) ) by XXREAL_3:103 .=-Integral(M,fm) by XXREAL_3:92; P6: ((-1)(#)fm)|E = (-1)(#)fm by FMM,K9,FUNCT_2:40; P7: Integral(M,fp+(-1)(#)fm) =Integral(M,fp) +Integral(M,(-1)(#)fm) by FPP,K9,FUNCT_2:40,P6,K6 .=Integral(M,fp) +-Integral(M,fm) by K10,MESFUNC6:102,K3; CFSD: for n be Nat st n in dom canFS(Omega) holds M.{(canFS(Omega)).n} in REAL proof let n be Nat; assume n in dom canFS(Omega);then (canFS(Omega)).n in rng canFS(Omega) by FUNCT_1:12;then B1: {(canFS(Omega)).n } c= Omega by ZFMISC_1:37; Omega in Sigma by MEASURE1:21; hence M.({(canFS(Omega)).n }) in REAL by Lm9A2,B1,AS; end; C7: for n being Nat st n in dom x holds x.n = R_EAL (f.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} proof let n be Nat; assume C71: n in dom x; C73:f.((canFS(D)).n) =a.n by C3,P1,C71,FUNCT_1:23; C74: (M*F).n =M.(F.n) by FUNCT_1:23,C3,C71 .= M.{(canFS(Omega)).n} by XD0,P1,C3,C71; thus x.n=R_EAL (a.n) *(M*F).n by C30,C71 .= R_EAL (f.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} by C73,C74,FUNCT_2:def 1; end; x is FinSequence of REAL proof let y be set; assume y in rng x;then consider n be Element of NAT such that C71: n in dom x & y=x.n by PARTFUN1:26; reconsider w=f.((canFS(Omega)).n) as Element of REAL; reconsider z=M.{(canFS(Omega)).n} as Element of REAL by CFSD,C3,P1,C71,XD0; x.n = R_EAL (f.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} by C7,C71 .= w*z by EXTREAL1:13; hence y in REAL by C71; end;then reconsider x1=x as FinSequence of REAL; XB7: for n being Nat st n in dom xp holds xp.n = R_EAL (fp.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} proof let n be Nat; assume C71: n in dom xp; C73:fp.((canFS(D)).n) =ap.n by A3,Q1,C71,FUNCT_1:23,XXX1; C74: (M*Fp).n =M.(Fp.n) by FUNCT_1:23,A3,C71 .= M.{(canFS(Omega)).n} by XD0,XXX1,A3,Q1,C71; thus xp.n=R_EAL (ap.n) *(M*Fp).n by A30,C71 .= R_EAL (fp.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} by C73,C74,FUNCT_2:def 1; end; xp is FinSequence of REAL proof now let y be set; assume y in rng xp; then consider n be Element of NAT such that C71: n in dom xp & y=xp.n by PARTFUN1:26; reconsider w=fp.((canFS(Omega)).n) as Element of REAL; reconsider z=M.{(canFS(Omega)).n} as Element of REAL by CFSD,XXX1,A3,Q1,C71,XD0; xp.n = R_EAL (fp.((canFS(Omega)).n)) * M.{(canFS(Omega)).n} by XB7,C71 .= w*z by EXTREAL1:13; hence y in REAL by C71; end; hence rng xp c= REAL by TARSKI:def 3; end;then reconsider xp1=xp as FinSequence of REAL; XA7: for n being Nat st n in dom xm holds xm.n = R_EAL (fm.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} proof let n be Nat; assume C71: n in dom xm; C74: (M*Fm).n =M.(Fm.n) by FUNCT_1:23,B3,C71 .= M.{(canFS(Omega)).n} by XD0,XXX1,B3,R1,C71; thus xm.n=R_EAL (am.n) *(M*Fm).n by B30,C71 .= R_EAL (fm.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} by B3,R1,C71,C74,FUNCT_1:23,X3; end; xm is FinSequence of REAL proof now let y be set; assume y in rng xm; then consider n be Element of NAT such that C71: n in dom xm & y=xm.n by PARTFUN1:26; reconsider w=fm.((canFS(Omega)).n) as Element of REAL; reconsider z=M.{(canFS(Omega)).n} as Element of REAL by CFSD,XXX1,B3,R1,C71,XD0; xm.n = R_EAL (fm.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} by XA7,C71 .= w*z by EXTREAL1:13; hence y in REAL by C71; end; hence rng xm c= REAL by TARSKI:def 3; end;then reconsider xm1=xm as FinSequence of REAL; C51: Sum(xp) = Sum(xp1) by MESFUNC3:2; C52: Sum(xm) = Sum(xm1) by MESFUNC3:2; C54: len xp1 =L by A30,FINSEQ_1:def 3 .= len xm1 by B30,FINSEQ_1:def 3; C53: x1=xp1-xm1 proof AA4: dom (xp1-xm1) = (dom xp1) /\ (dom xm1) by VALUED_1:12 .= dom x1 by A3,B3,C30,FINSEQ_1:def 3,XXX2; for k be Nat st k in dom x1 holds (xp1 - xm1).k =x1.k proof let k be Nat; assume A6: k in dom x1; k in (dom xp1) /\ (dom xm1) by A30,B30,C30,A6;then PA8: k in dom (xp1 - xm1) by VALUED_1:12; A80: k in dom canFS(Omega) by C3,P1,A6,FUNCT_2:def 1; reconsider z=M.{(canFS(Omega)).k} as Element of REAL by CFSD,C3,P1,A6,XD0; A9: xp1.k =R_EAL (fp.((canFS(Omega)).k) ) * M.{(canFS(Omega)).k} by XB7,A30,C30,A6 .=(fp.((canFS(Omega)).k) )*z by EXTREAL1:13; A10: xm1.k =R_EAL (fm.((canFS(Omega)).k) ) * M.{(canFS(Omega)).k} by XA7,B30,C30,A6 .= (fm.((canFS(Omega)).k) ) * z by EXTREAL1:13; (canFS(Omega)).k in rng canFS(Omega) by A80,FUNCT_1:12; then (canFS(Omega)).k in Omega; then A11: (canFS(Omega)).k in dom f by FUNCT_2:def 1; A12: f =fp-fm by MESFUNC6:42; thus (xp1 - xm1).k = (fp.((canFS(Omega)).k) ) * z - (fm.((canFS(Omega)).k) ) * z by A9,A10,VALUED_1:13,PA8 .=( fp.((canFS(Omega)).k) - fm.((canFS(Omega)).k) ) * z .= (f.((canFS(Omega)).k) ) * z by VALUED_1:13,A11,A12 .= R_EAL (f.((canFS(Omega)).k) ) * M.{(canFS(Omega)).k} by EXTREAL1:13 .=x1.k by C7,A6; end; hence thesis by FINSEQ_1:17,AA4; end; UU1: dom Fm=dom am by LmX2,R1; UU2: for n be Nat st n in dom Fm for x be set st x in Fm.n holds fm.x=am.n proof let n be Nat such that Z: n in dom Fm; let x be set; assume x in Fm.n; then x in {(canFS(Dm)).n} by Z,R1; then x = (canFS(Dm)).n by TARSKI:def 1; hence fm.x=am.n by Z,UU1,FUNCT_1:22; end; C5:Integral(M,f) =Integral(M,fp-fm) by MESFUNC6:42 .=Sum(xp) -Sum(xm) by A5,MES43,B1,B2,B3,R1,XDm,UU1,UU2,P7 .=Sum(xp1) -Sum(xm1) by C51,C52,SUPINF_2:5 .=Sum(xp1-xm1) by INTEGRA5:2,C54 .=Sum(x) by MESFUNC3:2,C53; C61: len x = L by C30,FINSEQ_1:def 3; dom (canFS(D))=Seg (len F) by FINSEQ_1:def 3,P1;then len F = len (canFS(D)) by FINSEQ_1:def 3; hence thesis by C5,C61,XD0,UPROOTS:5,C7; end; theorem Lm9A4: for Omega be non empty finite set, M being sigma_Measure of Trivial-SigmaField (Omega), f be Function of Omega,REAL, x being FinSequence of ExtREAL, s being FinSequence of (Omega) st M.Omega < +infty & s is one-to-one & rng s = Omega & len s = card (Omega) ex F be Finite_Sep_Sequence of Trivial-SigmaField (Omega), a being FinSequence of REAL st dom f = union (rng F) & dom a = dom s & dom F = dom s & (for k be Nat st k in dom F holds F.k={s.k} ) & for n being Nat for x,y being Element of Omega st n in dom F & x in F.n & y in F.n holds f.x = f.y proof let Omega be non empty finite set, M be sigma_Measure of Trivial-SigmaField (Omega), f be Function of Omega,REAL, x be FinSequence of ExtREAL, s be FinSequence of (Omega); assume AS: M.Omega < +infty & s is one-to-one & rng s = Omega & len s = card (Omega); set Sigma=Trivial-SigmaField (Omega); defpred P[Nat,set] means $2={s.$1}; set L = len s; P1:for k be Nat st k in Seg L ex x being Element of bool Omega st P[k,x] proof let k be Nat; assume k in Seg L; then k in dom s by FINSEQ_1:def 3;then PP1PP: s.k in rng s by FUNCT_1:12; take {s.k}; thus thesis by PP1PP,ZFMISC_1:37; end; consider F being FinSequence of bool Omega such that P2: dom F = Seg L & for k be Nat st k in Seg L holds P[k,F.k] from FINSEQ_1:sch 5(P1); defpred Q[Nat,set] means $2=f.(s.$1); R1:for k be Nat st k in Seg L ex x being Element of REAL st Q[k,x]; consider a being FinSequence of REAL such that Q2: dom a = Seg L & for k be Nat st k in Seg L holds Q[k,a.k] from FINSEQ_1:sch 5(R1); Q1: dom F = dom s by P2,FINSEQ_1:def 3; now let i,j be Nat; assume A1: i in dom F & j in dom F & i <> j; A4: i in dom s & j in dom s by FINSEQ_1:def 3,A1,P2; PA3: s.i <> s.j by A1,A4,FUNCT_1:def 8,AS; F.i = {s.i } & F.j = {s.j } by A1,P2; hence F.i misses F.j by ZFMISC_1:17,PA3; end; then reconsider F as Finite_Sep_Sequence of Sigma by MESFUNC3:4; take F; union rng F = rng s proof now let x be set; assume x in union rng F; then consider y be set such that A2: x in y & y in rng F by TARSKI:def 4; consider n be set such that A3: n in dom F & y=F.n by A2,FUNCT_1:def 5; F.n = {s.n } by A3,P2;then A5:x = s.n by A2,A3,TARSKI:def 1; n in dom s by P2,A3,FINSEQ_1:def 3; hence x in rng s by FUNCT_1:def 5,A5; end; hence union rng F c= rng s by TARSKI:def 3; let x be set; assume x in rng s;then consider n be set such that A5: n in dom s & x=s.n by FUNCT_1:def 5; A4: n in Seg L by A5,FINSEQ_1:def 3; reconsider n as Element of NAT by A5; A3: n in dom F by P2,A5,FINSEQ_1:def 3; x in {s.n} by A5,TARSKI:def 1;then A2: x in F.n by P2,A4; F.n in rng F by A3,FUNCT_1:def 5; hence x in union rng F by A2,TARSKI:def 4; end;then P3: dom f = union rng F by AS,FUNCT_2:def 1; for n being Nat for x,y being Element of Omega st n in dom F & x in F.n & y in F.n holds f.x = f.y proof let n be Nat; let x,y be Element of Omega; assume AS1: n in dom F & x in F.n & y in F.n; P41: F.n = {s.n} by P2,AS1; thus f.x =f.(s.n) by P41,AS1,TARSKI:def 1 .=f.y by P41,AS1,TARSKI:def 1; end; hence thesis by Q1,P2,P3,Q2; end; theorem Lm9A3: for Omega be non empty finite set, M being sigma_Measure of Trivial-SigmaField (Omega), f be Function of Omega,REAL, x being FinSequence of ExtREAL, s being FinSequence of (Omega) st M.Omega < +infty & len x = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in dom x holds x.n = R_EAL (f.(s.n)) * M.{s.n}) holds Integral(M,f) =Sum x proof let Omega be non empty finite set, M be sigma_Measure of Trivial-SigmaField (Omega), f be Function of Omega,REAL, x be FinSequence of ExtREAL, s be FinSequence of (Omega); assume AS: M.Omega < +infty & len x = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in dom x holds x.n = R_EAL (f.(s.n)) * M.{s.n}); set Sigma= Trivial-SigmaField (Omega); consider F be Finite_Sep_Sequence of Sigma, a being FinSequence of REAL such that P1: dom f = union (rng F) & dom a = dom s & dom F = dom s & (for k be Nat st k in dom F holds F.k={s.k} ) & for n being Nat for x,y being Element of Omega st n in dom F & x in F.n & y in F.n holds f.x = f.y by Lm9A4,AS; set fp=max+(f); set fm=max-(f); XSD: dom x =Seg len s by AS,FINSEQ_1:def 3 .= dom F by P1,FINSEQ_1:def 3; XD0: dom f =Omega by FUNCT_2:def 1; XDp: dom fp=dom f by RFUNCT_3:def 10; XDm:dom fm=dom f by RFUNCT_3:def 11; set L=len F; CC:dom F =Seg L by FINSEQ_1:def 3; defpred AP[Nat,set] means for x be set st x in F.$1 holds $2=fp.x; AP1:for k be Nat st k in Seg L ex y being Element of REAL st AP[k,y] proof let k be Nat; assume P0: k in Seg L; take y=fp.(s.k); F.k = {s.k} by P1,CC,P0; hence thesis by TARSKI:def 1; end; consider ap being FinSequence of REAL such that AP2: dom ap = Seg L & for k be Nat st k in Seg L holds AP[k,ap.k] from FINSEQ_1:sch 5(AP1); defpred AM[Nat,set] means for x be set st x in F.$1 holds $2=fm.x; AM1:for k be Nat st k in Seg L ex y being Element of REAL st AM[k,y] proof let k be Nat; assume P0: k in Seg L; take y=fm.(s.k); F.k = {s.k} by P1,CC,P0; hence thesis by TARSKI:def 1; end; consider am being FinSequence of REAL such that AM2: dom am = Seg L & for k be Nat st k in Seg L holds AM[k,am.k] from FINSEQ_1:sch 5(AM1); FPP: fp is Function of Omega,REAL by XD0,XDp,FUNCT_2:def 1; A1: fp is_simple_func_in Sigma by Lm6; A2: fp is nonnegative by MESFUNC6:61; FMM: fm is Function of Omega,REAL by XD0,XDm,FUNCT_2:def 1; B1: fm is_simple_func_in Sigma by Lm6; B2: fm is nonnegative by MESFUNC6:61; defpred Pp[ Nat,set ] means $2=R_EAL (ap.$1) *(M*F).$1; A1P: for k being Nat st k in Seg L holds ex x being Element of ExtREAL st Pp[k,x]; consider xp being FinSequence of ExtREAL such that A30: dom xp = Seg L & for k being Nat st k in Seg L holds Pp[k,xp.k] from FINSEQ_1:sch 5(A1P); A3: dom xp = dom F & for n be Nat st n in dom xp holds xp.n=R_EAL (ap.n) *(M*F).n by A30,FINSEQ_1:def 3; defpred Pm[ Nat,set ] means $2=R_EAL (am.$1) *(M*F).$1; B1P: for k being Nat st k in Seg L holds ex x being Element of ExtREAL st Pm[k,x]; consider xm being FinSequence of ExtREAL such that B30: dom xm = Seg L & for k being Nat st k in Seg L holds Pm[k,xm.k] from FINSEQ_1:sch 5(B1P); B3: dom xm = dom F & for n be Nat st n in dom xm holds xm.n=R_EAL (am.n) *(M*F).n by B30,FINSEQ_1:def 3; A5:Integral(M,fp)=Sum(xp) by MES43,A1,A2,A30,P1,CC,AP2,XDp; X2:dom fp = Omega by XD0,RFUNCT_3:def 10; K2: fp is_integrable_on M by X2,Lm9A0,Lm6,AS; X3: dom fm = Omega by XD0,RFUNCT_3:def 11; K3: fm is_integrable_on M by X3,Lm9A0,Lm6,AS; M.(dom ((-1)(#)fm)) < +infty by AS,FUNCT_2:def 1,FMM;then K5:(-1)(#)fm is_integrable_on M by FMM,Lm9A0,Lm6; consider E be Element of Sigma such that K6: E = (dom fp) /\ dom ((-1)(#)fm) & Integral(M,fp+(-1)(#)fm) =Integral(M,fp|E)+Integral(M,((-1)(#)fm)|E) by K2,K5,MESFUNC6:101; K8: dom ((-1)(#)fm) = dom fm by VALUED_1:def 5 .=Omega by XD0,RFUNCT_3:def 11; K9: E = Omega /\ Omega by K8,XD0,RFUNCT_3:def 10,K6 .= Omega; K10: R_EAL(-1)*Integral(M,fm) =(-R_EAL(1)) *Integral(M,fm) by SUPINF_2:3 .= -(R_EAL(1)*Integral(M,fm) ) by XXREAL_3:103 .=-Integral(M,fm) by XXREAL_3:92; P6: ((-1)(#)fm)|E = (-1)(#)fm by FMM,K9,FUNCT_2:40; P7: Integral(M,fp+(-1)(#)fm) =Integral(M,fp) +Integral(M,(-1)(#)fm) by FPP,K9,FUNCT_2:40,P6,K6 .=Integral(M,fp) +-Integral(M,fm) by K10,MESFUNC6:102,K3; CFSD:for n be Nat st n in dom s holds M.{s.n} in REAL proof let n be Nat; assume n in dom s;then s.n in rng s by FUNCT_1:12;then {s.n } c= Omega by ZFMISC_1:37; hence M.({s.n }) in REAL by Lm9A2,AS; end; x is FinSequence of REAL proof now let y be set; assume y in rng x; then consider n be Element of NAT such that C71: n in dom x & y=x.n by PARTFUN1:26; reconsider w=f.(s.n) as Element of REAL; reconsider z=M.{s.n} as Element of REAL by CFSD,XSD,P1,C71; x.n = R_EAL (f.(s.n) ) * M.{s.n} by AS,C71 .= w*z by EXTREAL1:13; hence y in REAL by C71; end; hence rng x c= REAL by TARSKI:def 3; end; then reconsider x1=x as FinSequence of REAL; XB7: for n being Nat st n in dom xp holds xp.n = R_EAL (fp.(s.n) ) * M.{s.n} proof let n be Nat; assume C71: n in dom xp; F.n={s.n} by P1,A3,C71;then PC73: s.n in F.n by TARSKI:def 1; C74: (M*F).n =M.(F.n) by FUNCT_1:23,A3,C71 .= M.{s.n} by P1,A3,C71; thus xp.n=R_EAL (ap.n) *(M*F).n by A30,C71 .= R_EAL (fp.(s.n) ) * M.{s.n} by A30,AP2,C71,PC73,C74; end; xp is FinSequence of REAL proof now let y be set; assume y in rng xp; then consider n be Element of NAT such that C71: n in dom xp & y=xp.n by PARTFUN1:26; reconsider w=fp.(s.n) as Element of REAL; reconsider z=M.{s.n} as Element of REAL by CFSD,P1,A3,C71; xp.n = R_EAL (fp.(s.n) ) * M.{s.n} by XB7,C71 .= w*z by EXTREAL1:13; hence y in REAL by C71; end; hence rng xp c= REAL by TARSKI:def 3; end; then reconsider xp1=xp as FinSequence of REAL; XA7: for n being Nat st n in dom xm holds xm.n = R_EAL (fm.(s.n) ) * M.{s.n} proof let n be Nat; assume C71: n in dom xm; F.n={s.n} by P1,B3,C71;then PC73: s.n in F.n by TARSKI:def 1; C74: (M*F).n =M.(F.n) by FUNCT_1:23,B3,C71 .= M.{s.n} by P1,B3,C71; thus xm.n=R_EAL (am.n) *(M*F).n by B30,C71 .= R_EAL (fm.(s.n) ) * M.{s.n} by B30,AM2,C71,PC73,C74; end; xm is FinSequence of REAL proof now let y be set; assume y in rng xm; then consider n be Element of NAT such that C71: n in dom xm & y=xm.n by PARTFUN1:26; reconsider w=fm.(s.n) as Element of REAL; reconsider z=M.{s.n} as Element of REAL by CFSD,B3,C71,P1; xm.n = R_EAL (fm.(s.n) ) * M.{s.n} by XA7,C71 .= w*z by EXTREAL1:13; hence y in REAL by C71; end; hence rng xm c= REAL by TARSKI:def 3; end; then reconsider xm1=xm as FinSequence of REAL; C51: Sum(xp) = Sum(xp1) by MESFUNC3:2; C52: Sum(xm) = Sum(xm1) by MESFUNC3:2; C54: len xp1=L by A30,FINSEQ_1:def 3 .= len xm1 by B30,FINSEQ_1:def 3; C53: x1=xp1-xm1 proof AA4: dom (xp1-xm1) = (dom xp1) /\ (dom xm1) by VALUED_1:12 .= dom x1 by XSD,A3,B3; for k be Nat st k in dom x1 holds (xp1 - xm1).k =x1.k proof let k be Nat; assume A6: k in dom x1; k in (dom xp1) /\ (dom xm1) by XSD,A3,B3,A6;then PA8: k in dom (xp1 - xm1) by VALUED_1:12; reconsider z=M.{s.k} as Element of REAL by CFSD,XSD,P1,A6; A9: xp1.k=R_EAL (fp.(s.k) ) * M.{s.k} by XB7,XSD,A3,A6 .=(fp.(s.k) )*z by EXTREAL1:13; A10: xm1.k=R_EAL (fm.(s.k) ) * M.{s.k} by XA7,XSD,B3,A6 .= (fm.(s.k) ) * z by EXTREAL1:13; s.k in rng s by XSD,P1,A6,FUNCT_1:12; then s.k in Omega;then A11: s.k in dom f by FUNCT_2:def 1; A12: f =fp-fm by MESFUNC6:42; thus (xp1 - xm1).k = (fp.(s.k) ) * z - (fm.(s.k) ) * z by A9,A10,VALUED_1:13,PA8 .=( fp.(s.k) - fm.(s.k) ) * z .= (f.(s.k) ) * z by VALUED_1:13,A11,A12 .= R_EAL (f.(s.k) ) * M.{s.k}by EXTREAL1:13 .=x1.k by AS,A6; end; hence thesis by FINSEQ_1:17,AA4; end; thus Integral(M,f) =Integral(M,fp-fm) by MESFUNC6:42 .=Sum(xp) -Sum(xm) by A5,MES43,B1,B2,B30,XDm,P1,AM2,CC,P7 .=Sum(xp1) -Sum(xm1) by C51,C52,SUPINF_2:5 .=Sum(xp1-xm1) by INTEGRA5:2,C54 .=Sum(x) by MESFUNC3:2,C53; end; theorem for Omega be non empty finite set, M being sigma_Measure of Trivial-SigmaField (Omega), f be Function of Omega,REAL st M.Omega < +infty holds ex x being FinSequence of ExtREAL, s being FinSequence of (Omega) st len x = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in dom x holds x.n = R_EAL (f.(s.n)) * M.{s.n}) & Integral(M,f) = Sum x proof let Omega be non empty finite set, M be sigma_Measure of Trivial-SigmaField (Omega), f be Function of Omega,REAL; assume AS:M.Omega < +infty; set Sigma= Trivial-SigmaField (Omega); consider x being FinSequence of ExtREAL such that P1: len x = card (Omega) & (for n being Nat st n in dom x holds x.n = R_EAL (f.((canFS(Omega)).n)) * M.{(canFS(Omega)).n} ) & Integral(M,f) =Sum x by AS,Lm9A; set s=canFS(Omega); P3: rng s = Omega by FUNCT_2:def 3; P4: len s = card (Omega) by UPROOTS:5; reconsider s as FinSequence of Omega; thus thesis by P1,P3,P4; end; Lm10A: for Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), f be Function of Omega,REAL holds ex F being FinSequence of REAL st len F = card (Omega) & (for n being Nat st n in dom F holds F.n = f.((canFS(Omega)).n) * P.{(canFS(Omega)).n}) & Integral(P2M(P),f) =Sum F proof let Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), f be Function of Omega,REAL; set Sigma=Trivial-SigmaField (Omega); PAA1: P.Omega in REAL;then AA1: (P2M(P)).Omega < +infty by XXREAL_0:9; consider x being FinSequence of ExtREAL such that P1: len x = card (Omega) & (for n being Nat st n in dom x holds x.n = R_EAL (f.((canFS(Omega)).n)) * (P2M(P)).{(canFS(Omega)).n}) & Integral(P2M(P),f) = Sum x by Lm9A,PAA1,XXREAL_0:9; set M = P2M(P); CFSD: for n be Nat st n in dom canFS(Omega) holds M.{(canFS(Omega)).n} in REAL proof let n be Nat; assume n in dom canFS(Omega);then (canFS(Omega)).n in rng canFS(Omega) by FUNCT_1:12;then B1: {(canFS(Omega)).n } c= Omega by ZFMISC_1:37; Omega in Sigma by MEASURE1:21; hence M.({(canFS(Omega)).n }) in REAL by Lm9A2,B1,AA1; end; x is FinSequence of REAL proof now let y be set; assume y in rng x; then consider n be Element of NAT such that C71: n in dom x & y=x.n by PARTFUN1:26; reconsider w=f.((canFS(Omega)).n) as Element of REAL; Seg len x=Seg(len(canFS(Omega))) by P1,UPROOTS:5;then dom x = Seg (len (canFS(Omega))) by FINSEQ_1:def 3; then n in dom canFS(Omega) by FINSEQ_1:def 3,C71;then reconsider z=M.{(canFS(Omega)).n} as Element of REAL by CFSD; x.n = R_EAL (f.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} by P1,C71 .= w*z by EXTREAL1:13; hence y in REAL by C71; end; hence rng x c= REAL by TARSKI:def 3; end; then reconsider F=x as FinSequence of REAL; take F; P2: now let n be Nat; assume P21: n in dom F; thus F.n =R_EAL (f.((canFS(Omega)).n)) * (P2M(P)).{(canFS(Omega)).n} by P21,P1 .= (f.((canFS(Omega)).n)) * P.({(canFS(Omega)).n}) by EXTREAL1:13; end; thus thesis by P1,P2,MESFUNC3:2; end; theorem LMTX1: for Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), f be Function of Omega,REAL, x be FinSequence of REAL, s be FinSequence of Omega st len x = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) & (for n being Nat st n in dom x holds x.n = f.(s.n) * P.{s.n}) holds Integral(P2M(P),f) =Sum x proof let Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), f be Function of Omega,REAL, x be FinSequence of REAL, s be FinSequence of Omega; assume that AS: len x = card (Omega) & s is one-to-one &rng s = Omega &len s = card (Omega) and ASt:(for n being Nat st n in dom x holds x.n = f.(s.n) * P.{s.n}); set Sigma= Trivial-SigmaField (Omega); AA1: P.Omega in REAL; rng x c= ExtREAL by NUMBERS:31,XBOOLE_1:1; then reconsider x1= x as FinSequence of ExtREAL by FINSEQ_1:def 4; set M = P2M(P); AA2: now let n be Nat; assume P21: n in dom x1; thus x1.n = f.(s.n) * P.{s.n} by ASt,P21 .=R_EAL (f.(s.n) ) * (P2M(P)).{s.n} by EXTREAL1:13; end; Integral(M,f) =Sum x1 by AA1,AA2,AS,Lm9A3,XXREAL_0:9 .=Sum x by MESFUNC3:2; hence thesis; end; theorem LMTX2: for Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), f be Function of Omega,REAL holds 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 = f.(s.n) * P.{s.n}) & Integral(P2M(P),f) = Sum F proof let Omega be non empty finite set, P be Probability of Trivial-SigmaField (Omega), f be Function of Omega,REAL; set Sigma =Trivial-SigmaField (Omega); consider F being FinSequence of REAL such that P1: len F = card (Omega) & (for n being Nat st n in dom F holds F.n = f.((canFS(Omega)).n) * P.{(canFS(Omega)).n}) & Integral(P2M(P),f) =Sum F by Lm10A; set s=canFS(Omega); P3: rng s = Omega by FUNCT_2:def 3; len s = card Omega by UPROOTS:5; hence thesis by P1,P3; end; theorem LME1: for E be finite non empty set, ASeq being SetSequence of E st ASeq is non-ascending holds ex N be Element of NAT st for m be Element of NAT st N<=m holds ASeq.N = ASeq.m proof let E be finite non empty set, ASeq being SetSequence of E; assume A1: ASeq is non-ascending; defpred P[Element of NAT,set] means $2=card(ASeq.$1 ); P1:for x be Element of NAT ex y be Element of REAL st P[x,y] proof let x be Element of NAT; card(ASeq.x) in NAT; hence thesis; end; consider seq being Function of NAT,REAL such that P2: for n being Element of NAT holds P[n,seq.n] from FUNCT_2:sch 3(P1); PP3: now let n,m be Element of NAT; assume n <= m;then P21: ASeq.m c= ASeq.n by A1,PROB_1:def 6; seq.m = card(ASeq.m) & seq.n = card(ASeq.n) by P2; hence seq.m <=seq.n by P21,NAT_1:44; end;then P3: seq is non-increasing by SEQM_3:14; now let m be Element of NAT; seq.m = card(ASeq.m) by P2; hence -1 < seq.m; end; then seq is bounded_below by SEQ_2:def 4; then consider g be real number such that P4:for p be real number st 0
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;