:: 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;