:: RANDOM_1 semantic presentation begin theorem Th1: :: RANDOM_1:1 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,ExtREAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being 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 ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,ExtREAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) holds (R_EAL a) * (M . E) <= Integral (M,(f | E)) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,ExtREAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) holds (R_EAL a) * (M . E) <= Integral (M,(f | E)) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,ExtREAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) holds (R_EAL a) * (M . E) <= Integral (M,(f | E)) let f be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) holds (R_EAL a) * (M . E) <= Integral (M,(f | E)) let E be Element of S; ::_thesis: for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) holds (R_EAL a) * (M . E) <= Integral (M,(f | E)) let a be Real; ::_thesis: ( f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) implies (R_EAL a) * (M . E) <= Integral (M,(f | E)) ) assume that A1: f is_integrable_on M and A2: E c= dom f and A3: M . E < +infty and A4: for x being Element of X st x in E holds a <= f . x ; ::_thesis: (R_EAL a) * (M . E) <= Integral (M,(f | E)) set C = chi (E,X); A5: f | E is_integrable_on M by A1, MESFUNC5:97; for x being Element of X st x in dom (a (#) ((chi (E,X)) | E)) holds (a (#) ((chi (E,X)) | E)) . x <= (f | E) . x proof let x be Element of X; ::_thesis: ( x in dom (a (#) ((chi (E,X)) | E)) implies (a (#) ((chi (E,X)) | E)) . x <= (f | E) . x ) assume A6: x in dom (a (#) ((chi (E,X)) | E)) ; ::_thesis: (a (#) ((chi (E,X)) | E)) . x <= (f | E) . x then A7: x in dom ((chi (E,X)) | E) by MESFUNC1:def_6; then x in (dom (chi (E,X))) /\ 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 (#) ((chi (E,X)) | E)) . x = (R_EAL a) * (((chi (E,X)) | E) . x) by A6, MESFUNC1:def_6 .= (R_EAL a) * ((chi (E,X)) . x) by A7, FUNCT_1:47 .= (R_EAL a) * 1. by A8, FUNCT_3:def_3 ; hence (a (#) ((chi (E,X)) | E)) . x <= (f | E) . x by A9, XXREAL_3:81; ::_thesis: verum end; then A10: (f | E) - (a (#) ((chi (E,X)) | E)) is nonnegative by MESFUNC7:1; dom (a (#) ((chi (E,X)) | E)) = dom ((chi (E,X)) | E) by MESFUNC1:def_6; then dom (a (#) ((chi (E,X)) | E)) = (dom (chi (E,X))) /\ E by RELAT_1:61; then dom (a (#) ((chi (E,X)) | E)) = X /\ E by FUNCT_3:def_3; then A11: dom (a (#) ((chi (E,X)) | E)) = E by XBOOLE_1:28; E = E /\ E ; then A12: Integral (M,((chi (E,X)) | E)) = M . E by A3, MESFUNC7:25; chi (E,X) is_integrable_on M by A3, MESFUNC7:24; then A13: (chi (E,X)) | E is_integrable_on M by MESFUNC5:97; then a (#) ((chi (E,X)) | E) is_integrable_on M by MESFUNC5:110; then consider E1 being Element of S such that A14: E1 = (dom (f | E)) /\ (dom (a (#) ((chi (E,X)) | E))) and A15: Integral (M,((a (#) ((chi (E,X)) | 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 (#) ((chi (E,X)) | E)) | E1 = a (#) ((chi (E,X)) | E) & (f | E) | E1 = f | E ) by A14, A11, RELAT_1:69; hence (R_EAL a) * (M . E) <= Integral (M,(f | E)) by A13, A15, A12, MESFUNC5:110; ::_thesis: verum end; theorem Th2: :: RANDOM_1:2 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being 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 ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) holds (R_EAL a) * (M . E) <= Integral (M,(f | E)) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) holds (R_EAL a) * (M . E) <= Integral (M,(f | E)) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) holds (R_EAL a) * (M . E) <= Integral (M,(f | E)) let f be PartFunc of X,REAL; ::_thesis: for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) holds (R_EAL a) * (M . E) <= Integral (M,(f | E)) let E be Element of S; ::_thesis: for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) holds (R_EAL a) * (M . E) <= Integral (M,(f | E)) let a be Real; ::_thesis: ( f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) implies (R_EAL a) * (M . E) <= Integral (M,(f | E)) ) assume f is_integrable_on M ; ::_thesis: ( not E c= dom f or not M . E < +infty or ex x being Element of X st ( x in E & not a <= f . x ) or (R_EAL a) * (M . E) <= Integral (M,(f | E)) ) then R_EAL f is_integrable_on M by MESFUNC6:def_4; hence ( not E c= dom f or not M . E < +infty or ex x being Element of X st ( x in E & not a <= f . x ) or (R_EAL a) * (M . E) <= Integral (M,(f | E)) ) by Th1; ::_thesis: verum end; theorem Th3: :: RANDOM_1:3 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,ExtREAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being 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 ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,ExtREAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) holds Integral (M,(f | E)) <= (R_EAL a) * (M . E) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,ExtREAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) holds Integral (M,(f | E)) <= (R_EAL a) * (M . E) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,ExtREAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) holds Integral (M,(f | E)) <= (R_EAL a) * (M . E) let f be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) holds Integral (M,(f | E)) <= (R_EAL a) * (M . E) let E be Element of S; ::_thesis: for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) holds Integral (M,(f | E)) <= (R_EAL a) * (M . E) let a be Real; ::_thesis: ( f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) implies Integral (M,(f | E)) <= (R_EAL a) * (M . E) ) assume that A1: f is_integrable_on M and A2: E c= dom f and A3: M . E < +infty and A4: for x being Element of X st x in E holds f . x <= a ; ::_thesis: Integral (M,(f | E)) <= (R_EAL a) * (M . E) set C = chi (E,X); A5: f | E is_integrable_on M by A1, MESFUNC5:97; dom (a (#) ((chi (E,X)) | E)) = dom ((chi (E,X)) | E) by MESFUNC1:def_6; then dom (a (#) ((chi (E,X)) | E)) = (dom (chi (E,X))) /\ E by RELAT_1:61; then dom (a (#) ((chi (E,X)) | E)) = X /\ E by FUNCT_3:def_3; then A6: dom (a (#) ((chi (E,X)) | 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 being Element of X st x in dom (f | E) holds (f | E) . x <= (a (#) ((chi (E,X)) | E)) . x proof let x be Element of X; ::_thesis: ( x in dom (f | E) implies (f | E) . x <= (a (#) ((chi (E,X)) | E)) . x ) assume A8: x in dom (f | E) ; ::_thesis: (f | E) . x <= (a (#) ((chi (E,X)) | E)) . x then A9: x in dom ((chi (E,X)) | E) by A7, A6, MESFUNC1:def_6; then x in (dom (chi (E,X))) /\ 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 (#) ((chi (E,X)) | E)) . x = (R_EAL a) * (((chi (E,X)) | E) . x) by A7, A6, A8, MESFUNC1:def_6 .= (R_EAL a) * ((chi (E,X)) . x) by A9, FUNCT_1:47 .= (R_EAL a) * 1. by A10, FUNCT_3:def_3 ; hence (f | E) . x <= (a (#) ((chi (E,X)) | E)) . x by A11, XXREAL_3:81; ::_thesis: verum end; then A12: (a (#) ((chi (E,X)) | E)) - (f | E) is nonnegative by MESFUNC7:1; dom (a (#) ((chi (E,X)) | E)) = dom ((chi (E,X)) | E) by MESFUNC1:def_6; then dom (a (#) ((chi (E,X)) | E)) = (dom (chi (E,X))) /\ E by RELAT_1:61; then dom (a (#) ((chi (E,X)) | E)) = X /\ E by FUNCT_3:def_3; then A13: dom (a (#) ((chi (E,X)) | E)) = E by XBOOLE_1:28; E = E /\ E ; then A14: Integral (M,((chi (E,X)) | E)) = M . E by A3, MESFUNC7:25; chi (E,X) is_integrable_on M by A3, MESFUNC7:24; then A15: (chi (E,X)) | E is_integrable_on M by MESFUNC5:97; then a (#) ((chi (E,X)) | E) is_integrable_on M by MESFUNC5:110; then consider E1 being Element of S such that A16: E1 = (dom (f | E)) /\ (dom (a (#) ((chi (E,X)) | E))) and A17: Integral (M,((f | E) | E1)) <= Integral (M,((a (#) ((chi (E,X)) | 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 (#) ((chi (E,X)) | E)) | E1 = a (#) ((chi (E,X)) | E) & (f | E) | E1 = f | E ) by A16, A13, RELAT_1:69; hence Integral (M,(f | E)) <= (R_EAL a) * (M . E) by A15, A17, A14, MESFUNC5:110; ::_thesis: verum end; theorem :: RANDOM_1:4 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being 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 ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) holds Integral (M,(f | E)) <= (R_EAL a) * (M . E) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) holds Integral (M,(f | E)) <= (R_EAL a) * (M . E) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) holds Integral (M,(f | E)) <= (R_EAL a) * (M . E) let f be PartFunc of X,REAL; ::_thesis: for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) holds Integral (M,(f | E)) <= (R_EAL a) * (M . E) let E be Element of S; ::_thesis: for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) holds Integral (M,(f | E)) <= (R_EAL a) * (M . E) let a be Real; ::_thesis: ( f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) implies Integral (M,(f | E)) <= (R_EAL a) * (M . E) ) assume f is_integrable_on M ; ::_thesis: ( not E c= dom f or not M . E < +infty or ex x being Element of X st ( x in E & not f . x <= a ) or Integral (M,(f | E)) <= (R_EAL a) * (M . E) ) then R_EAL f is_integrable_on M by MESFUNC6:def_4; hence ( not E c= dom f or not M . E < +infty or ex x being Element of X st ( x in E & not f . x <= a ) or Integral (M,(f | E)) <= (R_EAL a) * (M . E) ) by Th3; ::_thesis: verum end; Lm1: for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for M being sigma_Measure of S for F being Finite_Sep_Sequence of S for a being FinSequence of REAL for x being 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 being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & dom x = dom F & ( for n being 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 ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for M being sigma_Measure of S for F being Finite_Sep_Sequence of S for a being FinSequence of REAL for x being 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 being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (R_EAL (a . n)) * ((M * F) . n) ) holds Integral (M,f) = Sum x let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for M being sigma_Measure of S for F being Finite_Sep_Sequence of S for a being FinSequence of REAL for x being 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 being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (R_EAL (a . n)) * ((M * F) . n) ) holds Integral (M,f) = Sum x let f be PartFunc of X,REAL; ::_thesis: for M being sigma_Measure of S for F being Finite_Sep_Sequence of S for a being FinSequence of REAL for x being 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 being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (R_EAL (a . n)) * ((M * F) . n) ) holds Integral (M,f) = Sum x let M be sigma_Measure of S; ::_thesis: for F being Finite_Sep_Sequence of S for a being FinSequence of REAL for x being 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 being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (R_EAL (a . n)) * ((M * F) . n) ) holds Integral (M,f) = Sum x let F be Finite_Sep_Sequence of S; ::_thesis: for a being FinSequence of REAL for x being 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 being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (R_EAL (a . n)) * ((M * F) . n) ) holds Integral (M,f) = Sum x let a be FinSequence of REAL ; ::_thesis: for x being 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 being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (R_EAL (a . n)) * ((M * F) . n) ) holds Integral (M,f) = Sum x let x be FinSequence of ExtREAL ; ::_thesis: ( f is_simple_func_in S & dom f <> {} & f is nonnegative & dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (R_EAL (a . n)) * ((M * F) . n) ) implies Integral (M,f) = Sum x ) 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 being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) and A5: dom x = dom F and A6: for n being Nat st n in dom x holds x . n = (R_EAL (a . n)) * ((M * F) . n) ; ::_thesis: Integral (M,f) = Sum x A7: ( R_EAL f is_simple_func_in S & ( for x being set st x in dom (R_EAL f) holds 0 <= (R_EAL f) . x ) ) by A1, A3, MESFUNC6:49, MESFUNC6: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 being Nat st n in dom x holds x . n = (a0 . n) * ((M * F) . n) proof let n be Nat; ::_thesis: ( n in dom x implies x . n = (a0 . n) * ((M * F) . n) ) assume n in dom x ; ::_thesis: x . n = (a0 . n) * ((M * F) . n) then x . n = (R_EAL (a . n)) * ((M * F) . n) by A6; hence x . n = (a0 . n) * ((M * F) . n) ; ::_thesis: verum end; thus Integral (M,f) = integral' (M,(R_EAL f)) by A1, A3, MESFUNC6:83 .= integral (X,S,M,(R_EAL f)) by A2, MESFUNC5:def_14 .= Sum x by A2, A5, A7, A8, A9, MESFUNC4:3 ; ::_thesis: verum end; Lm2: for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL st f is_simple_func_in S holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of REAL st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL st f is_simple_func_in S holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of REAL st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL st f is_simple_func_in S holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of REAL st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) let f be PartFunc of X,REAL; ::_thesis: ( f is_simple_func_in S implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of REAL st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) ) assume f is_simple_func_in S ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of REAL st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) then consider F being Finite_Sep_Sequence of S such that A1: dom f = union (rng F) and A2: for n being Nat for 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_2; defpred S1[ Nat, Element of REAL ] means for x being set st x in F . $1 holds $2 = f . x; A3: for k being Nat st k in Seg (len F) holds ex y being Element of REAL st S1[k,y] proof let k be Nat; ::_thesis: ( k in Seg (len F) implies ex y being Element of REAL st S1[k,y] ) assume k in Seg (len F) ; ::_thesis: ex y being Element of REAL st S1[k,y] then A4: k in dom F by FINSEQ_1:def_3; then A5: F . k in rng F by FUNCT_1:3; percases ( F . k = {} or F . k <> {} ) ; supposeA6: F . k = {} ; ::_thesis: ex y being Element of REAL st S1[k,y] take 0 ; ::_thesis: S1[k, 0 ] thus S1[k, 0 ] by A6; ::_thesis: verum end; suppose F . k <> {} ; ::_thesis: ex y being Element of REAL st S1[k,y] then consider x1 being set such that A7: x1 in F . k by XBOOLE_0:def_1; take f . x1 ; ::_thesis: S1[k,f . x1] rng F c= bool X by XBOOLE_1:1; hence S1[k,f . x1] by A2, A4, A5, A7; ::_thesis: verum end; end; end; consider a being FinSequence of REAL such that A8: ( dom a = Seg (len F) & ( for k being Nat st k in Seg (len F) holds S1[k,a . k] ) ) from FINSEQ_1:sch_5(A3); take F ; ::_thesis: ex a being FinSequence of REAL st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) take a ; ::_thesis: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) for n being Nat st n in dom F holds for x being set st x in F . n holds a . n = f . x proof let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds a . n = f . x ) assume n in dom F ; ::_thesis: for x being set st x in F . n holds a . n = f . x then n in Seg (len F) by FINSEQ_1:def_3; hence for x being set st x in F . n holds a . n = f . x by A8; ::_thesis: verum end; hence ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) by A1, A8, FINSEQ_1:def_3; ::_thesis: verum end; Lm3: for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL st f is_simple_func_in S holds rng f is real-bounded proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL st f is_simple_func_in S holds rng f is real-bounded let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL st f is_simple_func_in S holds rng f is real-bounded let f be PartFunc of X,REAL; ::_thesis: ( f is_simple_func_in S implies rng f is real-bounded ) assume f is_simple_func_in S ; ::_thesis: rng f is real-bounded then consider F being Finite_Sep_Sequence of S, a being FinSequence of REAL such that A1: dom f = union (rng F) and A2: dom F = dom a and A3: for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n by Lm2; rng f c= rng a proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in rng a ) assume y in rng f ; ::_thesis: y in rng a then consider x being set such that A4: x in dom f and A5: y = f . x by FUNCT_1:def_3; consider z being set such that A6: x in z and A7: z in rng F by A1, A4, TARSKI:def_4; consider n being set 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; ::_thesis: verum end; hence rng f is real-bounded by RCOMP_1:10; ::_thesis: verum end; Lm4: for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL st dom f <> {} & rng f is real-bounded & M . (dom f) < +infty & ex E being 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 ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL st dom f <> {} & rng f is real-bounded & M . (dom f) < +infty & ex E being Element of S st ( E = dom f & f is_measurable_on E ) holds f is_integrable_on M let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL st dom f <> {} & rng f is real-bounded & M . (dom f) < +infty & ex E being Element of S st ( E = dom f & f is_measurable_on E ) holds f is_integrable_on M let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st dom f <> {} & rng f is real-bounded & M . (dom f) < +infty & ex E being Element of S st ( E = dom f & f is_measurable_on E ) holds f is_integrable_on M let f be PartFunc of X,REAL; ::_thesis: ( dom f <> {} & rng f is real-bounded & M . (dom f) < +infty & ex E being Element of S st ( E = dom f & f is_measurable_on E ) implies f is_integrable_on M ) assume that A1: dom f <> {} and A2: rng f is real-bounded and A3: M . (dom f) < +infty and A4: ex E being Element of S st ( E = dom f & f is_measurable_on E ) ; ::_thesis: f is_integrable_on M consider E being Element of S such that A5: E = dom f and A6: f is_measurable_on E 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 V63() & (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__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ (((R_EAL_f)_(#)_(chi_(E,X)))_|_E)_._x_=_f_._x let x be set ; ::_thesis: ( x in dom f implies (((R_EAL f) (#) (chi (E,X))) | E) . x = f . x ) assume A11: x in dom f ; ::_thesis: (((R_EAL f) (#) (chi (E,X))) | E) . x = f . x 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) * (R_EAL 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, RELAT_1:68; ::_thesis: verum end; A12: R_EAL f is_measurable_on E by A6, MESFUNC6:def_1; 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, RELAT_1:62; 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 f is_integrable_on M by A14, MESFUNC6:def_4; ::_thesis: verum end; Lm5: for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being 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 ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f being 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 let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being 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 let M be sigma_Measure of S; ::_thesis: for f being 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 let f be PartFunc of X,REAL; ::_thesis: ( f is_simple_func_in S & dom f <> {} & dom f in S & M . (dom f) < +infty implies f is_integrable_on M ) assume A1: f is_simple_func_in S ; ::_thesis: ( not dom f <> {} or not dom f in S or not M . (dom f) < +infty or f is_integrable_on M ) then rng f is real-bounded by Lm3; hence ( not dom f <> {} or not dom f in S or not M . (dom f) < +infty or f is_integrable_on M ) by A1, Lm4, MESFUNC6:50; ::_thesis: verum end; begin notation let E be non empty set ; synonym Trivial-SigmaField E for bool E; end; definition let E be non empty set ; :: original: Trivial-SigmaField redefine func Trivial-SigmaField E -> SigmaField of E; correctness coherence Trivial-SigmaField E is SigmaField of E; by PROB_1:40; end; Lm6: for Omega being non empty finite set for f being PartFunc of Omega,REAL ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega st ( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being 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 ; ::_thesis: for f being PartFunc of Omega,REAL ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega st ( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being 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 ) ) let f be PartFunc of Omega,REAL; ::_thesis: ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega st ( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being 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 ) ) set Sigma = Trivial-SigmaField Omega; set D = dom f; defpred S1[ Nat, set ] means $2 = {((canFS (dom f)) . $1)}; set L = len (canFS (dom f)); A1: for k being Nat st k in Seg (len (canFS (dom f))) holds ex x being Element of bool Omega st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len (canFS (dom f))) implies ex x being Element of bool Omega st S1[k,x] ) assume A2: k in Seg (len (canFS (dom f))) ; ::_thesis: ex x being Element of bool Omega st S1[k,x] take {((canFS (dom f)) . k)} ; ::_thesis: ( {((canFS (dom f)) . k)} is Element of bool Omega & S1[k,{((canFS (dom f)) . k)}] ) k in dom (canFS (dom f)) by A2, FINSEQ_1:def_3; then (canFS (dom f)) . k in rng (canFS (dom f)) by FUNCT_1:3; then (canFS (dom f)) . k in dom f ; hence ( {((canFS (dom f)) . k)} is Element of bool Omega & S1[k,{((canFS (dom f)) . k)}] ) by ZFMISC_1:31; ::_thesis: verum end; consider F being FinSequence of bool Omega such that A3: ( dom F = Seg (len (canFS (dom f))) & ( for k being Nat st k in Seg (len (canFS (dom f))) holds S1[k,F . k] ) ) from FINSEQ_1:sch_5(A1); now__::_thesis:_for_i,_j_being_Nat_st_i_in_dom_F_&_j_in_dom_F_&_i_<>_j_holds_ F_._i_misses_F_._j let i, j be Nat; ::_thesis: ( i in dom F & j in dom F & i <> j implies F . i misses F . j ) assume that A4: ( i in dom F & j in dom F ) and A5: i <> j ; ::_thesis: F . i misses F . j ( i in dom (canFS (dom f)) & j in dom (canFS (dom f)) ) by A3, A4, FINSEQ_1:def_3; then A6: (canFS (dom f)) . i <> (canFS (dom f)) . j by A5, FUNCT_1:def_4; ( F . i = {((canFS (dom f)) . i)} & F . j = {((canFS (dom f)) . j)} ) by A3, A4; hence F . i misses F . j by A6, ZFMISC_1:11; ::_thesis: verum end; then reconsider F = F as Finite_Sep_Sequence of Trivial-SigmaField Omega by MESFUNC3:4; now__::_thesis:_for_x_being_set_st_x_in_rng_(canFS_(dom_f))_holds_ x_in_union_(rng_F) let x be set ; ::_thesis: ( x in rng (canFS (dom f)) implies x in union (rng F) ) assume x in rng (canFS (dom f)) ; ::_thesis: x in union (rng F) then consider n being set such that A7: n in dom (canFS (dom f)) and A8: x = (canFS (dom f)) . n by FUNCT_1:def_3; A9: n in Seg (len (canFS (dom f))) by A7, FINSEQ_1:def_3; reconsider n = 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 (dom f)) . 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; ::_thesis: verum end; then A11: rng (canFS (dom f)) c= union (rng F) by TARSKI:def_3; take F ; ::_thesis: ( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being 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 ) ) 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; ::_thesis: 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 let x, y be Element of Omega; ::_thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y ) assume that A13: n in dom F and A14: x in F . n and A15: y in F . n ; ::_thesis: f . x = f . y A16: F . n = {((canFS (dom f)) . n)} by A3, A13; hence f . x = f . ((canFS (dom f)) . n) by A14, TARSKI:def_1 .= f . y by A15, A16, TARSKI:def_1 ; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_union_(rng_F)_holds_ x_in_rng_(canFS_(dom_f)) let x be set ; ::_thesis: ( x in union (rng F) implies x in rng (canFS (dom f)) ) assume x in union (rng F) ; ::_thesis: x in rng (canFS (dom f)) then consider y being set such that A17: x in y and A18: y in rng F by TARSKI:def_4; consider n being set such that A19: n in dom F and A20: y = F . n by A18, FUNCT_1:def_3; reconsider n = n as Element of NAT by A19; F . n = {((canFS (dom f)) . n)} by A3, A19; then A21: x = (canFS (dom f)) . n by A17, A20, TARSKI:def_1; n in dom (canFS (dom f)) by A3, A19, FINSEQ_1:def_3; hence x in rng (canFS (dom f)) by A21, FUNCT_1:def_3; ::_thesis: verum end; then union (rng F) c= rng (canFS (dom f)) by TARSKI:def_3; then union (rng F) = rng (canFS (dom f)) by A11, XBOOLE_0:def_10; hence ( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being 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 ) ) by A3, A12, FINSEQ_1:def_3, FUNCT_2:def_3; ::_thesis: verum end; theorem :: RANDOM_1:5 for Omega being non empty finite set for f being PartFunc of Omega,REAL ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex 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 being 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 ; ::_thesis: for f being PartFunc of Omega,REAL ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex 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 being 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 ) ) let f be PartFunc of Omega,REAL; ::_thesis: ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex 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 being 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 ) ) set Sigma = Trivial-SigmaField Omega; set D = dom f; set s = canFS (dom f); A1: len (canFS (dom f)) = card (dom f) by UPROOTS:3; ( ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega st ( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being 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 ) ) & rng (canFS (dom f)) = dom f ) by Lm6, FUNCT_2:def_3; hence ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex 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 being 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 A1; ::_thesis: verum end; theorem Th6: :: RANDOM_1:6 for Omega being non empty finite set for f being 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 ; ::_thesis: for f being PartFunc of Omega,REAL holds ( f is_simple_func_in Trivial-SigmaField Omega & dom f is Element of Trivial-SigmaField Omega ) let f be PartFunc of Omega,REAL; ::_thesis: ( f is_simple_func_in Trivial-SigmaField Omega & dom f is Element of Trivial-SigmaField Omega ) set Sigma = Trivial-SigmaField Omega; set D = dom f; ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega st ( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being 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 ) ) by Lm6; hence ( f is_simple_func_in Trivial-SigmaField Omega & dom f is Element of Trivial-SigmaField Omega ) by MESFUNC6:def_2; ::_thesis: verum end; theorem :: RANDOM_1:7 for Omega being non empty finite set for M being sigma_Measure of (Trivial-SigmaField Omega) for f being PartFunc of Omega,REAL st dom f <> {} & M . (dom f) < +infty holds f is_integrable_on M by Lm5, Th6; Lm7: for Omega being non empty set for Sigma being SigmaField of Omega for M being sigma_Measure of Sigma for A, B being 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 ; ::_thesis: for Sigma being SigmaField of Omega for M being sigma_Measure of Sigma for A, B being set st A in Sigma & B in Sigma & A c= B & M . B < +infty holds M . A in REAL let Sigma be SigmaField of Omega; ::_thesis: for M being sigma_Measure of Sigma for A, B being set st A in Sigma & B in Sigma & A c= B & M . B < +infty holds M . A in REAL let M be sigma_Measure of Sigma; ::_thesis: for A, B being set st A in Sigma & B in Sigma & A c= B & M . B < +infty holds M . A in REAL let A, B be set ; ::_thesis: ( A in Sigma & B in Sigma & A c= B & M . B < +infty implies M . A in REAL ) assume ( A in Sigma & B in Sigma & A c= B & M . B < +infty ) ; ::_thesis: M . A in REAL then ( M . A <> -infty & M . A <> +infty ) by MEASURE1:31, MEASURE1:def_2; hence M . A in REAL by XXREAL_0:14; ::_thesis: verum end; Lm8: for Omega being non empty finite set for f being PartFunc of Omega,REAL holds f * (canFS (dom f)) is FinSequence of REAL proof let Omega be non empty finite set ; ::_thesis: for f being PartFunc of Omega,REAL holds f * (canFS (dom f)) is FinSequence of REAL let f be PartFunc of Omega,REAL; ::_thesis: f * (canFS (dom f)) is FinSequence of 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; ::_thesis: verum end; Lm9: for Omega being non empty finite set for f being PartFunc of Omega,REAL holds dom (f * (canFS (dom f))) = dom (canFS (dom f)) proof let Omega be non empty finite set ; ::_thesis: for f being PartFunc of Omega,REAL holds dom (f * (canFS (dom f))) = dom (canFS (dom f)) let f be PartFunc of Omega,REAL; ::_thesis: dom (f * (canFS (dom f))) = dom (canFS (dom f)) rng (canFS (dom f)) c= dom f ; hence dom (f * (canFS (dom f))) = dom (canFS (dom f)) by RELAT_1:27; ::_thesis: verum end; theorem Th8: :: RANDOM_1:8 for Omega being non empty finite set for f being PartFunc of Omega,REAL ex X being Element of Trivial-SigmaField Omega st ( dom f = X & f is_measurable_on X ) proof let Omega be non empty finite set ; ::_thesis: for f being PartFunc of Omega,REAL ex X being Element of Trivial-SigmaField Omega st ( dom f = X & f is_measurable_on X ) let f be PartFunc of Omega,REAL; ::_thesis: ex X being Element of Trivial-SigmaField Omega st ( dom f = X & f is_measurable_on X ) set Sigma = Trivial-SigmaField Omega; reconsider X = dom f as Element of Trivial-SigmaField Omega ; take X ; ::_thesis: ( dom f = X & f is_measurable_on X ) thus ( dom f = X & f is_measurable_on X ) by Th6, MESFUNC6:50; ::_thesis: verum end; Lm10: for Omega being non empty finite set for M being sigma_Measure of (Trivial-SigmaField Omega) for f being 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 ; ::_thesis: for M being sigma_Measure of (Trivial-SigmaField Omega) for f being 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 ) let M be sigma_Measure of (Trivial-SigmaField Omega); ::_thesis: for f being 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 ) let f be Function of Omega,REAL; ::_thesis: ( M . Omega < +infty implies 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 ) ) set fm = max- f; set Dm = dom (max- f); reconsider am = (max- f) * (canFS (dom (max- f))) as FinSequence of REAL by Lm8; set fp = max+ f; set Dp = dom (max+ f); reconsider ap = (max+ f) * (canFS (dom (max+ f))) as FinSequence of REAL by Lm8; set Sigma = Trivial-SigmaField Omega; set D = dom f; consider F being Finite_Sep_Sequence of Trivial-SigmaField Omega such that dom f = union (rng F) and A1: dom F = dom (canFS (dom f)) and A2: for k being Nat st k in dom F holds F . k = {((canFS (dom f)) . 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 being Finite_Sep_Sequence of Trivial-SigmaField Omega such that A3: dom (max+ f) = union (rng Fp) and A4: dom Fp = dom (canFS (dom (max+ f))) and A5: for k being Nat st k in dom Fp holds Fp . k = {((canFS (dom (max+ f))) . 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 (max+ f) . x = (max+ f) . y by Lm6; defpred S1[ Nat, set ] means $2 = (R_EAL (ap . $1)) * ((M * Fp) . $1); A6: for k being Nat st k in Seg (len F) holds ex x being Element of ExtREAL st S1[k,x] ; consider xp being FinSequence of ExtREAL such that A7: ( dom xp = Seg (len F) & ( for k being Nat st k in Seg (len F) holds S1[k,xp . k] ) ) from FINSEQ_1:sch_5(A6); A8: dom Fp = dom ap by A4, Lm9; A9: for n being Nat st n in dom Fp holds for x being set st x in Fp . n holds (max+ f) . x = ap . n proof let n be Nat; ::_thesis: ( n in dom Fp implies for x being set st x in Fp . n holds (max+ f) . x = ap . n ) assume A10: n in dom Fp ; ::_thesis: for x being set st x in Fp . n holds (max+ f) . x = ap . n let x be set ; ::_thesis: ( x in Fp . n implies (max+ f) . x = ap . n ) assume x in Fp . n ; ::_thesis: (max+ f) . x = ap . n then x in {((canFS (dom (max+ f))) . n)} by A5, A10; then x = (canFS (dom (max+ f))) . n by TARSKI:def_1; hence (max+ f) . x = ap . n by A8, A10, FUNCT_1:12; ::_thesis: verum end; reconsider a = f * (canFS (dom f)) as FinSequence of REAL by Lm8; A11: (R_EAL (- 1)) * (Integral (M,(max- f))) = (- (R_EAL 1)) * (Integral (M,(max- f))) by SUPINF_2:2 .= - ((R_EAL 1) * (Integral (M,(max- f)))) by XXREAL_3:92 .= - (Integral (M,(max- f))) by XXREAL_3:81 ; defpred S2[ Nat, set ] means $2 = (R_EAL (a . $1)) * ((M * F) . $1); A12: for k being Nat st k in Seg (len F) holds ex x being Element of ExtREAL st S2[k,x] ; consider x being FinSequence of ExtREAL such that A13: ( dom x = Seg (len F) & ( for k being Nat st k in Seg (len F) holds S2[k,x . k] ) ) from FINSEQ_1:sch_5(A12); assume A14: M . Omega < +infty ; ::_thesis: 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 ) A15: for n being Nat st n in dom (canFS Omega) holds M . {((canFS Omega) . n)} in REAL proof let n be Nat; ::_thesis: ( n in dom (canFS Omega) implies M . {((canFS Omega) . n)} in REAL ) assume n in dom (canFS Omega) ; ::_thesis: M . {((canFS Omega) . n)} in REAL 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 Trivial-SigmaField Omega by MEASURE1:7; hence M . {((canFS Omega) . n)} in REAL by A14, A16, Lm7; ::_thesis: verum end; A17: dom f = Omega by FUNCT_2:def_1; then A18: dom (max- f) = Omega by RFUNCT_3:def_11; then A19: max- f 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 = (R_EAL (f . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) proof let n be Nat; ::_thesis: ( n in dom x implies x . n = (R_EAL (f . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) ) assume A22: n in dom x ; ::_thesis: x . n = (R_EAL (f . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) 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 (dom f)) . n) = a . n by A1, A20, A22, FUNCT_1:13; thus x . n = (R_EAL (a . n)) * ((M * F) . n) by A13, A22 .= (R_EAL (f . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by A24, A23, FUNCT_2:def_1 ; ::_thesis: verum end; x is FinSequence of REAL proof let y be set ; :: according to TARSKI:def_3,FINSEQ_1:def_4 ::_thesis: ( not y in rng x or y in REAL ) assume y in rng x ; ::_thesis: y in REAL then consider n being 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 ; x . n = (R_EAL (f . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by A21, A25 .= w * z by EXTREAL1:1 ; hence y in REAL by A26; ::_thesis: verum end; then reconsider x1 = x as FinSequence of REAL ; take x ; ::_thesis: ( 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 ) A27: ( max- f is_simple_func_in Trivial-SigmaField Omega & max- f 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: dom (max+ f) = dom f by RFUNCT_3:def_10; A31: for n being Nat st n in dom xp holds xp . n = (R_EAL ((max+ f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) proof let n be Nat; ::_thesis: ( n in dom xp implies xp . n = (R_EAL ((max+ f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) ) assume A32: n in dom xp ; ::_thesis: xp . n = (R_EAL ((max+ f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) then A33: (M * Fp) . n = M . (Fp . n) by A29, FUNCT_1:13 .= M . {((canFS Omega) . n)} by A17, A5, A30, A29, A32 ; A34: (max+ f) . ((canFS (dom f)) . n) = ap . n by A4, A30, A29, A32, FUNCT_1:13; thus xp . n = (R_EAL (ap . n)) * ((M * Fp) . n) by A7, A32 .= (R_EAL ((max+ f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by A34, A33, FUNCT_2:def_1 ; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in_rng_xp_holds_ y_in_REAL let y be set ; ::_thesis: ( y in rng xp implies y in REAL ) assume y in rng xp ; ::_thesis: y in REAL then consider n being 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 = (max+ f) . ((canFS Omega) . n) as Element of REAL ; xp . n = (R_EAL ((max+ f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by A31, A35 .= w * z by EXTREAL1:1 ; hence y in REAL by A36; ::_thesis: verum end; then rng xp c= REAL by TARSKI:def_3; then reconsider xp1 = xp as FinSequence of REAL by FINSEQ_1:def_4; consider Fm being Finite_Sep_Sequence of Trivial-SigmaField Omega such that A37: dom (max- f) = union (rng Fm) and A38: dom Fm = dom (canFS (dom (max- f))) and A39: for k being Nat st k in dom Fm holds Fm . k = {((canFS (dom (max- f))) . 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 (max- f) . x = (max- f) . y by Lm6; defpred S3[ Nat, set ] means $2 = (R_EAL (am . $1)) * ((M * Fm) . $1); A40: for k being Nat st k in Seg (len F) holds ex x being Element of ExtREAL st S3[k,x] ; consider xm being FinSequence of ExtREAL such that A41: ( dom xm = Seg (len F) & ( for k being Nat st k in Seg (len F) holds S3[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: dom (max- f) = dom f by RFUNCT_3:def_11; A45: for n being Nat st n in dom xm holds xm . n = (R_EAL ((max- f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) proof let n be Nat; ::_thesis: ( n in dom xm implies xm . n = (R_EAL ((max- f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) ) assume A46: n in dom xm ; ::_thesis: xm . n = (R_EAL ((max- f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) 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 = (R_EAL (am . n)) * ((M * Fm) . n) by A41, A46 .= (R_EAL ((max- f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by A38, A43, A18, A46, A47, FUNCT_1:13 ; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in_rng_xm_holds_ y_in_REAL let y be set ; ::_thesis: ( y in rng xm implies y in REAL ) assume y in rng xm ; ::_thesis: y in REAL then consider n being 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 = (max- f) . ((canFS Omega) . n) as Element of REAL ; xm . n = (R_EAL ((max- f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by A45, A48 .= w * z by EXTREAL1:1 ; hence y in REAL by A49; ::_thesis: verum end; then rng xm c= REAL by TARSKI:def_3; 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 (max+ f) = Omega by A17, RFUNCT_3:def_10; then A51: max+ f is_integrable_on M by A14, Lm5, Th6; A52: dom (max- f) = dom f by RFUNCT_3:def_11; then A53: max- f is Function of Omega,REAL by A17, FUNCT_2:def_1; then M . (dom ((- 1) (#) (max- f))) < +infty by A14, FUNCT_2:def_1; then (- 1) (#) (max- f) is_integrable_on M by A53, Lm5, Th6; then consider E being Element of Trivial-SigmaField Omega such that A54: E = (dom (max+ f)) /\ (dom ((- 1) (#) (max- f))) and A55: Integral (M,((max+ f) + ((- 1) (#) (max- f)))) = (Integral (M,((max+ f) | E))) + (Integral (M,(((- 1) (#) (max- f)) | E))) by A51, MESFUNC6:101; A56: dom (max+ f) = dom f by RFUNCT_3:def_10; then A57: max+ f is Function of Omega,REAL by A17, FUNCT_2:def_1; dom ((- 1) (#) (max- f)) = dom (max- f) by VALUED_1:def_5 .= Omega by A52, FUNCT_2:def_1 ; then A58: E = Omega /\ Omega by A56, A54, FUNCT_2:def_1 .= Omega ; then ((- 1) (#) (max- f)) | E = (- 1) (#) (max- f) by A53, FUNCT_2:33; then A59: Integral (M,((max+ f) + ((- 1) (#) (max- f)))) = (Integral (M,(max+ f))) + (Integral (M,((- 1) (#) (max- f)))) by A57, A55, A58, FUNCT_2:33 .= (Integral (M,(max+ f))) + (- (Integral (M,(max- f)))) by A19, A11, MESFUNC6:102 ; A60: dom Fm = dom am by A38, Lm9; A61: for n being Nat st n in dom Fm holds for x being set st x in Fm . n holds (max- f) . x = am . n proof let n be Nat; ::_thesis: ( n in dom Fm implies for x being set st x in Fm . n holds (max- f) . x = am . n ) assume A62: n in dom Fm ; ::_thesis: for x being set st x in Fm . n holds (max- f) . x = am . n let x be set ; ::_thesis: ( x in Fm . n implies (max- f) . x = am . n ) assume x in Fm . n ; ::_thesis: (max- f) . x = am . n then x in {((canFS (dom (max- f))) . n)} by A39, A62; then x = (canFS (dom (max- f))) . n by TARSKI:def_1; hence (max- f) . x = am . n by A60, A62, FUNCT_1:12; ::_thesis: verum end; ( max+ f is_simple_func_in Trivial-SigmaField Omega & max+ f is nonnegative ) by Th6, MESFUNC6:61; then A63: Integral (M,(max+ f)) = Sum xp by A56, A3, A7, A29, A8, A9, Lm1; dom (canFS (dom f)) = Seg (len F) by A1, FINSEQ_1:def_3; then A64: len F = len (canFS (dom f)) by FINSEQ_1:def_3; A65: len x = len F by A13, FINSEQ_1:def_3; A66: dom (xp1 - xm1) = (dom xp1) /\ (dom xm1) by VALUED_1:12 .= dom x1 by A28, A42, A13, A29, A43, FINSEQ_1:def_3 ; A67: len xp1 = len F by A7, FINSEQ_1:def_3 .= len xm1 by A41, FINSEQ_1:def_3 ; A68: for k being Nat st k in dom x1 holds (xp1 - xm1) . k = x1 . k proof let k be Nat; ::_thesis: ( k in dom x1 implies (xp1 - xm1) . k = x1 . k ) A69: f = (max+ f) - (max- f) by MESFUNC6:42; assume A70: k in dom x1 ; ::_thesis: (xp1 - xm1) . k = x1 . k then reconsider z = M . {((canFS Omega) . k)} as Element of REAL by A1, A17, A20, A15; A71: xm1 . k = (R_EAL ((max- f) . ((canFS Omega) . k))) * (M . {((canFS Omega) . k)}) by A13, A41, A45, A70 .= ((max- f) . ((canFS Omega) . k)) * z by EXTREAL1:1 ; k in dom (canFS Omega) by A1, A20, A70, FUNCT_2:def_1; then (canFS Omega) . k in rng (canFS Omega) by FUNCT_1:3; then (canFS Omega) . k in Omega ; then A72: (canFS Omega) . k in dom f by FUNCT_2:def_1; k in (dom xp1) /\ (dom xm1) by A13, A7, A41, A70; then A73: k in dom (xp1 - xm1) by VALUED_1:12; xp1 . k = (R_EAL ((max+ f) . ((canFS Omega) . k))) * (M . {((canFS Omega) . k)}) by A13, A7, A31, A70 .= ((max+ f) . ((canFS Omega) . k)) * z by EXTREAL1:1 ; hence (xp1 - xm1) . k = (((max+ f) . ((canFS Omega) . k)) * z) - (((max- f) . ((canFS Omega) . k)) * z) by A73, A71, VALUED_1:13 .= (((max+ f) . ((canFS Omega) . k)) - ((max- f) . ((canFS Omega) . k))) * z .= (f . ((canFS Omega) . k)) * z by A72, A69, VALUED_1:13 .= (R_EAL (f . ((canFS Omega) . k))) * (M . {((canFS Omega) . k)}) by EXTREAL1:1 .= x1 . k by A21, A70 ; ::_thesis: verum end; Integral (M,f) = Integral (M,((max+ f) - (max- f))) by MESFUNC6:42 .= (Sum xp) - (Sum xm) by A52, A37, A27, A41, A43, A63, A59, A60, A61, Lm1 .= (Sum xp1) - (Sum xm1) by A50, SUPINF_2:3 .= Sum (xp1 - xm1) by A67, INTEGRA5:2 .= Sum x by A66, A68, FINSEQ_1:13, MESFUNC3:2 ; hence ( 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 A17, A21, A65, A64, UPROOTS:3; ::_thesis: verum end; theorem Th9: :: RANDOM_1:9 for Omega being non empty finite set for M being sigma_Measure of (Trivial-SigmaField Omega) for f being Function of Omega,REAL for x being FinSequence of ExtREAL for s being FinSequence of Omega st s is one-to-one & rng s = Omega holds ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st ( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being 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 ; ::_thesis: for M being sigma_Measure of (Trivial-SigmaField Omega) for f being Function of Omega,REAL for x being FinSequence of ExtREAL for s being FinSequence of Omega st s is one-to-one & rng s = Omega holds ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st ( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being 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 ) ) let M be sigma_Measure of (Trivial-SigmaField Omega); ::_thesis: for f being Function of Omega,REAL for x being FinSequence of ExtREAL for s being FinSequence of Omega st s is one-to-one & rng s = Omega holds ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st ( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being 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 ) ) let f be Function of Omega,REAL; ::_thesis: for x being FinSequence of ExtREAL for s being FinSequence of Omega st s is one-to-one & rng s = Omega holds ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st ( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being 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 ) ) let x be FinSequence of ExtREAL ; ::_thesis: for s being FinSequence of Omega st s is one-to-one & rng s = Omega holds ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st ( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being 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 ) ) let s be FinSequence of Omega; ::_thesis: ( s is one-to-one & rng s = Omega implies ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st ( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being 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 ) ) ) assume that A1: s is one-to-one and A2: rng s = Omega ; ::_thesis: ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st ( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being 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 ) ) defpred S1[ Nat, set ] means $2 = f . (s . $1); set Sigma = Trivial-SigmaField Omega; set L = len s; defpred S2[ Nat, set ] means $2 = {(s . $1)}; A3: for k being Nat st k in Seg (len s) holds ex x being Element of bool Omega st S2[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len s) implies ex x being Element of bool Omega st S2[k,x] ) assume A4: k in Seg (len s) ; ::_thesis: ex x being Element of bool Omega st S2[k,x] take {(s . k)} ; ::_thesis: ( {(s . k)} is Element of bool Omega & S2[k,{(s . k)}] ) k in dom s by A4, FINSEQ_1:def_3; then s . k in rng s by FUNCT_1:3; hence ( {(s . k)} is Element of bool Omega & S2[k,{(s . k)}] ) by ZFMISC_1:31; ::_thesis: verum end; consider F being FinSequence of bool Omega such that A5: ( dom F = Seg (len s) & ( for k being Nat st k in Seg (len s) holds S2[k,F . k] ) ) from FINSEQ_1:sch_5(A3); A6: now__::_thesis:_for_i,_j_being_Nat_st_i_in_dom_F_&_j_in_dom_F_&_i_<>_j_holds_ F_._i_misses_F_._j let i, j be Nat; ::_thesis: ( i in dom F & j in dom F & i <> j implies F . i misses F . j ) assume that A7: ( i in dom F & j in dom F ) and A8: i <> j ; ::_thesis: F . i misses F . 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; ::_thesis: verum end; A10: dom F = dom s by A5, FINSEQ_1:def_3; reconsider F = F as Finite_Sep_Sequence of Trivial-SigmaField Omega by A6, MESFUNC3:4; union (rng F) = rng s proof now__::_thesis:_for_x_being_set_st_x_in_union_(rng_F)_holds_ x_in_rng_s let x be set ; ::_thesis: ( x in union (rng F) implies x in rng s ) assume x in union (rng F) ; ::_thesis: x in rng s then consider y being set such that A11: x in y and A12: y in rng F by TARSKI:def_4; consider n being set 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; ::_thesis: verum end; hence union (rng F) c= rng s by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: rng s c= union (rng F) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng s or x in union (rng F) ) assume x in rng s ; ::_thesis: x in union (rng F) then consider n being set such that A16: n in dom s and A17: x = s . n by FUNCT_1:def_3; A18: n in Seg (len s) by A16, FINSEQ_1:def_3; reconsider n = 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; ::_thesis: verum end; then A20: dom f = union (rng F) by A2, FUNCT_2:def_1; take F ; ::_thesis: ex a being FinSequence of REAL st ( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being 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 ) ) 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; ::_thesis: 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 let x, y be Element of Omega; ::_thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y ) assume that A22: n in dom F and A23: x in F . n and A24: y in F . n ; ::_thesis: f . x = f . y 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 ; ::_thesis: verum end; A26: for k being Nat st k in Seg (len s) holds ex x being Element of REAL st S1[k,x] ; ex a being FinSequence of REAL st ( dom a = Seg (len s) & ( for k being Nat st k in Seg (len s) holds S1[k,a . k] ) ) from FINSEQ_1:sch_5(A26); hence ex a being FinSequence of REAL st ( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being 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 A5, A10, A20, A21; ::_thesis: verum end; theorem Th10: :: RANDOM_1:10 for Omega being non empty finite set for M being sigma_Measure of (Trivial-SigmaField Omega) for f being Function of Omega,REAL for x being FinSequence of ExtREAL for 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 ; ::_thesis: for M being sigma_Measure of (Trivial-SigmaField Omega) for f being Function of Omega,REAL for x being FinSequence of ExtREAL for 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 let M be sigma_Measure of (Trivial-SigmaField Omega); ::_thesis: for f being Function of Omega,REAL for x being FinSequence of ExtREAL for 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 let f be Function of Omega,REAL; ::_thesis: for x being FinSequence of ExtREAL for 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 let x be FinSequence of ExtREAL ; ::_thesis: for 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 let s be FinSequence of Omega; ::_thesis: ( 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)}) ) implies Integral (M,f) = Sum x ) 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 = (R_EAL (f . (s . n))) * (M . {(s . n)}) ; ::_thesis: Integral (M,f) = Sum x set Sigma = Trivial-SigmaField Omega; consider F being Finite_Sep_Sequence of Trivial-SigmaField Omega, 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 being 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 (max+ f) = Omega by RFUNCT_3:def_10; then A12: max+ f is_integrable_on M by A1, Lm5, Th6; A13: for n being Nat st n in dom s holds M . {(s . n)} in REAL proof let n be Nat; ::_thesis: ( n in dom s implies M . {(s . n)} in REAL ) assume n in dom s ; ::_thesis: M . {(s . n)} in REAL 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; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in_rng_x_holds_ y_in_REAL let y be set ; ::_thesis: ( y in rng x implies y in REAL ) assume y in rng x ; ::_thesis: y in REAL then consider n being 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 ; x . n = (R_EAL (f . (s . n))) * (M . {(s . n)}) by A6, A14 .= w * z by EXTREAL1:1 ; hence y in REAL by A15; ::_thesis: verum end; then rng x c= REAL by TARSKI:def_3; then reconsider x1 = x as FinSequence of REAL by FINSEQ_1:def_4; A16: ( max- f is_simple_func_in Trivial-SigmaField Omega & max- f is nonnegative ) by Th6, MESFUNC6:61; defpred S1[ Nat, set ] means for x being set st x in F . $1 holds $2 = (max+ f) . x; set L = len F; A17: dom F = Seg (len F) by FINSEQ_1:def_3; A18: for k being Nat st k in Seg (len F) holds ex y being Element of REAL st S1[k,y] proof let k be Nat; ::_thesis: ( k in Seg (len F) implies ex y being Element of REAL st S1[k,y] ) assume A19: k in Seg (len F) ; ::_thesis: ex y being Element of REAL st S1[k,y] take (max+ f) . (s . k) ; ::_thesis: S1[k,(max+ f) . (s . k)] F . k = {(s . k)} by A9, A17, A19; hence S1[k,(max+ f) . (s . k)] by TARSKI:def_1; ::_thesis: verum end; consider ap being FinSequence of REAL such that A20: ( dom ap = Seg (len F) & ( for k being Nat st k in Seg (len F) holds S1[k,ap . k] ) ) from FINSEQ_1:sch_5(A18); defpred S2[ Nat, set ] means for x being set st x in F . $1 holds $2 = (max- f) . x; A21: for k being Nat st k in Seg (len F) holds ex y being Element of REAL st S2[k,y] proof let k be Nat; ::_thesis: ( k in Seg (len F) implies ex y being Element of REAL st S2[k,y] ) assume A22: k in Seg (len F) ; ::_thesis: ex y being Element of REAL st S2[k,y] take (max- f) . (s . k) ; ::_thesis: S2[k,(max- f) . (s . k)] F . k = {(s . k)} by A9, A17, A22; hence S2[k,(max- f) . (s . k)] by TARSKI:def_1; ::_thesis: verum end; consider am being FinSequence of REAL such that A23: ( dom am = Seg (len F) & ( for k being Nat st k in Seg (len F) holds S2[k,am . k] ) ) from FINSEQ_1:sch_5(A21); A24: dom (max- f) = dom f by RFUNCT_3:def_11; then A25: max- f is Function of Omega,REAL by A11, FUNCT_2:def_1; then M . (dom ((- 1) (#) (max- f))) < +infty by A1, FUNCT_2:def_1; then (- 1) (#) (max- f) is_integrable_on M by A25, Lm5, Th6; then consider E being Element of Trivial-SigmaField Omega such that A26: E = (dom (max+ f)) /\ (dom ((- 1) (#) (max- f))) and A27: Integral (M,((max+ f) + ((- 1) (#) (max- f)))) = (Integral (M,((max+ f) | E))) + (Integral (M,(((- 1) (#) (max- f)) | E))) by A12, MESFUNC6:101; A28: (R_EAL (- 1)) * (Integral (M,(max- f))) = (- (R_EAL 1)) * (Integral (M,(max- f))) by SUPINF_2:2 .= - ((R_EAL 1) * (Integral (M,(max- f)))) by XXREAL_3:92 .= - (Integral (M,(max- f))) by XXREAL_3:81 ; defpred S3[ Nat, set ] means $2 = (R_EAL (ap . $1)) * ((M * F) . $1); A29: for k being Nat st k in Seg (len F) holds ex x being Element of ExtREAL st S3[k,x] ; consider xp being FinSequence of ExtREAL such that A30: ( dom xp = Seg (len F) & ( for k being Nat st k in Seg (len F) holds S3[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 = (R_EAL ((max+ f) . (s . n))) * (M . {(s . n)}) proof let n be Nat; ::_thesis: ( n in dom xp implies xp . n = (R_EAL ((max+ f) . (s . n))) * (M . {(s . n)}) ) assume A33: n in dom xp ; ::_thesis: xp . n = (R_EAL ((max+ f) . (s . n))) * (M . {(s . n)}) 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 = (R_EAL (ap . n)) * ((M * F) . n) by A30, A33 .= (R_EAL ((max+ f) . (s . n))) * (M . {(s . n)}) by A20, A30, A33, A35, A34 ; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in_rng_xp_holds_ y_in_REAL let y be set ; ::_thesis: ( y in rng xp implies y in REAL ) assume y in rng xp ; ::_thesis: y in REAL then consider n being 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 = (max+ f) . (s . n) as Element of REAL ; xp . n = (R_EAL ((max+ f) . (s . n))) * (M . {(s . n)}) by A32, A36 .= w * z by EXTREAL1:1 ; hence y in REAL by A37; ::_thesis: verum end; then rng xp c= REAL by TARSKI:def_3; then reconsider xp1 = xp as FinSequence of REAL by FINSEQ_1:def_4; defpred S4[ Nat, set ] means $2 = (R_EAL (am . $1)) * ((M * F) . $1); A38: for k being Nat st k in Seg (len F) holds ex x being Element of ExtREAL st S4[k,x] ; consider xm being FinSequence of ExtREAL such that A39: ( dom xm = Seg (len F) & ( for k being Nat st k in Seg (len F) holds S4[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 = (R_EAL ((max- f) . (s . n))) * (M . {(s . n)}) proof let n be Nat; ::_thesis: ( n in dom xm implies xm . n = (R_EAL ((max- f) . (s . n))) * (M . {(s . n)}) ) assume A42: n in dom xm ; ::_thesis: xm . n = (R_EAL ((max- f) . (s . n))) * (M . {(s . n)}) 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 = (R_EAL (am . n)) * ((M * F) . n) by A39, A42 .= (R_EAL ((max- f) . (s . n))) * (M . {(s . n)}) by A23, A39, A42, A44, A43 ; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in_rng_xm_holds_ y_in_REAL let y be set ; ::_thesis: ( y in rng xm implies y in REAL ) assume y in rng xm ; ::_thesis: y in REAL then consider n being 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 = (max- f) . (s . n) as Element of REAL ; xm . n = (R_EAL ((max- f) . (s . n))) * (M . {(s . n)}) by A41, A45 .= w * z by EXTREAL1:1 ; hence y in REAL by A46; ::_thesis: verum end; then rng xm c= REAL by TARSKI:def_3; 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 being Nat st k in dom x1 holds (xp1 - xm1) . k = x1 . k proof let k be Nat; ::_thesis: ( k in dom x1 implies (xp1 - xm1) . k = x1 . k ) A49: f = (max+ f) - (max- f) by MESFUNC6:42; assume A50: k in dom x1 ; ::_thesis: (xp1 - xm1) . k = x1 . k then reconsider z = M . {(s . k)} as Element of REAL by A8, A10, A13; A51: xm1 . k = (R_EAL ((max- f) . (s . k))) * (M . {(s . k)}) by A10, A40, A41, A50 .= ((max- f) . (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 = (R_EAL ((max+ f) . (s . k))) * (M . {(s . k)}) by A10, A31, A32, A50 .= ((max+ f) . (s . k)) * z by EXTREAL1:1 ; hence (xp1 - xm1) . k = (((max+ f) . (s . k)) * z) - (((max- f) . (s . k)) * z) by A53, A51, VALUED_1:13 .= (((max+ f) . (s . k)) - ((max- f) . (s . k))) * z .= (f . (s . k)) * z by A52, A49, VALUED_1:13 .= (R_EAL (f . (s . k))) * (M . {(s . k)}) by EXTREAL1:1 .= x1 . k by A6, A50 ; ::_thesis: verum end; dom (max- f) = Omega by A11, RFUNCT_3:def_11; then A54: max- f is_integrable_on M by A1, Lm5, Th6; A55: dom (max+ f) = dom f by RFUNCT_3:def_10; then A56: max+ f is Function of Omega,REAL by A11, FUNCT_2:def_1; A57: dom (xp1 - xm1) = (dom xp1) /\ (dom xm1) by VALUED_1:12 .= dom x1 by A10, A31, A40 ; A58: len xp1 = len F by A30, FINSEQ_1:def_3 .= len xm1 by A39, FINSEQ_1:def_3 ; dom ((- 1) (#) (max- f)) = dom (max- f) by VALUED_1:def_5 .= Omega by A11, RFUNCT_3:def_11 ; then A59: E = Omega /\ Omega by A11, A26, RFUNCT_3:def_10 .= Omega ; then ((- 1) (#) (max- f)) | E = (- 1) (#) (max- f) by A25, FUNCT_2:33; then A60: Integral (M,((max+ f) + ((- 1) (#) (max- f)))) = (Integral (M,(max+ f))) + (Integral (M,((- 1) (#) (max- f)))) by A56, A27, A59, FUNCT_2:33 .= (Integral (M,(max+ f))) + (- (Integral (M,(max- f)))) by A54, A28, MESFUNC6:102 ; ( max+ f is_simple_func_in Trivial-SigmaField Omega & max+ f is nonnegative ) by Th6, MESFUNC6:61; then A61: Integral (M,(max+ f)) = Sum xp by A7, A55, A17, A20, A30, Lm1; thus Integral (M,f) = Integral (M,((max+ f) - (max- f))) by MESFUNC6:42 .= (Sum xp) - (Sum xm) by A7, A24, A17, A23, A16, A39, A61, A60, Lm1 .= (Sum xp1) - (Sum xm1) by A47, SUPINF_2:3 .= Sum (xp1 - xm1) by A58, INTEGRA5:2 .= Sum x by A57, A48, FINSEQ_1:13, MESFUNC3:2 ; ::_thesis: verum end; theorem :: RANDOM_1:11 for Omega being non empty finite set for M being sigma_Measure of (Trivial-SigmaField Omega) for f being Function of Omega,REAL st M . Omega < +infty holds ex x being FinSequence of ExtREAL ex 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 ; ::_thesis: for M being sigma_Measure of (Trivial-SigmaField Omega) for f being Function of Omega,REAL st M . Omega < +infty holds ex x being FinSequence of ExtREAL ex 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 ) let M be sigma_Measure of (Trivial-SigmaField Omega); ::_thesis: for f being Function of Omega,REAL st M . Omega < +infty holds ex x being FinSequence of ExtREAL ex 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 ) let f be Function of Omega,REAL; ::_thesis: ( M . Omega < +infty implies ex x being FinSequence of ExtREAL ex 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 ) ) set s = canFS Omega; assume M . Omega < +infty ; ::_thesis: ex x being FinSequence of ExtREAL ex 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 ) 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 = (R_EAL (f . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) ) & Integral (M,f) = Sum x ) by Lm10; ( rng (canFS Omega) = Omega & len (canFS Omega) = card Omega ) by FUNCT_2:def_3, UPROOTS:3; hence ex x being FinSequence of ExtREAL ex 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 ) by A1; ::_thesis: verum end; Lm11: for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for f being Function of Omega,REAL 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 ; ::_thesis: for P being Probability of Trivial-SigmaField Omega for f being Function of Omega,REAL 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 ) let P be Probability of Trivial-SigmaField Omega; ::_thesis: for f being Function of Omega,REAL 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 ) let f be Function of Omega,REAL; ::_thesis: 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 ) set Sigma = Trivial-SigmaField Omega; set M = P2M P; A1: P . Omega in REAL ; 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 = (R_EAL (f . ((canFS Omega) . n))) * ((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 being Nat st n in dom (canFS Omega) holds (P2M P) . {((canFS Omega) . n)} in REAL proof let n be Nat; ::_thesis: ( n in dom (canFS Omega) implies (P2M P) . {((canFS Omega) . n)} in REAL ) assume n in dom (canFS Omega) ; ::_thesis: (P2M P) . {((canFS Omega) . n)} in REAL 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 Trivial-SigmaField Omega by MEASURE1:7; hence (P2M P) . {((canFS Omega) . n)} in REAL by A5, A7, Lm7; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in_rng_x_holds_ y_in_REAL let y be set ; ::_thesis: ( y in rng x implies y in REAL ) assume y in rng x ; ::_thesis: y in REAL then consider n being 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, UPROOTS:3; 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 = (P2M P) . {((canFS Omega) . n)} as Element of REAL by A6; reconsider w = f . ((canFS Omega) . n) as Element of REAL ; x . n = (R_EAL (f . ((canFS Omega) . n))) * ((P2M P) . {((canFS Omega) . n)}) by A3, A8 .= w * z by EXTREAL1:1 ; hence y in REAL by A9; ::_thesis: verum end; then rng x c= REAL by TARSKI:def_3; then reconsider F = x as FinSequence of REAL by FINSEQ_1:def_4; take F ; ::_thesis: ( 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 ) now__::_thesis:_for_n_being_Nat_st_n_in_dom_F_holds_ F_._n_=_(f_._((canFS_Omega)_._n))_*_(P_._{((canFS_Omega)_._n)}) let n be Nat; ::_thesis: ( n in dom F implies F . n = (f . ((canFS Omega) . n)) * (P . {((canFS Omega) . n)}) ) assume n in dom F ; ::_thesis: F . n = (f . ((canFS Omega) . n)) * (P . {((canFS Omega) . n)}) hence F . n = (R_EAL (f . ((canFS Omega) . n))) * ((P2M P) . {((canFS Omega) . n)}) by A3 .= (f . ((canFS Omega) . n)) * (P . {((canFS Omega) . n)}) by EXTREAL1:1 ; ::_thesis: verum end; hence ( 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 A2, A4, MESFUNC3:2; ::_thesis: verum end; theorem Th12: :: RANDOM_1:12 for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for f being Function of Omega,REAL for x being FinSequence of REAL for 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)) * (P . {(s . n)}) ) holds Integral ((P2M P),f) = Sum x proof let Omega be non empty finite set ; ::_thesis: for P being Probability of Trivial-SigmaField Omega for f being Function of Omega,REAL for x being FinSequence of REAL for 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)) * (P . {(s . n)}) ) holds Integral ((P2M P),f) = Sum x let P be Probability of Trivial-SigmaField Omega; ::_thesis: for f being Function of Omega,REAL for x being FinSequence of REAL for 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)) * (P . {(s . n)}) ) holds Integral ((P2M P),f) = Sum x let f be Function of Omega,REAL; ::_thesis: for x being FinSequence of REAL for 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)) * (P . {(s . n)}) ) holds Integral ((P2M P),f) = Sum x let x be FinSequence of REAL ; ::_thesis: for 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)) * (P . {(s . n)}) ) holds Integral ((P2M P),f) = Sum x let s be FinSequence of Omega; ::_thesis: ( 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)}) ) implies Integral ((P2M P),f) = Sum x ) 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)}) ; ::_thesis: Integral ((P2M P),f) = Sum x set M = P2M P; rng x c= ExtREAL by NUMBERS:31, XBOOLE_1:1; then reconsider x1 = x as FinSequence of ExtREAL by FINSEQ_1:def_4; A3: now__::_thesis:_for_n_being_Nat_st_n_in_dom_x1_holds_ x1_._n_=_(R_EAL_(f_._(s_._n)))_*_((P2M_P)_._{(s_._n)}) let n be Nat; ::_thesis: ( n in dom x1 implies x1 . n = (R_EAL (f . (s . n))) * ((P2M P) . {(s . n)}) ) assume n in dom x1 ; ::_thesis: x1 . n = (R_EAL (f . (s . n))) * ((P2M P) . {(s . n)}) hence x1 . n = (f . (s . n)) * (P . {(s . n)}) by A2 .= (R_EAL (f . (s . n))) * ((P2M P) . {(s . n)}) by EXTREAL1:1 ; ::_thesis: verum end; P . Omega in REAL ; then Integral ((P2M P),f) = Sum x1 by A1, A3, Th10, XXREAL_0:9 .= Sum x by MESFUNC3:2 ; hence Integral ((P2M P),f) = Sum x ; ::_thesis: verum end; theorem Th13: :: RANDOM_1:13 for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for f being Function of Omega,REAL ex F being FinSequence of REAL ex 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 ; ::_thesis: for P being Probability of Trivial-SigmaField Omega for f being Function of Omega,REAL ex F being FinSequence of REAL ex 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 ) let P be Probability of Trivial-SigmaField Omega; ::_thesis: for f being Function of Omega,REAL ex F being FinSequence of REAL ex 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 ) let f be Function of Omega,REAL; ::_thesis: ex F being FinSequence of REAL ex 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 ) set s = canFS Omega; A1: len (canFS Omega) = card Omega by UPROOTS:3; ( 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 (canFS Omega) = Omega ) by Lm11, FUNCT_2:def_3; hence ex F being FinSequence of REAL ex 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 ) by A1; ::_thesis: verum end; theorem Th14: :: RANDOM_1:14 for E being non empty finite set for ASeq being SetSequence of E st ASeq is non-ascending holds ex N being Element of NAT st for m being Element of NAT st N <= m holds ASeq . N = ASeq . m proof let E be non empty finite set ; ::_thesis: for ASeq being SetSequence of E st ASeq is non-ascending holds ex N being Element of NAT st for m being Element of NAT st N <= m holds ASeq . N = ASeq . m let ASeq be SetSequence of E; ::_thesis: ( ASeq is non-ascending implies ex N being Element of NAT st for m being Element of NAT st N <= m holds ASeq . N = ASeq . m ) defpred S1[ Element of NAT , set ] means $2 = card (ASeq . $1); A1: for x being Element of NAT ex y being Element of REAL st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of REAL st S1[x,y] card (ASeq . x) in NAT ; hence ex y being Element of REAL st S1[x,y] ; ::_thesis: verum end; consider seq being Function of NAT,REAL such that A2: for n being Element of NAT holds S1[n,seq . n] from FUNCT_2:sch_3(A1); now__::_thesis:_for_m_being_Element_of_NAT_holds_-_1_<_seq_._m let m be Element of NAT ; ::_thesis: - 1 < seq . m seq . m = card (ASeq . m) by A2; hence - 1 < seq . m ; ::_thesis: verum end; then A3: seq is V139() by SEQ_2:def_4; assume A4: ASeq is non-ascending ; ::_thesis: ex N being Element of NAT st for m being Element of NAT st N <= m holds ASeq . N = ASeq . m A5: now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ seq_._m_<=_seq_._n let n, m be Element of NAT ; ::_thesis: ( n <= m implies seq . m <= seq . n ) assume n <= m ; ::_thesis: seq . m <= seq . n then A6: ASeq . m c= ASeq . n by A4, PROB_1:def_4; ( seq . m = card (ASeq . m) & seq . n = card (ASeq . n) ) by A2; hence seq . m <= seq . n by A6, NAT_1:43; ::_thesis: verum end; then seq is V68() by SEQM_3:8; then consider g being real number such that A7: for p being real number st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - g) < p by A3, SEQ_2:def_6; consider N being Element of NAT such that A8: for m being Element of NAT st N <= m holds abs ((seq . m) - g) < 1 / 2 by A7; take N ; ::_thesis: for m being Element of NAT st N <= m holds ASeq . N = ASeq . m now__::_thesis:_for_m_being_Element_of_NAT_st_N_<=_m_holds_ ASeq_._m_=_ASeq_._N abs ((seq . N) - g) < 1 / 2 by A8; then A9: abs (g - (seq . N)) < 1 / 2 by COMPLEX1:60; let m be Element of NAT ; ::_thesis: ( N <= m implies ASeq . m = ASeq . N ) A10: ( seq . N = card (ASeq . N) & seq . m = card (ASeq . m) ) by A2; assume A11: N <= m ; ::_thesis: ASeq . m = ASeq . N then A12: ( seq . m <= seq . N & ASeq . m c= ASeq . N ) by A4, A5, PROB_1:def_4; abs ((seq . m) - g) < 1 / 2 by A8, A11; then A13: (abs ((seq . m) - g)) + (abs (g - (seq . N))) < (1 / 2) + (1 / 2) by A9, XREAL_1:8; abs ((seq . m) - (seq . N)) <= (abs ((seq . m) - g)) + (abs (g - (seq . N))) by COMPLEX1:63; then abs ((seq . m) - (seq . N)) < 1 by A13, XXREAL_0:2; then abs ((seq . N) - (seq . m)) < 1 by COMPLEX1:60; then (seq . N) - (seq . m) < 1 by ABSVALUE:def_1; then ((seq . N) - (seq . m)) + (seq . m) < 1 + (seq . m) by XREAL_1:8; then seq . N <= seq . m by A10, NAT_1:8; hence ASeq . m = ASeq . N by A10, A12, CARD_FIN:1, XXREAL_0:1; ::_thesis: verum end; hence for m being Element of NAT st N <= m holds ASeq . N = ASeq . m ; ::_thesis: verum end; theorem Th15: :: RANDOM_1:15 for E being non empty finite set for ASeq being SetSequence of E st ASeq is non-ascending holds ex N being Element of NAT st for m being Element of NAT st N <= m holds Intersection ASeq = ASeq . m proof let E be non empty finite set ; ::_thesis: for ASeq being SetSequence of E st ASeq is non-ascending holds ex N being Element of NAT st for m being Element of NAT st N <= m holds Intersection ASeq = ASeq . m let ASeq be SetSequence of E; ::_thesis: ( ASeq is non-ascending implies ex N being Element of NAT st for m being Element of NAT st N <= m holds Intersection ASeq = ASeq . m ) assume A1: ASeq is non-ascending ; ::_thesis: ex N being Element of NAT st for m being Element of NAT st N <= m holds Intersection ASeq = ASeq . m then consider N0 being Element of NAT such that A2: for m being Element of NAT st N0 <= m holds ASeq . N0 = ASeq . m by Th14; take N0 ; ::_thesis: for m being Element of NAT st N0 <= m holds Intersection ASeq = ASeq . m let N be Element of NAT ; ::_thesis: ( N0 <= N implies Intersection ASeq = ASeq . N ) assume N0 <= N ; ::_thesis: Intersection ASeq = ASeq . N then A3: ASeq . N = ASeq . N0 by A2; thus Intersection ASeq = ASeq . N ::_thesis: verum proof for x being set st x in Intersection ASeq holds x in ASeq . N by PROB_1:13; hence Intersection ASeq c= ASeq . N by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: ASeq . N c= Intersection ASeq let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ASeq . N or x in Intersection ASeq ) assume A4: x in ASeq . N ; ::_thesis: x in Intersection ASeq now__::_thesis:_for_n_being_Element_of_NAT_holds_x_in_ASeq_._n let n be Element of NAT ; ::_thesis: x in ASeq . b1 percases ( n <= N0 or N0 < n ) ; suppose n <= N0 ; ::_thesis: x in ASeq . b1 then ASeq . N0 c= ASeq . n by A1, PROB_1:def_4; hence x in ASeq . n by A3, A4; ::_thesis: verum end; suppose N0 < n ; ::_thesis: x in ASeq . b1 hence x in ASeq . n by A2, A3, A4; ::_thesis: verum end; end; end; hence x in Intersection ASeq by PROB_1:13; ::_thesis: verum end; end; theorem Th16: :: RANDOM_1:16 for E being non empty finite set for ASeq being SetSequence of E st ASeq is non-descending holds ex N being Element of NAT st for m being Element of NAT st N <= m holds ASeq . N = ASeq . m proof let E be non empty finite set ; ::_thesis: for ASeq being SetSequence of E st ASeq is non-descending holds ex N being Element of NAT st for m being Element of NAT st N <= m holds ASeq . N = ASeq . m let ASeq be SetSequence of E; ::_thesis: ( ASeq is non-descending implies ex N being Element of NAT st for m being Element of NAT st N <= m holds ASeq . N = ASeq . m ) defpred S1[ Element of NAT , set ] means $2 = card (ASeq . $1); A1: for x being Element of NAT ex y being Element of REAL st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of REAL st S1[x,y] card (ASeq . x) in NAT ; hence ex y being Element of REAL st S1[x,y] ; ::_thesis: verum end; consider seq being Function of NAT,REAL such that A2: for n being Element of NAT holds S1[n,seq . n] from FUNCT_2:sch_3(A1); now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_<_(card_E)_+_1 let n be Element of NAT ; ::_thesis: seq . n < (card E) + 1 card (ASeq . n) <= card E by NAT_1:43; then card (ASeq . n) < (card E) + 1 by NAT_1:13; hence seq . n < (card E) + 1 by A2; ::_thesis: verum end; then A3: seq is V138() by SEQ_2:def_3; assume A4: ASeq is non-descending ; ::_thesis: ex N being Element of NAT st for m being Element of NAT st N <= m holds ASeq . N = ASeq . m A5: now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ seq_._n_<=_seq_._m let n, m be Element of NAT ; ::_thesis: ( n <= m implies seq . n <= seq . m ) assume n <= m ; ::_thesis: seq . n <= seq . m then A6: ASeq . n c= ASeq . m by A4, PROB_1:def_5; ( seq . m = card (ASeq . m) & seq . n = card (ASeq . n) ) by A2; hence seq . n <= seq . m by A6, NAT_1:43; ::_thesis: verum end; then seq is V67() by SEQM_3:6; then consider g being real number such that A7: for p being real number st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - g) < p by A3, SEQ_2:def_6; consider N being Element of NAT such that A8: for m being Element of NAT st N <= m holds abs ((seq . m) - g) < 1 / 2 by A7; take N ; ::_thesis: for m being Element of NAT st N <= m holds ASeq . N = ASeq . m now__::_thesis:_for_m_being_Element_of_NAT_st_N_<=_m_holds_ ASeq_._m_=_ASeq_._N abs ((seq . N) - g) < 1 / 2 by A8; then A9: abs (g - (seq . N)) < 1 / 2 by COMPLEX1:60; let m be Element of NAT ; ::_thesis: ( N <= m implies ASeq . m = ASeq . N ) A10: ( seq . N = card (ASeq . N) & seq . m = card (ASeq . m) ) by A2; assume A11: N <= m ; ::_thesis: ASeq . m = ASeq . N then A12: ( seq . N <= seq . m & ASeq . N c= ASeq . m ) by A4, A5, PROB_1:def_5; abs ((seq . m) - g) < 1 / 2 by A8, A11; then A13: (abs ((seq . m) - g)) + (abs (g - (seq . N))) < (1 / 2) + (1 / 2) by A9, XREAL_1:8; abs ((seq . m) - (seq . N)) <= (abs ((seq . m) - g)) + (abs (g - (seq . N))) by COMPLEX1:63; then abs ((seq . m) - (seq . N)) < 1 by A13, XXREAL_0:2; then (seq . m) - (seq . N) < 1 by ABSVALUE:def_1; then ((seq . m) - (seq . N)) + (seq . N) < 1 + (seq . N) by XREAL_1:8; then seq . m <= seq . N by A10, NAT_1:8; hence ASeq . m = ASeq . N by A10, A12, CARD_FIN:1, XXREAL_0:1; ::_thesis: verum end; hence for m being Element of NAT st N <= m holds ASeq . N = ASeq . m ; ::_thesis: verum end; theorem :: RANDOM_1:17 for E being non empty finite set for ASeq being SetSequence of E st ASeq is non-descending holds ex N being Nat st for m being Nat st N <= m holds Union ASeq = ASeq . m proof let E be non empty finite set ; ::_thesis: for ASeq being SetSequence of E st ASeq is non-descending holds ex N being Nat st for m being Nat st N <= m holds Union ASeq = ASeq . m let ASeq be SetSequence of E; ::_thesis: ( ASeq is non-descending implies ex N being Nat st for m being Nat st N <= m holds Union ASeq = ASeq . m ) assume A1: ASeq is non-descending ; ::_thesis: ex N being Nat st for m being Nat st N <= m holds Union ASeq = ASeq . m then consider N0 being Element of NAT such that A2: for m being Element of NAT st N0 <= m holds ASeq . N0 = ASeq . m by Th16; reconsider N = N0 as Nat ; take N ; ::_thesis: for m being Nat st N <= m holds Union ASeq = ASeq . m let m be Nat; ::_thesis: ( N <= m implies Union ASeq = ASeq . m ) reconsider M = m as Element of NAT by ORDINAL1:def_12; assume A3: N <= m ; ::_thesis: Union ASeq = ASeq . m now__::_thesis:_for_x_being_set_st_x_in_Union_ASeq_holds_ x_in_ASeq_._m let x be set ; ::_thesis: ( x in Union ASeq implies b1 in ASeq . m ) assume x in Union ASeq ; ::_thesis: b1 in ASeq . m then consider n being Element of NAT such that A4: x in ASeq . n by PROB_1:12; percases ( n < N or N <= n ) ; supposeA5: n < N ; ::_thesis: b1 in ASeq . m A6: ASeq . N c= ASeq . M by A2, A3; ASeq . n c= ASeq . N by A1, A5, PROB_1:def_5; then ASeq . n c= ASeq . m by A6, XBOOLE_1:1; hence x in ASeq . m by A4; ::_thesis: verum end; suppose N <= n ; ::_thesis: b1 in ASeq . m then ASeq . N = ASeq . n by A2; then ASeq . n c= ASeq . M by A2, A3; hence x in ASeq . m by A4; ::_thesis: verum end; end; end; then A7: Union ASeq c= ASeq . m by TARSKI:def_3; ASeq . m c= Union ASeq by ABCMIZ_1:1; hence ASeq . m = Union ASeq by A7, XBOOLE_0:def_10; ::_thesis: verum end; definition let E be non empty finite set ; func Trivial-Probability E -> Probability of Trivial-SigmaField E means :Def1: :: RANDOM_1:def 1 for A being Event of E holds it . A = prob A; existence ex b1 being Probability of Trivial-SigmaField E st for A being Event of E holds b1 . A = prob A proof deffunc H1( Element of bool E) -> Element of REAL = prob $1; consider EP being Function of (Trivial-SigmaField E),REAL such that A1: for x being Element of Trivial-SigmaField E holds EP . x = H1(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 be Event of Trivial-SigmaField E; ::_thesis: ( A misses B implies EP . (A \/ B) = (EP . A) + (EP . B) ) assume A3: A misses B ; ::_thesis: EP . (A \/ B) = (EP . A) + (EP . B) thus EP . (A \/ B) = prob (A \/ B) by A1 .= ((prob A) + (prob B)) - (prob (A /\ B)) by RPR_1:20 .= ((prob A) + (prob B)) - 0 by A3, RPR_1:16 .= (EP . A) + (prob B) by A1 .= (EP . A) + (EP . B) by A1 ; ::_thesis: verum end; A4: for A being Event of Trivial-SigmaField E holds 0 <= EP . A proof let A be Event of Trivial-SigmaField E; ::_thesis: 0 <= EP . A EP . A = prob A by A1; hence 0 <= EP . A ; ::_thesis: verum end; take EP ; ::_thesis: ( EP is Probability of Trivial-SigmaField E & ( for A being Event of E holds EP . A = prob A ) ) A5: 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 be SetSequence of Trivial-SigmaField E; ::_thesis: ( ASeq is non-ascending implies ( EP * ASeq is convergent & lim (EP * ASeq) = EP . (Intersection ASeq) ) ) assume ASeq is non-ascending ; ::_thesis: ( EP * ASeq is convergent & lim (EP * ASeq) = EP . (Intersection ASeq) ) then consider N being Element of NAT such that A6: for m being Element of NAT st N <= m holds Intersection ASeq = ASeq . m by Th15; now__::_thesis:_for_m_being_Element_of_NAT_st_N_<=_m_holds_ (EP_*_ASeq)_._m_=_EP_._(Intersection_ASeq) let m be Element of NAT ; ::_thesis: ( N <= m implies (EP * ASeq) . m = EP . (Intersection ASeq) ) assume A7: N <= m ; ::_thesis: (EP * ASeq) . m = EP . (Intersection ASeq) m in NAT ; 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 A6, A7 ; ::_thesis: verum end; hence ( EP * ASeq is convergent & lim (EP * ASeq) = EP . (Intersection ASeq) ) by PROB_1:1; ::_thesis: verum end; EP . E = prob ([#] E) by A1 .= 1 by RPR_1:15 ; hence ( EP is Probability of Trivial-SigmaField E & ( for A being Event of E holds EP . A = prob A ) ) by A1, A4, A2, A5, PROB_1:def_8; ::_thesis: verum end; uniqueness for b1, b2 being Probability of Trivial-SigmaField E st ( for A being Event of E holds b1 . A = prob A ) & ( for A being Event of E holds b2 . A = prob A ) holds b1 = b2 proof let F, G be Probability of Trivial-SigmaField E; ::_thesis: ( ( for A being Event of E holds F . A = prob A ) & ( for A being Event of E holds G . A = prob A ) implies F = G ) assume A8: for A being Event of E holds F . A = prob A ; ::_thesis: ( ex A being Event of E st not G . A = prob A or F = G ) assume A9: for A being Event of E holds G . A = prob A ; ::_thesis: F = G now__::_thesis:_for_x_being_set_st_x_in_Trivial-SigmaField_E_holds_ F_._x_=_G_._x let x be set ; ::_thesis: ( x in Trivial-SigmaField E implies F . x = G . x ) assume x in Trivial-SigmaField E ; ::_thesis: F . x = G . x then reconsider A = x as Event of E ; thus F . x = prob A by A8 .= G . x by A9 ; ::_thesis: verum end; hence F = G by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def1 defines Trivial-Probability RANDOM_1:def_1_:_ for E being non empty finite set for b2 being Probability of Trivial-SigmaField E holds ( b2 = Trivial-Probability E iff for A being Event of E holds b2 . A = prob A ); definition let Omega be non empty set ; let Sigma be SigmaField of Omega; mode Real-Valued-Random-Variable of Sigma -> Function of Omega,REAL means :Def2: :: RANDOM_1:def 2 ex X being Element of Sigma st ( X = Omega & it is_measurable_on X ); correctness existence ex b1 being Function of Omega,REAL ex X being Element of Sigma st ( X = Omega & b1 is_measurable_on X ); proof reconsider X = Omega as Element of Sigma by MEASURE1:7; chi (X,Omega) is V63() by MESFUNC2:28; then ( dom (chi (X,Omega)) = Omega & rng (chi (X,Omega)) c= REAL ) by FUNCT_3:def_3, VALUED_0:def_3; then reconsider f = chi (X,Omega) as Function of Omega,REAL by FUNCT_2:2; ( R_EAL f = chi (X,Omega) & chi (X,Omega) is_measurable_on X ) by MESFUNC2:29; then f is_measurable_on X by MESFUNC6:def_1; hence ex b1 being Function of Omega,REAL ex X being Element of Sigma st ( X = Omega & b1 is_measurable_on X ) ; ::_thesis: verum end; end; :: deftheorem Def2 defines Real-Valued-Random-Variable RANDOM_1:def_2_:_ for Omega being non empty set for Sigma being SigmaField of Omega for b3 being Function of Omega,REAL holds ( b3 is Real-Valued-Random-Variable of Sigma iff ex X being Element of Sigma st ( X = Omega & b3 is_measurable_on X ) ); theorem Th18: :: RANDOM_1:18 for Omega being non empty set for Sigma being SigmaField of Omega for f, g being Real-Valued-Random-Variable of Sigma holds f + g is Real-Valued-Random-Variable of Sigma proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for f, g being Real-Valued-Random-Variable of Sigma holds f + g is Real-Valued-Random-Variable of Sigma let Sigma be SigmaField of Omega; ::_thesis: for f, g being Real-Valued-Random-Variable of Sigma holds f + g is Real-Valued-Random-Variable of Sigma let f, g be Real-Valued-Random-Variable of Sigma; ::_thesis: f + g is Real-Valued-Random-Variable of Sigma ( ex X being Element of Sigma st ( X = Omega & f is_measurable_on X ) & ex Y being Element of Sigma st ( Y = Omega & g is_measurable_on Y ) ) by Def2; hence f + g is Real-Valued-Random-Variable of Sigma by Def2, MESFUNC6:26; ::_thesis: verum end; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let f, g be Real-Valued-Random-Variable of Sigma; :: original: + redefine funcf + g -> Real-Valued-Random-Variable of Sigma; correctness coherence f + g is Real-Valued-Random-Variable of Sigma; by Th18; end; theorem Th19: :: RANDOM_1:19 for Omega being non empty set for Sigma being SigmaField of Omega for f, g being Real-Valued-Random-Variable of Sigma holds f - g is Real-Valued-Random-Variable of Sigma proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for f, g being Real-Valued-Random-Variable of Sigma holds f - g is Real-Valued-Random-Variable of Sigma let Sigma be SigmaField of Omega; ::_thesis: for f, g being Real-Valued-Random-Variable of Sigma holds f - g is Real-Valued-Random-Variable of Sigma let f, g be Real-Valued-Random-Variable of Sigma; ::_thesis: f - g is Real-Valued-Random-Variable of Sigma A1: ex X being Element of Sigma st ( X = Omega & f is_measurable_on X ) by Def2; consider Y being Element of Sigma such that A2: Y = Omega and A3: g is_measurable_on Y by Def2; dom g = Y by A2, FUNCT_2:def_1; hence f - g is Real-Valued-Random-Variable of Sigma by A1, A2, A3, Def2, MESFUNC6:29; ::_thesis: verum end; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let f, g be Real-Valued-Random-Variable of Sigma; :: original: - redefine funcf - g -> Real-Valued-Random-Variable of Sigma; correctness coherence f - g is Real-Valued-Random-Variable of Sigma; by Th19; end; theorem Th20: :: RANDOM_1:20 for Omega being non empty set for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma for r being Real holds r (#) f is Real-Valued-Random-Variable of Sigma proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma for r being Real holds r (#) f is Real-Valued-Random-Variable of Sigma let Sigma be SigmaField of Omega; ::_thesis: for f being Real-Valued-Random-Variable of Sigma for r being Real holds r (#) f is Real-Valued-Random-Variable of Sigma let f be Real-Valued-Random-Variable of Sigma; ::_thesis: for r being Real holds r (#) f is Real-Valued-Random-Variable of Sigma let r be Real; ::_thesis: r (#) f is Real-Valued-Random-Variable of Sigma consider X being Element of Sigma such that A1: X = Omega and A2: f is_measurable_on X by Def2; dom f = X by A1, FUNCT_2:def_1; hence r (#) f is Real-Valued-Random-Variable of Sigma by A1, A2, Def2, MESFUNC6:21; ::_thesis: verum end; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let f be Real-Valued-Random-Variable of Sigma; let r be Real; :: original: (#) redefine funcr (#) f -> Real-Valued-Random-Variable of Sigma; correctness coherence r (#) f is Real-Valued-Random-Variable of Sigma; by Th20; end; theorem Th21: :: RANDOM_1:21 for Omega being non empty set for f, g being PartFunc of Omega,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) proof let Omega be non empty set ; ::_thesis: for f, g being PartFunc of Omega,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) let f, g be PartFunc of Omega,REAL; ::_thesis: (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) 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__::_thesis:_for_x_being_set_st_x_in_dom_((R_EAL_f)_(#)_(R_EAL_g))_holds_ ((R_EAL_f)_(#)_(R_EAL_g))_._x_=_(f_(#)_g)_._x let x be set ; ::_thesis: ( x in dom ((R_EAL f) (#) (R_EAL g)) implies ((R_EAL f) (#) (R_EAL g)) . x = (f (#) g) . x ) assume A2: x in dom ((R_EAL f) (#) (R_EAL g)) ; ::_thesis: ((R_EAL f) (#) (R_EAL g)) . x = (f (#) g) . x hence ((R_EAL f) (#) (R_EAL g)) . x = ((R_EAL f) . x) * ((R_EAL g) . x) by MESFUNC1:def_5 .= (f . x) * (g . x) by EXTREAL1:1 .= (f (#) g) . x by A1, A2, VALUED_1:def_4 ; ::_thesis: verum end; hence (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th22: :: RANDOM_1:22 for Omega being non empty set for Sigma being SigmaField of Omega for f, g being Real-Valued-Random-Variable of Sigma holds f (#) g is Real-Valued-Random-Variable of Sigma proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for f, g being Real-Valued-Random-Variable of Sigma holds f (#) g is Real-Valued-Random-Variable of Sigma let Sigma be SigmaField of Omega; ::_thesis: for f, g being Real-Valued-Random-Variable of Sigma holds f (#) g is Real-Valued-Random-Variable of Sigma let f, g be Real-Valued-Random-Variable of Sigma; ::_thesis: f (#) g is Real-Valued-Random-Variable of Sigma consider X being Element of Sigma such that A1: X = Omega and A2: f is_measurable_on X by Def2; A3: R_EAL f is_measurable_on X by A2, MESFUNC6:def_1; ( dom (R_EAL f) = X & dom (R_EAL g) = X ) by A1, FUNCT_2:def_1; then A4: (dom (R_EAL f)) /\ (dom (R_EAL g)) = X ; ex Y being Element of Sigma st ( Y = Omega & g is_measurable_on Y ) by Def2; then R_EAL g is_measurable_on X by A1, MESFUNC6:def_1; then (R_EAL f) (#) (R_EAL g) is_measurable_on X by A3, A4, MESFUNC7:15; then R_EAL (f (#) g) is_measurable_on X by Th21; then f (#) g is_measurable_on X by MESFUNC6:def_1; hence f (#) g is Real-Valued-Random-Variable of Sigma by A1, Def2; ::_thesis: verum end; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let f, g be Real-Valued-Random-Variable of Sigma; :: original: (#) redefine funcf (#) g -> Real-Valued-Random-Variable of Sigma; correctness coherence f (#) g is Real-Valued-Random-Variable of Sigma; by Th22; end; theorem Th23: :: RANDOM_1:23 for Omega being non empty set for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma for r being real number st 0 <= r & f is nonnegative holds f to_power r is Real-Valued-Random-Variable of Sigma proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma for r being real number st 0 <= r & f is nonnegative holds f to_power r is Real-Valued-Random-Variable of Sigma let Sigma be SigmaField of Omega; ::_thesis: for f being Real-Valued-Random-Variable of Sigma for r being real number st 0 <= r & f is nonnegative holds f to_power r is Real-Valued-Random-Variable of Sigma let f be Real-Valued-Random-Variable of Sigma; ::_thesis: for r being real number st 0 <= r & f is nonnegative holds f to_power r is Real-Valued-Random-Variable of Sigma let r be real number ; ::_thesis: ( 0 <= r & f is nonnegative implies f to_power r is Real-Valued-Random-Variable of Sigma ) assume A1: ( 0 <= r & f is nonnegative ) ; ::_thesis: f to_power r is Real-Valued-Random-Variable of Sigma 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; consider X being Element of Sigma such that A4: X = Omega and A5: f is_measurable_on X by Def2; dom f = X by A4, FUNCT_2:def_1; hence f to_power r is Real-Valued-Random-Variable of Sigma by A1, A4, A5, A3, Def2, MESFUN6C:29; ::_thesis: verum end; Lm12: for X being non empty set for f being PartFunc of X,REAL holds abs f is nonnegative proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds abs f is nonnegative let f be PartFunc of X,REAL; ::_thesis: abs f is nonnegative now__::_thesis:_for_x_being_set_st_x_in_dom_(abs_f)_holds_ 0_<=_(abs_f)_._x let x be set ; ::_thesis: ( x in dom (abs f) implies 0 <= (abs f) . x ) assume x in dom (abs f) ; ::_thesis: 0 <= (abs f) . x then (abs f) . x = abs (f . x) by VALUED_1:def_11; hence 0 <= (abs f) . x by COMPLEX1:46; ::_thesis: verum end; hence abs f is nonnegative by MESFUNC6:52; ::_thesis: verum end; theorem Th24: :: RANDOM_1:24 for Omega being non empty set for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma holds abs f is Real-Valued-Random-Variable of Sigma proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma holds abs f is Real-Valued-Random-Variable of Sigma let Sigma be SigmaField of Omega; ::_thesis: for f being Real-Valued-Random-Variable of Sigma holds abs f is Real-Valued-Random-Variable of Sigma let f be Real-Valued-Random-Variable of Sigma; ::_thesis: abs f is Real-Valued-Random-Variable of Sigma consider X being Element of Sigma such that A1: X = Omega and A2: f is_measurable_on X by Def2; ( dom f = X & R_EAL f is_measurable_on X ) by A1, A2, FUNCT_2:def_1, MESFUNC6:def_1; then |.(R_EAL f).| is_measurable_on X by MESFUNC2:27; then R_EAL (abs f) is_measurable_on X by MESFUNC6:1; then abs f is_measurable_on X by MESFUNC6:def_1; hence abs f is Real-Valued-Random-Variable of Sigma by A1, Def2; ::_thesis: verum end; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let f be Real-Valued-Random-Variable of Sigma; :: original: |. redefine func abs f -> Real-Valued-Random-Variable of Sigma; correctness coherence |.f.| is Real-Valued-Random-Variable of Sigma; by Th24; end; theorem :: RANDOM_1:25 for Omega being non empty set for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma for r being real number st 0 <= r holds (abs f) to_power r is Real-Valued-Random-Variable of Sigma proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma for r being real number st 0 <= r holds (abs f) to_power r is Real-Valued-Random-Variable of Sigma let Sigma be SigmaField of Omega; ::_thesis: for f being Real-Valued-Random-Variable of Sigma for r being real number st 0 <= r holds (abs f) to_power r is Real-Valued-Random-Variable of Sigma let f be Real-Valued-Random-Variable of Sigma; ::_thesis: for r being real number st 0 <= r holds (abs f) to_power r is Real-Valued-Random-Variable of Sigma let r be real number ; ::_thesis: ( 0 <= r implies (abs f) to_power r is Real-Valued-Random-Variable of Sigma ) assume A1: 0 <= r ; ::_thesis: (abs f) to_power r is Real-Valued-Random-Variable of Sigma abs f is nonnegative by Lm12; hence (abs f) to_power r is Real-Valued-Random-Variable of Sigma by A1, Th23; ::_thesis: verum end; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let f be Real-Valued-Random-Variable of Sigma; let P be Probability of Sigma; predf is_integrable_on P means :Def3: :: RANDOM_1:def 3 f is_integrable_on P2M P; end; :: deftheorem Def3 defines is_integrable_on RANDOM_1:def_3_:_ for Omega being non empty set for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma for P being Probability of Sigma holds ( f is_integrable_on P iff f is_integrable_on P2M P ); definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let P be Probability of Sigma; let f be Real-Valued-Random-Variable of Sigma; assume A1: f is_integrable_on P ; func expect (f,P) -> Element of REAL equals :Def4: :: RANDOM_1:def 4 Integral ((P2M P),f); correctness coherence Integral ((P2M P),f) is Element of REAL ; proof f is_integrable_on P2M P by A1, Def3; then ( -infty < Integral ((P2M P),f) & Integral ((P2M P),f) < +infty ) by MESFUNC6:90; hence Integral ((P2M P),f) is Element of REAL by XXREAL_0:48; ::_thesis: verum end; end; :: deftheorem Def4 defines expect RANDOM_1:def_4_:_ for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for f being Real-Valued-Random-Variable of Sigma st f is_integrable_on P holds expect (f,P) = Integral ((P2M P),f); theorem Th26: :: RANDOM_1:26 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for f, g being Real-Valued-Random-Variable of Sigma st f is_integrable_on P & g is_integrable_on P holds expect ((f + g),P) = (expect (f,P)) + (expect (g,P)) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for f, g being Real-Valued-Random-Variable of Sigma st f is_integrable_on P & g is_integrable_on P holds expect ((f + g),P) = (expect (f,P)) + (expect (g,P)) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for f, g being Real-Valued-Random-Variable of Sigma st f is_integrable_on P & g is_integrable_on P holds expect ((f + g),P) = (expect (f,P)) + (expect (g,P)) let P be Probability of Sigma; ::_thesis: for f, g being Real-Valued-Random-Variable of Sigma st f is_integrable_on P & g is_integrable_on P holds expect ((f + g),P) = (expect (f,P)) + (expect (g,P)) let f, g be Real-Valued-Random-Variable of Sigma; ::_thesis: ( f is_integrable_on P & g is_integrable_on P implies expect ((f + g),P) = (expect (f,P)) + (expect (g,P)) ) set h = f + g; assume A1: ( f is_integrable_on P & g is_integrable_on P ) ; ::_thesis: expect ((f + g),P) = (expect (f,P)) + (expect (g,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, Def3; then consider E being 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; then A7: f | E = f by A4, FUNCT_2:33; f + g is_integrable_on P2M P by A3, MESFUNC6:100; then f + g is_integrable_on P by Def3; hence expect ((f + g),P) = Integral ((P2M P),(f + g)) by Def4 .= (Integral ((P2M P),f)) + (Integral ((P2M P),g)) by A4, A5, A6, A7, FUNCT_2:33 .= (expect (f,P)) + (expect (g,P)) by A2, SUPINF_2:1 ; ::_thesis: verum end; theorem Th27: :: RANDOM_1:27 for Omega being non empty set for r being Real for Sigma being SigmaField of Omega for P being Probability of Sigma for f being Real-Valued-Random-Variable of Sigma st f is_integrable_on P holds expect ((r (#) f),P) = r * (expect (f,P)) proof let Omega be non empty set ; ::_thesis: for r being Real for Sigma being SigmaField of Omega for P being Probability of Sigma for f being Real-Valued-Random-Variable of Sigma st f is_integrable_on P holds expect ((r (#) f),P) = r * (expect (f,P)) let r be Real; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for f being Real-Valued-Random-Variable of Sigma st f is_integrable_on P holds expect ((r (#) f),P) = r * (expect (f,P)) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for f being Real-Valued-Random-Variable of Sigma st f is_integrable_on P holds expect ((r (#) f),P) = r * (expect (f,P)) let P be Probability of Sigma; ::_thesis: for f being Real-Valued-Random-Variable of Sigma st f is_integrable_on P holds expect ((r (#) f),P) = r * (expect (f,P)) let f be Real-Valued-Random-Variable of Sigma; ::_thesis: ( f is_integrable_on P implies expect ((r (#) f),P) = r * (expect (f,P)) ) set h = r (#) f; assume A1: f is_integrable_on P ; ::_thesis: expect ((r (#) f),P) = r * (expect (f,P)) then A2: Integral ((P2M P),f) = expect (f,P) by Def4; A3: f is_integrable_on P2M P by A1, Def3; then r (#) f is_integrable_on P2M P by MESFUNC6:102; then r (#) f is_integrable_on P by Def3; hence expect ((r (#) f),P) = Integral ((P2M P),(r (#) f)) by Def4 .= (R_EAL r) * (Integral ((P2M P),f)) by A3, MESFUNC6:102 .= r * (expect (f,P)) by A2, EXTREAL1:1 ; ::_thesis: verum end; theorem :: RANDOM_1:28 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for f, g being Real-Valued-Random-Variable of Sigma st f is_integrable_on P & g is_integrable_on P holds expect ((f - g),P) = (expect (f,P)) - (expect (g,P)) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for f, g being Real-Valued-Random-Variable of Sigma st f is_integrable_on P & g is_integrable_on P holds expect ((f - g),P) = (expect (f,P)) - (expect (g,P)) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for f, g being Real-Valued-Random-Variable of Sigma st f is_integrable_on P & g is_integrable_on P holds expect ((f - g),P) = (expect (f,P)) - (expect (g,P)) let P be Probability of Sigma; ::_thesis: for f, g being Real-Valued-Random-Variable of Sigma st f is_integrable_on P & g is_integrable_on P holds expect ((f - g),P) = (expect (f,P)) - (expect (g,P)) let f, g be Real-Valued-Random-Variable of Sigma; ::_thesis: ( f is_integrable_on P & g is_integrable_on P implies expect ((f - g),P) = (expect (f,P)) - (expect (g,P)) ) assume that A1: f is_integrable_on P and A2: g is_integrable_on P ; ::_thesis: expect ((f - g),P) = (expect (f,P)) - (expect (g,P)) g is_integrable_on P2M P by A2, Def3; then (- 1) (#) g is_integrable_on P2M P by MESFUNC6:102; then (- 1) (#) g is_integrable_on P by Def3; hence expect ((f - g),P) = (expect (f,P)) + (expect (((- 1) (#) g),P)) by A1, Th26 .= (expect (f,P)) + ((- 1) * (expect (g,P))) by A2, Th27 .= (expect (f,P)) - (expect (g,P)) ; ::_thesis: verum end; theorem :: RANDOM_1:29 for Omega being non empty finite set for f being Function of Omega,REAL holds f is Real-Valued-Random-Variable of Trivial-SigmaField Omega proof let Omega be non empty finite set ; ::_thesis: for f being Function of Omega,REAL holds f is Real-Valued-Random-Variable of Trivial-SigmaField Omega let f be Function of Omega,REAL; ::_thesis: f is Real-Valued-Random-Variable of Trivial-SigmaField Omega set Sigma = Trivial-SigmaField Omega; ( ex X being Element of Trivial-SigmaField Omega st ( dom f = X & f is_measurable_on X ) & dom f = Omega ) by Th8, FUNCT_2:def_1; hence f is Real-Valued-Random-Variable of Trivial-SigmaField Omega by Def2; ::_thesis: verum end; theorem Th30: :: RANDOM_1:30 for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega holds X is_integrable_on P proof let Omega be non empty finite set ; ::_thesis: for P being Probability of Trivial-SigmaField Omega for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega holds X is_integrable_on P let P be Probability of Trivial-SigmaField Omega; ::_thesis: for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega holds X is_integrable_on P let X be Real-Valued-Random-Variable of Trivial-SigmaField Omega; ::_thesis: X is_integrable_on P set M = P2M P; dom X = Omega by FUNCT_2:def_1; then (P2M P) . (dom X) = 1 by PROB_1:def_8; then (P2M P) . (dom X) < +infty by XXREAL_0:9; then X is_integrable_on P2M P by Lm5, Th6; hence X is_integrable_on P by Def3; ::_thesis: verum end; theorem Th31: :: RANDOM_1:31 for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega for F being FinSequence of REAL for 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 ; ::_thesis: for P being Probability of Trivial-SigmaField Omega for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega for F being FinSequence of REAL for 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 let P be Probability of Trivial-SigmaField Omega; ::_thesis: for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega for F being FinSequence of REAL for 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 let X be Real-Valued-Random-Variable of Trivial-SigmaField Omega; ::_thesis: for F being FinSequence of REAL for 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 let F be FinSequence of REAL ; ::_thesis: for 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 let s be FinSequence of Omega; ::_thesis: ( 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)}) ) implies expect (X,P) = Sum F ) 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)}) ) ) ; ::_thesis: expect (X,P) = Sum F then Integral ((P2M P),X) = Sum F by Th12; hence expect (X,P) = Sum F by Def4, Th30; ::_thesis: verum end; theorem :: RANDOM_1:32 for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex F being FinSequence of REAL ex 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 ; ::_thesis: for P being Probability of Trivial-SigmaField Omega for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex F being FinSequence of REAL ex 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 ) let P be Probability of Trivial-SigmaField Omega; ::_thesis: for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex F being FinSequence of REAL ex 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 ) let X be Real-Valued-Random-Variable of Trivial-SigmaField Omega; ::_thesis: ex F being FinSequence of REAL ex 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 ) ( X is_integrable_on P & ex F being FinSequence of REAL ex 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 ex F being FinSequence of REAL ex 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 ) by Def4; ::_thesis: verum end; theorem Th33: :: RANDOM_1:33 for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex F being FinSequence of REAL ex 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 ; ::_thesis: for P being Probability of Trivial-SigmaField Omega for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex F being FinSequence of REAL ex 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 ) let P be Probability of Trivial-SigmaField Omega; ::_thesis: for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex F being FinSequence of REAL ex 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 ) let X be Real-Valued-Random-Variable of Trivial-SigmaField Omega; ::_thesis: ex F being FinSequence of REAL ex 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 ) ( X is_integrable_on P & ex F being FinSequence of REAL ex 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 ex F being FinSequence of REAL ex 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 ) by Def4; ::_thesis: verum end; theorem :: RANDOM_1:34 for Omega being non empty finite set for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega for G being FinSequence of REAL for 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 ; ::_thesis: for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega for G being FinSequence of REAL for 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) let X be Real-Valued-Random-Variable of Trivial-SigmaField Omega; ::_thesis: for G being FinSequence of REAL for 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) let G be FinSequence of REAL ; ::_thesis: for 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) let s be FinSequence of Omega; ::_thesis: ( 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) ) implies expect (X,(Trivial-Probability Omega)) = (Sum G) / (card 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) ; ::_thesis: expect (X,(Trivial-Probability Omega)) = (Sum G) / (card Omega) set P = Trivial-Probability Omega; deffunc H1( Nat) -> Element of REAL = (X . (s . $1)) * ((Trivial-Probability Omega) . {(s . $1)}); 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 = H1(j) ) ) from FINSEQ_2:sch_1(); A6: dom F = dom G by A5, FINSEQ_3:29; A7: now__::_thesis:_for_n_being_Nat_st_n_in_dom_F_holds_ ((1_/_(card_Omega))_(#)_G)_._n_=_F_._n let n be Nat; ::_thesis: ( n in dom F implies ((1 / (card Omega)) (#) G) . n = F . n ) assume A8: n in dom F ; ::_thesis: ((1 / (card Omega)) (#) G) . n = F . n 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 A8, PARTFUN1:4; then reconsider A = {(s . n)} as Singleton of Omega by RPR_1:4; A9: (Trivial-Probability Omega) . {(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)) * (X . (s . n)) by A4, A6, A8 .= F . n by A5, A8, A9 ; ::_thesis: verum end; dom F = dom ((1 / (card Omega)) (#) G) by A6, VALUED_1:def_5; then (1 / (card Omega)) (#) G = F by A7, FINSEQ_1:13; then expect (X,(Trivial-Probability Omega)) = Sum ((1 / (card Omega)) (#) G) by A1, A2, A3, A5, Th31 .= (Sum G) / (card Omega) by RVSUM_1:87 ; hence expect (X,(Trivial-Probability Omega)) = (Sum G) / (card Omega) ; ::_thesis: verum end; theorem :: RANDOM_1:35 for Omega being non empty finite set for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex G being FinSequence of REAL ex 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 ; ::_thesis: for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex G being FinSequence of REAL ex 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) ) let X be Real-Valued-Random-Variable of Trivial-SigmaField Omega; ::_thesis: ex G being FinSequence of REAL ex 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) ) 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)) * ((Trivial-Probability Omega) . {(s . n)}) and A5: expect (X,(Trivial-Probability Omega)) = Sum F by Th33; deffunc H1( Nat) -> Element of REAL = X . (s . $1); 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 = H1(j) ) ) from FINSEQ_2:sch_1(); A7: dom F = dom G by A6, FINSEQ_3:29; A8: now__::_thesis:_for_n_being_Nat_st_n_in_dom_F_holds_ ((1_/_(card_Omega))_(#)_G)_._n_=_F_._n let n be Nat; ::_thesis: ( n in dom F implies ((1 / (card Omega)) (#) G) . n = F . n ) assume A9: n in dom F ; ::_thesis: ((1 / (card Omega)) (#) G) . n = F . n 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: (Trivial-Probability Omega) . {(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)) * (X . (s . n)) by A6, A7, A9 .= F . n by A4, A9, A10 ; ::_thesis: verum end; take G ; ::_thesis: ex 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) ) dom F = dom ((1 / (card Omega)) (#) G) by A7, VALUED_1:def_5; then (1 / (card Omega)) (#) G = F by A8, FINSEQ_1:13; hence ex 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) ) by A1, A2, A3, A5, A6, RVSUM_1:87; ::_thesis: verum end; theorem :: RANDOM_1:36 for Omega being non empty set for r being Real for Sigma being SigmaField of Omega for P being Probability of Sigma for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P holds P . { t where t is Element of Omega : r <= X . t } <= (expect (X,P)) / r proof let Omega be non empty set ; ::_thesis: for r being Real for Sigma being SigmaField of Omega for P being Probability of Sigma for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P holds P . { t where t is Element of Omega : r <= X . t } <= (expect (X,P)) / r let r be Real; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P holds P . { t where t is Element of Omega : r <= X . t } <= (expect (X,P)) / r let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P holds P . { t where t is Element of Omega : r <= X . t } <= (expect (X,P)) / r let P be Probability of Sigma; ::_thesis: for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P holds P . { t where t is Element of Omega : r <= X . t } <= (expect (X,P)) / r let X be Real-Valued-Random-Variable of Sigma; ::_thesis: ( 0 < r & X is nonnegative & X is_integrable_on P implies P . { t where t is Element of Omega : r <= X . t } <= (expect (X,P)) / r ) assume that A1: 0 < r and A2: X is nonnegative and A3: X is_integrable_on P ; ::_thesis: P . { t where t is Element of Omega : r <= X . t } <= (expect (X,P)) / r set PM = P2M P; set K = { t where t is Element of Omega : r <= X . t } ; consider S being Element of Sigma such that A4: S = Omega and A5: X is_measurable_on S by Def2; now__::_thesis:_for_t_being_set_st_t_in_S_/\_(great_eq_dom_(X,r))_holds_ t_in__{__t_where_t_is_Element_of_Omega_:_r_<=_X_._t__}_ let t be set ; ::_thesis: ( t in S /\ (great_eq_dom (X,r)) implies t in { t where t is Element of Omega : r <= X . t } ) assume t in S /\ (great_eq_dom (X,r)) ; ::_thesis: t in { t where t is Element of Omega : r <= X . t } 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 { t where t is Element of Omega : r <= X . t } ; ::_thesis: verum end; then A6: S /\ (great_eq_dom (X,r)) c= { t where t is Element of Omega : r <= X . t } by TARSKI:def_3; A7: dom X = S by A4, FUNCT_2:def_1; now__::_thesis:_for_x_being_set_st_x_in__{__t_where_t_is_Element_of_Omega_:_r_<=_X_._t__}__holds_ x_in_S_/\_(great_eq_dom_(X,r)) let x be set ; ::_thesis: ( x in { t where t is Element of Omega : r <= X . t } implies x in S /\ (great_eq_dom (X,r)) ) assume x in { t where t is Element of Omega : r <= X . t } ; ::_thesis: x in S /\ (great_eq_dom (X,r)) then A8: ex t being Element of Omega st ( x = t & r <= X . t ) ; then x in great_eq_dom (X,r) by A4, A7, MESFUNC1:def_14; hence x in S /\ (great_eq_dom (X,r)) by A4, A8, XBOOLE_0:def_4; ::_thesis: verum end; then { t where t is Element of Omega : r <= X . t } c= S /\ (great_eq_dom (X,r)) by TARSKI:def_3; then S /\ (great_eq_dom (X,r)) = { t where t is Element of Omega : r <= X . t } by A6, XBOOLE_0:def_10; then reconsider K = { t where t is Element of Omega : r <= X . t } as Element of Sigma by A5, A7, MESFUNC6:13; Integral ((P2M P),(X | K)) <= Integral ((P2M P),(X | S)) by A2, A4, A5, A7, MESFUNC6:87; then A9: Integral ((P2M P),(X | K)) <= Integral ((P2M P),X) by A4, FUNCT_2:33; expect (X,P) = Integral ((P2M P),X) by A3, Def4; then reconsider IX = Integral ((P2M P),X) as Element of REAL ; reconsider PMK = (P2M P) . K as Element of REAL by XXREAL_0:14; A10: for t being Element of Omega st t in K holds r <= X . t proof let t be Element of Omega; ::_thesis: ( t in K implies r <= X . t ) assume t in K ; ::_thesis: r <= X . t then ex s being Element of Omega st ( s = t & r <= X . s ) ; hence r <= X . t ; ::_thesis: verum end; (P2M P) . K <= 1 by PROB_1:35; then A11: (P2M P) . K < +infty by XXREAL_0:2, XXREAL_0:9; X is_integrable_on P2M P by A3, Def3; then (R_EAL r) * ((P2M P) . K) <= Integral ((P2M P),(X | K)) by A4, A7, A11, A10, Th2; then r * PMK <= Integral ((P2M P),(X | K)) by EXTREAL1:1; then r * PMK <= Integral ((P2M P),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 P . { t where t is Element of Omega : r <= X . t } <= (expect (X,P)) / r by A3, Def4; ::_thesis: verum end;