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