:: Probability on Finite Set and Real Valued Random Variables :: by Hiroyuki Okazaki and Yasunari Shidama :: :: Received March 17, 2009 :: Copyright (c) 2009-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, PROB_1, MEASURE1, PARTFUN1, SUBSET_1, REAL_1, INTEGRA5, TARSKI, RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0, MEASURE6, MESFUNC5, FUNCT_3, VALUED_1, MESFUNC1, ARYTM_1, SUPINF_2, MESFUNC2, FINSEQ_1, NAT_1, CARD_3, CARD_1, MESFUNC3, INTEGRA1, ZFMISC_1, XXREAL_2, VALUED_0, RPR_1, FINSET_1, UPROOTS, RFUNCT_3, PROB_4, COMPLEX1, EQREL_1, SEQ_2, ORDINAL2, POWER, RANDOM_1, BSPACE, FUNCT_7, XCMPLX_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FINSET_1, CARD_1, NUMBERS, XXREAL_3, XREAL_0, XXREAL_0, XCMPLX_0, COMPLEX1, XXREAL_2, FUNCT_1, REAL_1, SUPINF_2, RELSET_1, PARTFUN1, VALUED_1, FINSEQ_1, RFUNCT_3, NAT_1, FUNCT_2, SEQ_2, RPR_1, PROB_1, PROB_4, MEASURE1, EXTREAL1, MESFUNC1, MESFUNC3, MEASURE6, MESFUNC5, MESFUNC6, MESFUNC2, RVSUM_1, UPROOTS, MESFUN6C; constructors REAL_1, RPR_1, NAT_3, EXTREAL1, POWER, RVSUM_1, MESFUNC6, MESFUNC3, MESFUNC5, MEASURE6, MESFUNC2, BINOP_2, INTEGRA2, PROB_4, SUPINF_1, UPROOTS, MESFUN6C, MESFUNC1, DOMAIN_1, RELSET_1, COMSEQ_2, FUNCT_7; registrations SUBSET_1, NAT_1, XREAL_0, XXREAL_0, MEMBERED, ORDINAL1, FINSEQ_1, MEASURE1, FUNCT_2, RELAT_1, SEQ_4, FINSET_1, NUMBERS, XCMPLX_0, VALUED_0, VALUED_1, RELSET_1, JORDAN5A, XXREAL_3; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions TARSKI, FINSEQ_1, XBOOLE_0; equalities RPR_1, SUBSET_1, MESFUNC5, MESFUNC6, PROB_4, VALUED_1, XBOOLE_0, XXREAL_3, SUPINF_2, PROB_1; expansions TARSKI, MESFUNC6, XBOOLE_0; 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, MESFUNC7, VALUED_0, VALUED_1, ABCMIZ_1, RCOMP_1, MESFUN6C, FINSEQ_3, XXREAL_3, XREAL_0, CARD_2; schemes FINSEQ_1, FUNCT_2, FINSEQ_2; begin theorem Th1: 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 (a qua ExtReal)*(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:97; 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 A6: x in dom(a(#)(C|E)); then A7: x in dom(C|E) by MESFUNC1:def 6; then x in dom C /\ E by RELAT_1:61; then A8: x in E by XBOOLE_0:def 4; then a <= f.x by A4; then A9: a <= (f|E).x by A8,FUNCT_1:49; (a(#)(C|E)).x = a * (C|E).x by A6,MESFUNC1:def 6 .= a * C.x by A7,FUNCT_1:47 .= a * 1.by A8,FUNCT_3:def 3; hence thesis by A9,XXREAL_3:81; end; then A10: (f|E) - (a(#)(C|E)) is nonnegative by MESFUNC7:1; dom(a(#)(C|E)) = dom(C|E) by MESFUNC1:def 6; then dom(a(#)(C|E)) = dom C /\ E by RELAT_1:61; then dom(a(#)(C|E)) = X /\ E by FUNCT_3:def 3; then A11: dom(a(#)(C|E)) = E by XBOOLE_1:28; E = E/\E; then A12: Integral(M,C|E) = M.E by A3,MESFUNC7:25; reconsider a as Real; chi(E,X) is_integrable_on M by A3,MESFUNC7:24; then A13: C|E is_integrable_on M by MESFUNC5:97; then a(#)(C|E) is_integrable_on M by MESFUNC5:110; then consider E1 be Element of S such that A14: E1 = dom(f|E) /\ dom(a(#)(C|E)) and A15: Integral(M,(a(#)(C|E))|E1) <= Integral(M,(f|E)|E1) by A5,A10,MESFUNC7:3; dom(f|E) = dom f /\ E by RELAT_1:61; then dom(f|E) = E by A2,XBOOLE_1:28; then (a(#)(C|E))|E1 = a(#)(C|E) & (f|E)|E1 = f|E by A14,A11; hence thesis by A13,A15,A12,MESFUNC5:110; end; theorem Th2: 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 (a qua ExtReal)*M.E <= Integral(M,f|E) by Th1; theorem Th3: 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) <= (a qua ExtReal)*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:97; dom(a(#)(C|E)) = dom(C|E) by MESFUNC1:def 6; then dom(a(#)(C|E)) = dom C /\ E by RELAT_1:61; then dom(a(#)(C|E)) = X /\ E by FUNCT_3:def 3; then A6: dom(a(#)(C|E)) = E by XBOOLE_1:28; dom(f|E) = dom f /\ E by RELAT_1:61; then A7: dom(f|E) = E by A2,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 A9: x in dom(C|E) by A7,A6,MESFUNC1:def 6; then x in dom C /\ E by RELAT_1:61; then A10: x in E by XBOOLE_0:def 4; then f.x <= a by A4; then A11: (f|E).x <=a by A10,FUNCT_1:49; (a(#)(C|E)).x = a * (C|E).x by A7,A6,A8,MESFUNC1:def 6 .= a * C.x by A9,FUNCT_1:47 .= a * 1.by A10,FUNCT_3:def 3; hence thesis by A11,XXREAL_3:81; end; then A12: (a(#)(C|E))-(f|E) is nonnegative by MESFUNC7:1; dom(a(#)(C|E)) = dom(C|E) by MESFUNC1:def 6; then dom(a(#)(C|E)) = dom C /\ E by RELAT_1:61; then dom(a(#)(C|E)) = X /\ E by FUNCT_3:def 3; then A13: dom(a(#)(C|E)) = E by XBOOLE_1:28; E = E/\E; then A14: Integral(M,C|E) = M.E by A3,MESFUNC7:25; chi(E,X) is_integrable_on M by A3,MESFUNC7:24; then A15: C|E is_integrable_on M by MESFUNC5:97; then a(#)(C|E) is_integrable_on M by MESFUNC5:110; then consider E1 be Element of S such that A16: E1 = dom(f|E) /\ dom(a(#)(C|E)) and A17: Integral(M,(f|E)|E1) <= Integral(M,(a(#)(C|E))|E1) by A5,A12,MESFUNC7:3; dom(f|E) = dom f /\ E by RELAT_1:61; then dom(f|E) = E by A2,XBOOLE_1:28; then (a(#)(C|E))|E1 = a(#)(C|E) & (f|E)|E1 = f|E by A16,A13; hence thesis by A15,A17,A14,MESFUNC5:110; 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) <=(a qua ExtReal)*M.E by Th3; :: Integral of real valued simple functions Lm1: 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 object 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=(a.n qua ExtReal)*(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 and A2: dom f <> {} and A3: f is nonnegative and A4: dom f = union rng F & dom F = dom a & for n be Nat st n in dom F for x be object st x in F.n holds f.x=a.n and A5: dom x = dom F and A6: for n be Nat st n in dom x holds x.n = (a.n qua ExtReal)*(M*F).n; A7: R_EAL f is_simple_func_in S & for x be object st x in dom(R_EAL f) holds 0 <=( R_EAL f).x by A1,A3,MESFUNC6:49,51; reconsider a0=a as FinSequence of ExtREAL by MESFUNC3:11; A8: F,a0 are_Re-presentation_of R_EAL f by A4,MESFUNC3:def 1; A9: for n be Nat st n in dom x holds x.n = a0.n*(M*F).n by A6; thus Integral(M,f) = integral'(M,R_EAL f) by A1,A3,MESFUNC6:83 .= integral(M,R_EAL f) by A2,MESFUNC5:def 14 .= Sum(x) by A2,A3,A5,A7,A8,A9,MESFUNC4:3; end; Lm2: 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; defpred P[Nat,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:3; per cases; suppose A6: F.k = {}; take In(0,REAL); thus thesis by A6; end; suppose F.k <> {}; then consider x1 be object such that A7: x1 in F.k by XBOOLE_0:def 1; reconsider fx1 = f.x1 as Element of REAL by XREAL_0:def 1; take fx1; rng F c= bool X by XBOOLE_1:1; hence thesis by A2,A4,A5,A7; end; end; consider a be FinSequence of REAL such that A8: 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); take F,a; 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 A8; end; hence thesis by A1,A8,FINSEQ_1:def 3; end; Lm3: 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 real-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 and A2: dom F = dom a and A3: for n be Nat st n in dom F for x be set st x in F.n holds f.x = a.n by Lm2; rng f c= rng a proof let y be object; assume y in rng f; then consider x be object such that A4: x in dom(f) and A5: y = f.x by FUNCT_1:def 3; consider z be set such that A6: x in z and A7: z in rng F by A1,A4,TARSKI:def 4; consider n be object such that A8: n in dom F and A9: z= F.n by A7,FUNCT_1:def 3; f.x = a.n by A3,A6,A8,A9; hence y in rng a by A2,A5,A8,FUNCT_1:def 3; end; hence thesis by RCOMP_1:10; end; Lm4: 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 real-bounded & M.(dom f) < +infty & ex E be Element of S st E = dom f & f is E-measurable 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 that A1: dom f <> {} and A2: rng f is real-bounded and A3: M.(dom f) < +infty and A4: ex E be Element of S st E = dom f & f is E-measurable; consider E be Element of S such that A5: E = dom f and A6: f is E-measurable by A4; A7: dom (R_EAL f) /\ dom(chi(E,X)) = E /\ X by A5,FUNCT_3:def 3; then A8: chi(E,X) is real-valued & dom (R_EAL f) /\ dom(chi(E,X)) = E by MESFUNC2:28 ,XBOOLE_1:28; A9: dom((R_EAL f)(#)(chi(E,X))) = dom (R_EAL f) /\ dom(chi(E,X)) by MESFUNC1:def 5 .= E by A7,XBOOLE_1:28; A10: now let x be object; assume A11: x in dom f; then ( (R_EAL f)(#)(chi(E,X)) ).x = (R_EAL f).x * (chi(E,X)).x by A5,A9, MESFUNC1:def 5; then ( (R_EAL f)(#)(chi(E,X)) ).x = (R_EAL f).x * 1 by A5,A11, FUNCT_3:def 3 .= f.x by XXREAL_3:81; hence (( (R_EAL f)(#)(chi(E,X)) )|E).x = f.x by A9; end; A12: R_EAL f is E-measurable by A6; A13: rng(R_EAL f) is non empty Subset of ExtREAL by A1,RELAT_1:42; dom(( (R_EAL f)(#)(chi(E,X)) )|E) = dom f by A5,A9; then A14: ( (R_EAL f)(#)(chi(E,X)) )|E = f by A10,FUNCT_1:2; chi(E,X) is_integrable_on M by A3,A5,MESFUNC7:24; then ((R_EAL f)(#)(chi(E,X)) )|E is_integrable_on M by A2,A13,A12,A8, MESFUNC7:17; hence thesis by A14; end; Lm5: 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; then rng f is real-bounded by Lm3; hence thesis by A1,Lm4,MESFUNC6:50; end; begin :: Trivial SigmaField and Probability on Finite set reserve Omega for non empty set; reserve r for Real; reserve Sigma for SigmaField of Omega; reserve P for Probability 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:40; end; Lm6: 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)); A1: 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 A2: k in Seg L; take {(canFS(D)).k }; k in dom canFS(D) by A2,FINSEQ_1:def 3; then (canFS(D)).k in rng canFS(D) by FUNCT_1:3; then (canFS(D)).k in D; hence thesis by ZFMISC_1:31; end; consider F being FinSequence of bool Omega such that A3: dom F = Seg L & for k be Nat st k in Seg L holds P[k,F.k] from FINSEQ_1:sch 5(A1); now let i,j be Nat; assume that A4: i in dom F & j in dom F and A5: i <> j; i in dom (canFS(D)) & j in dom (canFS(D)) by A3,A4,FINSEQ_1:def 3; then A6: (canFS(D)).i <> (canFS(D)).j by A5,FUNCT_1:def 4; F.i = {(canFS(D)).i } & F.j = {(canFS(D)).j } by A3,A4; hence F.i misses F.j by A6,ZFMISC_1:11; end; then reconsider F as Finite_Sep_Sequence of Sigma by MESFUNC3:4; now let x be object; assume x in rng canFS(D); then consider n be object such that A7: n in dom (canFS(D)) and A8: x=(canFS(D)).n by FUNCT_1:def 3; A9: n in Seg L by A7,FINSEQ_1:def 3; reconsider n as Element of NAT by A7; n in dom F by A3,A7,FINSEQ_1:def 3; then A10: F.n in rng F by FUNCT_1:def 3; x in {(canFS(D)).n} by A8,TARSKI:def 1; then x in F.n by A3,A9; hence x in union rng F by A10,TARSKI:def 4; end; then A11: rng canFS(D) c= union rng F; take F; A12: 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 that A13: n in dom F and A14: x in F.n and A15: y in F.n; A16: F.n = {(canFS(D)).n} by A3,A13; hence f.x =f.((canFS(D)).n) by A14,TARSKI:def 1 .=f.y by A15,A16,TARSKI:def 1; end; now let x be object; assume x in union rng F; then consider y be set such that A17: x in y and A18: y in rng F by TARSKI:def 4; consider n be object such that A19: n in dom F and A20: y=F.n by A18,FUNCT_1:def 3; reconsider n as Element of NAT by A19; F.n = {(canFS(D)).n } by A3,A19; then A21: x= (canFS(D)).n by A17,A20,TARSKI:def 1; n in dom (canFS(D)) by A3,A19,FINSEQ_1:def 3; hence x in rng canFS(D) by A21,FUNCT_1:def 3; end; then union rng F c= rng canFS(D); then union rng F = rng canFS(D) by A11; hence thesis by A3,A12,FINSEQ_1:def 3,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; set s=canFS(D); A1: len s = card (dom f) by FINSEQ_1:93; (ex F be Finite_Sep_Sequence of Sigma st 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 )& rng s = dom f by Lm6,FUNCT_2:def 3; hence thesis by A1; end; theorem Th6: 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; ex F be Finite_Sep_Sequence of Sigma st 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 Lm6; hence thesis; 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 Lm5,Th6; Lm7: 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 A in Sigma & B in Sigma & A c= B & M.B < +infty; then M.A <> -infty & M.A <> +infty by MEASURE1:31,def 2; hence thesis by XXREAL_0:14; end; Lm8: 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 A1: f*canFS dom f is FinSequence by FINSEQ_1:16; rng(f*canFS dom f) c= REAL; hence f*canFS dom f is FinSequence of REAL by A1,FINSEQ_1:def 4; end; Lm9: 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:27; end; theorem Th8: 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 X-measurable 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 Th6,MESFUNC6:50; end; reconsider jj=1 as Real; Lm10: 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 = (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; set fm=max-(f); set Dm = dom fm; reconsider am = fm*canFS Dm as FinSequence of REAL by Lm8; set fp=max+(f); set Dp = dom fp; reconsider ap = fp*canFS Dp as FinSequence of REAL by Lm8; set Sigma= Trivial-SigmaField (Omega),D =dom f; consider F be Finite_Sep_Sequence of Sigma such that dom f = union (rng F) and A1: dom F = dom (canFS(D)) and A2: for k be Nat st k in dom F holds F.k={(canFS(D)).k} and 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 Lm6; set L=len F; consider Fp be Finite_Sep_Sequence of Sigma such that A3: dom fp = union (rng Fp) and A4: dom Fp = dom (canFS(Dp)) and A5: for k be Nat st k in dom Fp holds Fp.k={(canFS(Dp)).k} and 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 Lm6; defpred Pp[ Nat,set ] means $2=(ap.$1) *(M*Fp).$1; A6: 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 A7: dom xp = Seg L & for k being Nat st k in Seg L holds Pp[k,xp.k] from FINSEQ_1:sch 5(A6); A8: dom Fp=dom ap by A4,Lm9; A9: for n be Nat st n in dom Fp for x be object st x in Fp.n holds fp.x=ap.n proof let n be Nat such that A10: n in dom Fp; let x be object; assume x in Fp.n; then x in {(canFS(Dp)).n} by A5,A10; then x = (canFS(Dp)).n by TARSKI:def 1; hence fp.x=ap.n by A8,A10,FUNCT_1:12; end; reconsider a = f*canFS D as FinSequence of REAL by Lm8; A11: (-jj)*Integral(M,fm) =(-(jj qua ExtReal)) *Integral(M,fm) .= -((1)*Integral(M,fm) ) by XXREAL_3:92 .=-Integral(M,fm) by XXREAL_3:81; defpred PX[ Nat,set ] means $2=(a.$1) *(M*F).$1; A12: 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 A13: dom x = Seg L & for k being Nat st k in Seg L holds PX[k,x.k] from FINSEQ_1:sch 5(A12); assume A14: M.Omega < +infty; A15: 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:3; then A16: {(canFS(Omega)).n } c= Omega by ZFMISC_1:31; Omega in Sigma by MEASURE1:7; hence M.({(canFS(Omega)).n }) in REAL by A14,A16,Lm7; end; A17: dom f =Omega by FUNCT_2:def 1; then A18: dom fm = Omega by RFUNCT_3:def 11; then A19: fm is_integrable_on M by A14,Lm5,Th6; A20: dom x = dom F by A13,FINSEQ_1:def 3; A21: for n being Nat st n in dom x holds x.n = (f.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} proof let n be Nat; assume A22: n in dom x; then A23: (M*F).n =M.(F.n) by A20,FUNCT_1:13 .= M.{(canFS(Omega)).n} by A2,A17,A20,A22; A24: f.((canFS(D)).n) =a.n by A1,A20,A22,FUNCT_1:13; thus x.n= (a.n) *(M*F).n by A13,A22 .= (f.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} by A24,A23, FUNCT_2:def 1; end; x is FinSequence of REAL proof let y be object; assume y in rng x; then consider n be Element of NAT such that A25: n in dom x and A26: y=x.n by PARTFUN1:3; reconsider z=M.{(canFS(Omega)).n} as Element of REAL by A1,A17,A20,A15,A25; reconsider w=f.((canFS(Omega)).n) as Element of REAL by XREAL_0:def 1; x.n = (f.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} by A21,A25 .= w*z by EXTREAL1:1; hence y in REAL by A26; end; then reconsider x1=x as FinSequence of REAL; take x; A27: fm is_simple_func_in Sigma & fm is nonnegative by Th6,MESFUNC6:61; A28: dom Fp=dom F by A1,A4,RFUNCT_3:def 10; then A29: dom xp = dom Fp by A7,FINSEQ_1:def 3; A30: Dp=D by RFUNCT_3:def 10; A31: for n being Nat st n in dom xp holds xp.n = (fp.((canFS(Omega)).n ) ) * M.{(canFS(Omega)).n} proof let n be Nat; assume A32: n in dom xp; then A33: (M*Fp).n =M.(Fp.n) by A29,FUNCT_1:13 .= M.{(canFS(Omega)).n} by A17,A5,A30,A29,A32; A34: fp.((canFS(D)).n) =ap.n by A4,A30,A29,A32,FUNCT_1:13; thus xp.n= (ap.n) *(M*Fp).n by A7,A32 .= (fp.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} by A34,A33, FUNCT_2:def 1; end; now let y be object; assume y in rng xp; then consider n be Element of NAT such that A35: n in dom xp and A36: y=xp.n by PARTFUN1:3; reconsider z=M.{(canFS(Omega)).n} as Element of REAL by A17,A4,A30,A29,A15 ,A35; reconsider w=fp.((canFS(Omega)).n) as Element of REAL by XREAL_0:def 1; xp.n = (fp.((canFS(Omega)).n)) * M.{(canFS(Omega)).n} by A31,A35 .= w*z by EXTREAL1:1; hence y in REAL by A36; end; then rng xp c= REAL; then reconsider xp1=xp as FinSequence of REAL by FINSEQ_1:def 4; consider Fm be Finite_Sep_Sequence of Sigma such that A37: dom fm = union (rng Fm) and A38: dom Fm = dom (canFS(Dm)) and A39: for k be Nat st k in dom Fm holds Fm.k={(canFS(Dm)).k} and 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 Lm6; defpred Pm[Nat,set] means $2=(am.$1) *(M*Fm).$1; A40: 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 A41: dom xm = Seg L & for k being Nat st k in Seg L holds Pm[k,xm.k] from FINSEQ_1:sch 5(A40); A42: dom Fm= dom F by A1,A38,RFUNCT_3:def 11; then A43: dom xm = dom Fm by A41,FINSEQ_1:def 3; A44: Dm=D by RFUNCT_3:def 11; A45: for n being Nat st n in dom xm holds xm.n = (fm.((canFS(Omega)).n ) ) * M.{(canFS(Omega)).n} proof let n be Nat; assume A46: n in dom xm; then A47: (M*Fm).n =M.(Fm.n) by A43,FUNCT_1:13 .= M.{(canFS(Omega)).n} by A17,A39,A44,A43,A46; thus xm.n= (am.n) *(M*Fm).n by A41,A46 .= (fm.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} by A38,A43,A18 ,A46,A47,FUNCT_1:13; end; now let y be object; assume y in rng xm; then consider n be Element of NAT such that A48: n in dom xm and A49: y=xm.n by PARTFUN1:3; reconsider z=M.{(canFS(Omega)).n} as Element of REAL by A17,A38,A44,A43,A15 ,A48; reconsider w=fm.((canFS(Omega)).n) as Element of REAL by XREAL_0:def 1; xm.n = (fm.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} by A45,A48 .= w*z by EXTREAL1:1; hence y in REAL by A49; end; then rng xm c= REAL; then reconsider xm1=xm as FinSequence of REAL by FINSEQ_1:def 4; A50: Sum(xp) = Sum(xp1) & Sum(xm) = Sum(xm1) by MESFUNC3:2; dom fp = Omega by A17,RFUNCT_3:def 10; then A51: fp is_integrable_on M by A14,Lm5,Th6; A52: dom fm=dom f by RFUNCT_3:def 11; then A53: fm is Function of Omega,REAL by A17,FUNCT_2:def 1; then M.(dom ((-1)(#)fm)) < +infty by A14,FUNCT_2:def 1; then (-1)(#)fm is_integrable_on M by A53,Lm5,Th6; then consider E be Element of Sigma such that A54: E = (dom fp) /\ dom ((-1)(#)fm) and A55: Integral(M,fp+(-1)(#)fm) =Integral(M,fp|E)+Integral(M,((-1)(#)fm)|E ) by A51,MESFUNC6:101; A56: dom fp=dom f by RFUNCT_3:def 10; dom ((-1)(#)fm) =dom fm by VALUED_1:def 5 .=Omega by A52,FUNCT_2:def 1; then A57: E = Omega /\ Omega by A56,A54,FUNCT_2:def 1 .= Omega; A58: Integral(M,fp+(-1)(#)fm) =Integral(M,fp) +Integral(M,(-1)(#)fm) by A55 ,A57 .=Integral(M,fp) +-Integral(M,fm) by A19,A11,MESFUNC6:102; A59: dom Fm=dom am by A38,Lm9; A60: for n be Nat st n in dom Fm for x be object st x in Fm.n holds fm.x=am.n proof let n be Nat such that A61: n in dom Fm; let x be object; assume x in Fm.n; then x in {(canFS(Dm)).n} by A39,A61; then x = (canFS(Dm)).n by TARSKI:def 1; hence fm.x=am.n by A59,A61,FUNCT_1:12; end; fp is_simple_func_in Sigma & fp is nonnegative by Th6,MESFUNC6:61; then A62: Integral(M,fp)=Sum(xp) by A56,A3,A7,A29,A8,A9,Lm1; dom (canFS(D))=Seg (len F) by A1,FINSEQ_1:def 3; then A63: len F = len (canFS(D)) by FINSEQ_1:def 3; A64: len x = L by A13,FINSEQ_1:def 3; A65: dom (xp1-xm1) = (dom xp1) /\ (dom xm1) by VALUED_1:12 .= dom x1 by A28,A42,A13,A29,A43,FINSEQ_1:def 3; A66: len xp1 =L by A7,FINSEQ_1:def 3 .= len xm1 by A41,FINSEQ_1:def 3; A67: for k be Nat st k in dom x1 holds (xp1 - xm1).k =x1.k proof let k be Nat; A68: f =fp-fm by MESFUNC6:42; assume A69: k in dom x1; then reconsider z=M.{(canFS(Omega)).k} as Element of REAL by A1,A17,A20,A15 ; A70: xm1.k = (fm.((canFS(Omega)).k) ) * M.{(canFS(Omega)).k} by A13,A41 ,A45,A69 .= (fm.((canFS(Omega)).k) ) * z by EXTREAL1:1; k in dom canFS(Omega) by A1,A20,A69,FUNCT_2:def 1; then (canFS(Omega)).k in rng canFS(Omega) by FUNCT_1:3; then (canFS(Omega)).k in Omega; then A71: (canFS(Omega)).k in dom f by FUNCT_2:def 1; k in (dom xp1) /\ (dom xm1) by A13,A7,A41,A69; then A72: k in dom (xp1 - xm1) by VALUED_1:12; xp1.k = (fp.((canFS(Omega)).k) ) * M.{(canFS(Omega)).k} by A13,A7,A31 ,A69 .=(fp.((canFS(Omega)).k) )*z by EXTREAL1:1; hence (xp1 - xm1).k = (fp.((canFS(Omega)).k) ) * z - (fm.((canFS(Omega)).k) ) * z by A72,A70,VALUED_1:13 .=( fp.((canFS(Omega)).k) - (fm.((canFS(Omega)).k) qua Real)) * z .= (f.((canFS(Omega)).k) ) * z by A71,A68,VALUED_1:13 .= (f.((canFS(Omega)).k) ) * M.{(canFS(Omega)).k} by EXTREAL1:1 .=x1.k by A21,A69; end; Integral(M,f) =Integral(M,fp-fm) by MESFUNC6:42 .=Sum(xp) -Sum(xm) by A52,A37,A27,A41,A43,A62,A58,A59,A60,Lm1 .=Sum(xp1) -Sum(xm1) by A50,SUPINF_2:3 .=Sum(xp1-xm1) by A66,INTEGRA5:2 .=Sum(x) by A65,A67,FINSEQ_1:13,MESFUNC3:2; hence thesis by A17,A21,A64,A63,FINSEQ_1:93; end; theorem Th9: 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 s is one-to-one & rng s = 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 that A1: s is one-to-one and A2: rng s = Omega; defpred Q[Nat,set] means $2=f.(s.$1); set Sigma=Trivial-SigmaField (Omega); set L = len s; defpred P[Nat,set] means $2={s.$1}; A3: 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 A4: k in Seg L; take {s.k}; k in dom s by A4,FINSEQ_1:def 3; then s.k in rng s by FUNCT_1:3; hence thesis by ZFMISC_1:31; end; consider F being FinSequence of bool Omega such that A5: dom F = Seg L & for k be Nat st k in Seg L holds P[k,F.k] from FINSEQ_1:sch 5(A3); A6: now let i,j be Nat; assume that A7: i in dom F & j in dom F and A8: i <> j; i in dom s & j in dom s by A5,A7,FINSEQ_1:def 3; then A9: s.i <> s.j by A1,A8,FUNCT_1:def 4; F.i = {s.i } & F.j = {s.j } by A5,A7; hence F.i misses F.j by A9,ZFMISC_1:11; end; A10: dom F = dom s by A5,FINSEQ_1:def 3; reconsider F as Finite_Sep_Sequence of Sigma by A6,MESFUNC3:4; union rng F = rng s proof now let x be object; assume x in union rng F; then consider y be set such that A11: x in y and A12: y in rng F by TARSKI:def 4; consider n be object such that A13: n in dom F and A14: y=F.n by A12,FUNCT_1:def 3; F.n = {s.n } by A5,A13; then A15: x = s.n by A11,A14,TARSKI:def 1; n in dom s by A5,A13,FINSEQ_1:def 3; hence x in rng s by A15,FUNCT_1:def 3; end; hence union rng F c= rng s; let x be object; assume x in rng s; then consider n be object such that A16: n in dom s and A17: x=s.n by FUNCT_1:def 3; A18: n in Seg L by A16,FINSEQ_1:def 3; reconsider n as Element of NAT by A16; n in dom F by A5,A16,FINSEQ_1:def 3; then A19: F.n in rng F by FUNCT_1:def 3; x in {s.n} by A17,TARSKI:def 1; then x in F.n by A5,A18; hence x in union rng F by A19,TARSKI:def 4; end; then A20: dom f = union rng F by A2,FUNCT_2:def 1; take F; A21: 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 that A22: n in dom F and A23: x in F.n and A24: y in F.n; A25: F.n = {s.n} by A5,A22; hence f.x =f.(s.n) by A23,TARSKI:def 1 .=f.y by A24,A25,TARSKI:def 1; end; A26: for k be Nat st k in Seg L ex x being Element of REAL st Q[k,x] proof let k be Nat; f.(s.k) in REAL by XREAL_0:def 1; hence thesis; end; ex a being FinSequence of REAL st ( dom a = Seg L & for k be Nat st k in Seg L holds Q[k,a.k]) from FINSEQ_1:sch 5(A26 ); hence thesis by A5,A10,A20,A21; end; theorem Th10: 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 = (f.(s.n) qua ExtReal) * 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 that A1: M.Omega < +infty and A2: len x = card (Omega) and A3: s is one-to-one and A4: rng s = Omega and A5: len s = card (Omega) and A6: for n being Nat st n in dom x holds x.n = (f.(s.n) qua ExtReal) * M.{s.n}; set Sigma= Trivial-SigmaField (Omega); consider F be Finite_Sep_Sequence of Sigma, a being FinSequence of REAL such that A7: dom f = union (rng F) and dom a = dom s and A8: dom F = dom s and A9: for k be Nat st k in dom F holds F.k={s.k} and 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 A3,A4,Th9; A10: dom x =Seg len s by A2,A5,FINSEQ_1:def 3 .= dom F by A8,FINSEQ_1:def 3; set fm=max-(f); set fp=max+(f); A11: dom f =Omega by FUNCT_2:def 1; then dom fp = Omega by RFUNCT_3:def 10; then A12: fp is_integrable_on M by A1,Lm5,Th6; A13: 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:3; then {s.n } c= Omega by ZFMISC_1:31; hence M.({s.n }) in REAL by A1,A4,Lm7; end; now let y be object; assume y in rng x; then consider n be Element of NAT such that A14: n in dom x and A15: y=x.n by PARTFUN1:3; reconsider z=M.{s.n} as Element of REAL by A8,A10,A13,A14; reconsider w=f.(s.n) as Element of REAL by XREAL_0:def 1; x.n = (f.(s.n) ) * M.{s.n} by A6,A14 .= w*z by EXTREAL1:1; hence y in REAL by A15; end; then rng x c= REAL; then reconsider x1=x as FinSequence of REAL by FINSEQ_1:def 4; A16: fm is_simple_func_in Sigma & fm is nonnegative by Th6,MESFUNC6:61; defpred AP[Nat,set] means for x be object st x in F.$1 holds $2=fp.x; set L=len F; A17: dom F =Seg L by FINSEQ_1:def 3; A18: 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 A19: k in Seg L; reconsider fpsk = fp.(s.k) as Element of REAL by XREAL_0:def 1; take fpsk; F.k = {s.k} by A9,A17,A19; hence thesis by TARSKI:def 1; end; consider ap being FinSequence of REAL such that A20: dom ap = Seg L & for k be Nat st k in Seg L holds AP[k,ap.k] from FINSEQ_1:sch 5(A18); defpred AM[Nat,set] means for x be object st x in F.$1 holds $2=fm.x; A21: 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 A22: k in Seg L; reconsider fmsk = fm.(s.k) as Element of REAL by XREAL_0:def 1; take fmsk; F.k = {s.k} by A9,A17,A22; hence thesis by TARSKI:def 1; end; consider am being FinSequence of REAL such that A23: dom am = Seg L & for k be Nat st k in Seg L holds AM[k,am.k] from FINSEQ_1:sch 5(A21); A24: dom fm=dom f by RFUNCT_3:def 11; then A25: fm is Function of Omega,REAL by A11,FUNCT_2:def 1; then M.(dom ((-1)(#)fm)) < +infty by A1,FUNCT_2:def 1; then (-1)(#)fm is_integrable_on M by A25,Lm5,Th6; then consider E be Element of Sigma such that A26: E = (dom fp) /\ dom ((-1)(#)fm) and A27: Integral(M,fp+(-1)(#)fm) =Integral(M,fp|E)+Integral(M,((-1)(#)fm)|E ) by A12,MESFUNC6:101; A28: (-jj)*Integral(M,fm) =(- (jj qua ExtReal)) *Integral(M,fm) .= -((1 qua ExtReal)*Integral(M,fm) ) by XXREAL_3:92 .=-Integral(M,fm) by XXREAL_3:81; defpred Pp[ Nat,set ] means $2= (ap.$1) *(M*F).$1; A29: 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(A29); A31: dom xp = dom F by A30,FINSEQ_1:def 3; A32: for n being Nat st n in dom xp holds xp.n = (fp.(s.n) ) * M.{s.n} proof let n be Nat; assume A33: n in dom xp; then A34: (M*F).n =M.(F.n) by A31,FUNCT_1:13 .= M.{s.n} by A9,A31,A33; F.n={s.n} by A9,A31,A33; then A35: s.n in F.n by TARSKI:def 1; thus xp.n= (ap.n) *(M*F).n by A30,A33 .= (fp.(s.n) ) * M.{s.n} by A20,A30,A33,A35,A34; end; now let y be object; assume y in rng xp; then consider n be Element of NAT such that A36: n in dom xp and A37: y=xp.n by PARTFUN1:3; reconsider z=M.{s.n} as Element of REAL by A8,A31,A13,A36; reconsider w=fp.(s.n) as Element of REAL by XREAL_0:def 1; xp.n = (fp.(s.n) ) * M.{s.n} by A32,A36 .= w*z by EXTREAL1:1; hence y in REAL by A37; end; then rng xp c= REAL; then reconsider xp1=xp as FinSequence of REAL by FINSEQ_1:def 4; defpred Pm[ Nat,set ] means $2= (am.$1) *(M*F).$1; A38: 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 A39: dom xm = Seg L & for k being Nat st k in Seg L holds Pm[k,xm.k] from FINSEQ_1:sch 5(A38); A40: dom xm = dom F by A39,FINSEQ_1:def 3; A41: for n being Nat st n in dom xm holds xm.n = (fm.(s.n) ) * M.{s.n} proof let n be Nat; assume A42: n in dom xm; then A43: (M*F).n =M.(F.n) by A40,FUNCT_1:13 .= M.{s.n} by A9,A40,A42; F.n={s.n} by A9,A40,A42; then A44: s.n in F.n by TARSKI:def 1; thus xm.n= (am.n) *(M*F).n by A39,A42 .= (fm.(s.n) ) * M.{s.n} by A23,A39,A42,A44,A43; end; now let y be object; assume y in rng xm; then consider n be Element of NAT such that A45: n in dom xm and A46: y=xm.n by PARTFUN1:3; reconsider z=M.{s.n} as Element of REAL by A8,A40,A13,A45; reconsider w=fm.(s.n) as Element of REAL by XREAL_0:def 1; xm.n = (fm.(s.n) ) * M.{s.n} by A41,A45 .= w*z by EXTREAL1:1; hence y in REAL by A46; end; then rng xm c= REAL; then reconsider xm1=xm as FinSequence of REAL by FINSEQ_1:def 4; A47: Sum(xp) = Sum(xp1) & Sum(xm) = Sum(xm1) by MESFUNC3:2; A48: for k be Nat st k in dom x1 holds (xp1 - xm1).k =x1.k proof let k be Nat; A49: f =fp-fm by MESFUNC6:42; assume A50: k in dom x1; then reconsider z=M.{s.k} as Element of REAL by A8,A10,A13; A51: xm1.k= (fm.(s.k) ) * M.{s.k} by A10,A40,A41,A50 .= (fm.(s.k) ) * z by EXTREAL1:1; s.k in rng s by A8,A10,A50,FUNCT_1:3; then s.k in Omega; then A52: s.k in dom f by FUNCT_2:def 1; k in (dom xp1) /\ (dom xm1) by A10,A31,A40,A50; then A53: k in dom (xp1 - xm1) by VALUED_1:12; xp1.k= (fp.(s.k) ) * M.{s.k} by A10,A31,A32,A50 .=(fp.(s.k) )*z by EXTREAL1:1; hence (xp1 - xm1).k = (fp.(s.k) ) * z - (fm.(s.k) ) * z by A53,A51, VALUED_1:13 .=( fp.(s.k) - (fm.(s.k)qua Real) ) * z .= (f.(s.k) ) * z by A52,A49,VALUED_1:13 .= (f.(s.k) ) * M.{s.k}by EXTREAL1:1 .=x1.k by A6,A50; end; dom fm = Omega by A11,RFUNCT_3:def 11; then A54: fm is_integrable_on M by A1,Lm5,Th6; A55: dom fp=dom f by RFUNCT_3:def 10; A56: dom (xp1-xm1) = (dom xp1) /\ (dom xm1) by VALUED_1:12 .= dom x1 by A10,A31,A40; A57: len xp1=L by A30,FINSEQ_1:def 3 .= len xm1 by A39,FINSEQ_1:def 3; dom ((-1)(#)fm) = dom fm by VALUED_1:def 5 .=Omega by A11,RFUNCT_3:def 11; then A58: E = Omega /\ Omega by A11,A26,RFUNCT_3:def 10 .= Omega; A59: Integral(M,fp+(-1)(#)fm) =Integral(M,fp) +Integral(M,(-1)(#)fm) by A27 ,A58 .=Integral(M,fp) +-Integral(M,fm) by A54,A28,MESFUNC6:102; fp is_simple_func_in Sigma & fp is nonnegative by Th6,MESFUNC6:61; then A60: Integral(M,fp)=Sum(xp) by A7,A55,A17,A20,A30,Lm1; thus Integral(M,f) =Integral(M,fp-fm) by MESFUNC6:42 .=Sum(xp) -Sum(xm) by A7,A24,A17,A23,A16,A39,A60,A59,Lm1 .=Sum(xp1) -Sum(xm1) by A47,SUPINF_2:3 .=Sum(xp1-xm1) by A57,INTEGRA5:2 .=Sum(x) by A56,A48,FINSEQ_1:13,MESFUNC3:2; 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 = (f.(s.n) qua ExtReal) * 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; set s=canFS(Omega); assume M.Omega < +infty; then A1: ex x being FinSequence of ExtREAL st len x = card (Omega) &( for n being Nat st n in dom x holds x.n = (f.((canFS(Omega)). n) qua ExtReal) * M .{(canFS(Omega) ).n})& Integral(M,f) =Sum x by Lm10; rng s = Omega & len s = card (Omega) by FINSEQ_1:93,FUNCT_2:def 3; hence thesis by A1; end; Lm11: 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); set M = P2M(P); A1: P.Omega in REAL by XREAL_0:def 1; then consider x being FinSequence of ExtREAL such that A2: len x = card (Omega) and A3: for n being Nat st n in dom x holds x.n = (f.((canFS(Omega)). n) qua ExtReal) * (P2M(P)).{(canFS(Omega)).n} and A4: Integral(P2M(P),f) = Sum x by Lm10,XXREAL_0:9; A5: (P2M(P)).Omega < +infty by A1,XXREAL_0:9; A6: 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:3; then A7: {(canFS(Omega)).n } c= Omega by ZFMISC_1:31; Omega in Sigma by MEASURE1:7; hence M.({(canFS(Omega)).n }) in REAL by A5,A7,Lm7; end; now let y be object; assume y in rng x; then consider n be Element of NAT such that A8: n in dom x and A9: y=x.n by PARTFUN1:3; Seg len x=Seg(len(canFS(Omega))) by A2,FINSEQ_1:93; then dom x = Seg (len (canFS(Omega))) by FINSEQ_1:def 3; then n in dom canFS(Omega) by A8,FINSEQ_1:def 3; then reconsider z=M.{(canFS(Omega)).n} as Element of REAL by A6; reconsider w=f.((canFS(Omega)).n) as Element of REAL by XREAL_0:def 1; x.n = (f.((canFS(Omega)).n) ) * M.{(canFS(Omega)).n} by A3,A8 .= w*z by EXTREAL1:1; hence y in REAL by A9; end; then rng x c= REAL; then reconsider F=x as FinSequence of REAL by FINSEQ_1:def 4; take F; for n being Nat st n in dom F holds F.n = (f.((canFS(Omega)).n)) * P.({(canFS(Omega)).n}) by A3; hence thesis by A2,A4,MESFUNC3:2; end; theorem Th12: 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 A1: len x = card (Omega) & s is one-to-one & rng s = Omega & len s = card (Omega) and A2: for n being Nat st n in dom x holds x.n = f.(s.n) * P.{s.n}; set M = P2M(P); rng x c= ExtREAL by NUMBERS:31; then reconsider x1= x as FinSequence of ExtREAL by FINSEQ_1:def 4; A3: for n being Nat st n in dom x1 holds x1.n = (f.(s.n) ) * (P2M(P)).{s.n} by A2; P.Omega in REAL by XREAL_0:def 1; then Integral(M,f) =Sum x1 by A1,A3,Th10,XXREAL_0:9 .=Sum x by MESFUNC3:2; hence thesis; end; theorem Th13: 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 s=canFS(Omega); A1: len s = card Omega by FINSEQ_1:93; (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 )& rng s = Omega by Lm11,FUNCT_2:def 3; hence thesis by A1; end; theorem Th14: for E be finite non empty set, ASeq being SetSequence of E st ASeq is non-ascending ex N be Nat st for m be Nat st N<=m holds ASeq.N = ASeq.m proof let E be finite non empty set, ASeq being SetSequence of E; defpred P[Element of NAT,set] means $2=card(ASeq.$1 ); A1: 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 REAL by NUMBERS:19; hence thesis; end; consider seq being sequence of REAL such that A2: for n being Element of NAT holds P[n,seq.n] from FUNCT_2:sch 3(A1); now let m be Nat; reconsider mm=m as Element of NAT by ORDINAL1:def 12; seq.mm = card(ASeq.mm) by A2; hence -1 < seq.m; end; then A3: seq is bounded_below by SEQ_2:def 4; assume A4: ASeq is non-ascending; A5: now let n,m be Nat; assume n <= m; then A6: ASeq.m c= ASeq.n by A4,PROB_1:def 4; reconsider mm=m, nn=n as Element of NAT by ORDINAL1:def 12; seq.mm = card(ASeq.mm) & seq.nn = card(ASeq.nn) by A2; hence seq.m <=seq.n by A6,NAT_1:43; end; then seq is non-increasing by SEQM_3:8; then consider g be Real such that A7: for p be Real st 0
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 registration let Omega,Sigma; cluster ([#]Sigma)-measurable for Function of Omega,REAL; existence 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 X-measurable by MESFUNC2:29; then f is X-measurable; hence thesis; end; end; definition let Omega,Sigma; mode Real-Valued-Random-Variable of Sigma is ([#]Sigma)-measurable Function of Omega,REAL; end; reserve f,g for Real-Valued-Random-Variable of Sigma; theorem Th18: f+g is Real-Valued-Random-Variable of Sigma proof f+g is ([#]Sigma)-measurable by MESFUNC6:26; hence thesis; 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 set Y = [#]Sigma; dom g = Y by FUNCT_2:def 1; then f-g is ([#]Sigma)-measurable by MESFUNC6:29; hence thesis; 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; dom f = X by FUNCT_2:def 1; then r(#)f is X-measurable by MESFUNC6:21; hence thesis; 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 X-measurable; A3: R_EAL f is X-measurable 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 ([#]Sigma)-measurable; then R_EAL g is X-measurable; then (R_EAL f)(#)(R_EAL g) is X-measurable by A3,A4,MESFUNC7:15; then R_EAL(f(#)g) is X-measurable by Th21; then f(#)g is X-measurable; hence thesis; 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; dom f = [#]Sigma by FUNCT_2:def 1; then (f to_power r) is ([#]Sigma)-measurable by A1,MESFUN6C:29; hence thesis by A3; 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 ([#]Sigma)-measurable; dom f = [#]Sigma & R_EAL f is ([#]Sigma)-measurable by A2,FUNCT_2:def 1; then |.R_EAL f.| is ([#]Sigma)-measurable by MESFUNC2:27; then R_EAL abs(f) is ([#]Sigma)-measurable by MESFUNC6:1; then abs(f) is ([#]Sigma)-measurable; hence thesis; 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 X-measurable by Th8; A2: f is X-measurable & dom f = Omega by FUNCT_2:def 1,A1; X = [#]Sigma by A1,A2; hence thesis by 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; 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 A7,MESFUNC6:13; Integral(PM,X|K) <= Integral(PM,X|S) by A2,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;