:: Probability Measure on Discrete Spaces and Algebra of Real Valued Random
:: Variables
:: by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received March 16, 2010
:: Copyright (c) 2010-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 FUNCT_1, COMPLEX1, RELAT_1, ZFMISC_1, XXREAL_0, PARTFUN1,
ARYTM_1, XBOOLE_0, ORDINAL4, INT_1, SQUARE_1, ARYTM_3, RLVECT_1,
SUPINF_2, RSSPACE, FUNCOP_1, FINSOP_1, NAT_1, FUNCT_4, BINOP_2, PROB_1,
MEASURE6, MESFUNC1, TARSKI, MESFUNC5, IDEAL_1, SUBSET_1, RANDOM_1,
RANDOM_2, C0SP1, FINSET_1, FINSEQ_1, ORDINAL2, RPR_1, CARD_1, SEQ_2,
POWER, FUNCT_3, PROB_4, UPROOTS, FINSEQ_2, CARD_3, FUNCT_2, RFINSEQ,
FUNCSDOM, POLYALG1, BHSP_5, NUMBERS, REAL_1, INTEGRA5, VALUED_1, EQREL_1,
XCMPLX_0, SUPINF_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, FINSEQ_1, ORDINAL1, REAL_1, CARD_1,
FINSET_1, NUMBERS, SUPINF_1, XXREAL_0,
XXREAL_3, XCMPLX_0, COMPLEX1, XREAL_0,
SUPINF_2, VALUED_0, FINSEQ_2, NAT_D, RFINSEQ, FINSOP_1,
STRUCT_0, IDEAL_1, BINOP_1, BINOP_2, RLVECT_1, FUNCSDOM, SEQ_2, SQUARE_1,
GROUP_1, POWER, PROB_1, PROB_4, EXTREAL1, MESFUNC1,
VALUED_1, MEASURE6, MESFUNC5,
MESFUNC6, MESFUNC2, RVSUM_1, UPROOTS, MESFUN6C, C0SP1, RANDOM_1, BHSP_5;
constructors EXTREAL1, REAL_1, IDEAL_1, MEASURE6, MESFUNC2, MESFUNC5,
MESFUNC6, SUPINF_1, REALSET1, RVSUM_1, MESFUNC1, RELSET_1, RANDOM_1,
C0SP1, RFINSEQ, POWER, FINSOP_1, BINARITH, FINSEQOP, SETWISEO, PROB_4,
WELLORD2, SQUARE_1, NAT_D, UPROOTS, MESFUN6C, BHSP_5, COMSEQ_2, BINOP_2,
NUMBERS;
registrations XBOOLE_0, ORDINAL1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, NAT_1,
SUBSET_1, XCMPLX_0, XXREAL_0, MEASURE1, FINSEQ_1, RELAT_1, XXREAL_3,
C0SP1, FUNCT_2, CARD_1, FINSET_1, BINOP_2, FUNCT_1, MESFUN6C, FUNCSDOM,
RELSET_1, SQUARE_1, INT_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, RLVECT_1;
equalities BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1, MESFUNC5, FINSEQ_2,
FINSEQ_1, PROB_4, FUNCSDOM, VALUED_1, BHSP_5, RVSUM_1, SQUARE_1,
ORDINAL1, PROB_1;
expansions TARSKI, FINSEQ_1;
theorems FUNCT_1, FUNCT_2, PARTFUN1, COMPLEX1, XBOOLE_0, TARSKI, RELAT_1,
VALUED_1, IDEAL_1, ZFMISC_1, RLVECT_1, FUNCOP_1, XBOOLE_1, MESFUNC2,
EXTREAL1, MEASURE1, MESFUNC6, PROB_1, XXREAL_0, ABSVALUE, MESFUNC7,
RELSET_1, XXREAL_3, XREAL_0, RANDOM_1, C0SP1, FINSEQ_4, POWER, BINOP_2,
RFINSEQ, CARD_2, FINSEQ_1, FUNCT_4, FINSOP_1, NAT_1, NAT_2, NAT_D,
XREAL_1, SQUARE_1, FINSEQ_2, INT_1, FUNCT_3, CARD_1, FINSEQ_3, FINSEQ_5,
MESFUN6C, FUNCSDOM, BHSP_5, RVSUM_1, FIB_NUM3, SUBSET, XTUPLE_0,
ORDINAL1, NUMBERS;
schemes FINSEQ_1, FUNCT_2, NAT_1, FUNCT_3;
begin
reserve Omega for non empty set;
reserve r for Real;
reserve Sigma for SigmaField of Omega;
reserve P for Probability of Sigma;
theorem Th1:
for f be one-to-one Function, A,B be set st A misses B holds
rng (f|A) misses rng (f|B)
proof
let f be one-to-one Function, A,B be set;
assume A1:A misses B;
assume rng (f|A) meets rng (f|B);then
consider y be object such that
A2: y in rng (f|A) & y in rng (f|B) by XBOOLE_0:3;
consider xa be object such that
A3: xa in dom (f|A) & y = (f|A).xa by A2,FUNCT_1:def 3;
consider xb be object such that
A4: xb in dom (f|B) & y = (f|B).xb by A2,FUNCT_1:def 3;
A5:xa in dom f & xb in dom f by A3,A4,RELAT_1:57;
y=f.xa &y=f.xb by A3,A4,FUNCT_1:47;then
A6:xa=xb by A5,FUNCT_1:def 4;
dom (f|A) c= A & dom (f|B) c=B by RELAT_1:58;
then xa in A /\ B by A6,A3,A4,XBOOLE_0:def 4;
hence contradiction by A1,XBOOLE_0:4;
end;
theorem Th2:
for f,g be Function holds rng (f*g) c= rng (f|(rng g))
proof
let f,g be Function;
let y be object;
assume y in rng(f*g);then
consider x be object such that
A1: x in dom (f*g) & y=(f*g).x by FUNCT_1:def 3;
A2: x in dom g & g.x in dom f by A1,FUNCT_1:11;
reconsider z=g.x as set;
f.z in rng (f|(rng g)) by A2,FUNCT_1:3,50;
hence thesis by A1,FUNCT_1:12;
end;
registration let Omega,Sigma;
cluster nonnegative for Real-Valued-Random-Variable of Sigma;
existence
proof
set X = the Real-Valued-Random-Variable of Sigma;
now let x be object;
assume x in dom abs X;
then (abs X).x = |.X.x qua Complex.| by VALUED_1:def 11;
hence 0 <= (abs X).x by COMPLEX1:46;
end; then
abs X is nonnegative by MESFUNC6:52;
hence thesis;
end;
end;
registration let Omega,Sigma;
let X be Real-Valued-Random-Variable of Sigma;
cluster abs X -> nonnegative;
coherence
proof
now let x be object;
assume x in dom (abs X);
then (abs X).x = |.X.x qua Complex.| by VALUED_1:def 11;
hence 0 <= (abs X).x by COMPLEX1:46;
end;
hence thesis by MESFUNC6:52;
end;
end;
theorem Th3:
(Omega --> 1) = chi(Omega, Omega)
proof
set E0 = (Omega --> 1);
A1: dom (chi(Omega,Omega)) = Omega by FUNCT_3:def 3;
A2: dom E0 = Omega by FUNCT_2:def 1;
now let x be object;
assume A3:x in dom (chi(Omega,Omega));
per cases;
suppose x in Omega;
hence (chi(Omega,Omega)).x = 1 by FUNCT_3:def 3
.=E0.x by A3,FUNCOP_1:7;
end;
suppose not x in Omega;
hence (chi(Omega,Omega)).x=E0.x by A3;
end;
end;
hence thesis by A1,A2,FUNCT_1:2;
end;
theorem Th4:
Omega --> r is Real-Valued-Random-Variable of Sigma
proof
set E0 = (Omega --> 1);
set E = (Omega --> r);
reconsider S= Omega as Element of Sigma by MEASURE1:7;
A1: dom E0 = Omega & rng E0 c= {1} by FUNCOP_1:13;
reconsider E0 as Function of Omega, REAL by FUNCT_2:7,NUMBERS:19;
A2: R_EAL E0 =chi(S,Omega) by Th3;
chi(S,Omega) is S-measurable by MESFUNC2:29; then
A3: E0 is Real-Valued-Random-Variable of Sigma
by A2,MESFUNC6:def 1;
A4: dom E = dom E0 by A1,FUNCT_2:def 1;
now let x be object;
assume
A5:x in dom E;
hence E.x = r*1 by FUNCOP_1:7
.= r*(E0.x) by A5,FUNCOP_1:7;
end; then
E = r(#) E0 by A4,VALUED_1:def 5;
hence thesis by A3,RANDOM_1:20;
end;
theorem Th5:
for X be non empty set, f be PartFunc of X,REAL holds
f to_power 2 = (-f) to_power 2 &
f to_power 2 = (abs(f)) to_power 2
proof
let X be non empty set, f be PartFunc of X,REAL;
dom (-f) = dom f by VALUED_1:8;
then dom((-f) to_power 2)= dom f by MESFUN6C:def 4;
then A1:dom(f to_power 2)= dom((-f) to_power 2) by MESFUN6C:def 4;
dom abs f = dom f by VALUED_1:def 11;
then A2:dom((abs f) to_power 2)= dom f by MESFUN6C:def 4;
then A3:
dom(f to_power 2)= dom((abs(f)) to_power 2) by MESFUN6C:def 4;
for x be Element of X st x in dom(f to_power 2)
holds (f to_power 2).x=((-f) to_power 2).x&
(f to_power 2).x =((abs(f)) to_power 2).x
proof
let x be Element of X;
assume A4: x in dom(f to_power 2);
then A5: x in dom((-f) to_power 2) &
x in dom(f to_power 2) & x in dom f & x in dom (-f) &
x in dom((abs(f)) to_power 2) by A2,A1,MESFUN6C:def 4;
A6: ((-f) to_power 2).x = (((-f).x) to_power 2)
by A4,A1,MESFUN6C:def 4
.= ((-(f.x)) to_power 2) by VALUED_1:8
.= ((f.x) to_power 2) by FIB_NUM3:3
.=(f to_power 2).x by A4,MESFUN6C:def 4;
A7: ((abs(f)) to_power 2).x = ((abs(f)).x) to_power 2
by A5,MESFUN6C:def 4
.= |.f.x qua Complex.| to_power 2 by VALUED_1:18;
((abs(f)) to_power 2).x = (f to_power 2).x
proof
per cases by A7,ABSVALUE:1;
suppose ((abs(f)) to_power 2).x = (f.x) to_power 2;
hence thesis by A4,MESFUN6C:def 4;
end;
suppose ((abs(f)) to_power 2).x = (-(f.x)) to_power 2; then
((abs(f)) to_power 2).x =((f.x) to_power 2) by FIB_NUM3:3
.=(f to_power 2).x by A4,MESFUN6C:def 4;
hence thesis;
end;
end;
hence thesis by A6;
end;then
(for x be Element of X st x in dom(f to_power 2)
holds (f to_power 2).x=((-f) to_power 2).x)&
(for x be Element of X st x in dom(f to_power 2) holds
(f to_power 2).x =((abs(f)) to_power 2).x);
hence thesis by A1,A3,PARTFUN1:5;
end;
theorem Th6:
for X be non empty set, f,g be PartFunc of X,REAL holds
(f+g) to_power 2 = (f to_power 2) + 2(#)(f(#)g) + (g to_power 2) &
(f-g) to_power 2 = (f to_power 2) - 2(#)(f(#)g) + (g to_power 2)
proof
let X be non empty set, f,g be PartFunc of X,REAL;
A1: dom ((f to_power 2)) = dom f
& for x be Element of X st x in dom ((f to_power 2)) holds
((f to_power 2)).x = (f.x) to_power 2 by MESFUN6C:def 4;
A2: dom (g to_power 2) = dom g
& for x be Element of X st x in dom (g to_power 2) holds
(g to_power 2).x = (g.x) to_power 2 by MESFUN6C:def 4;
A3: dom (2(#)(f(#)g)) = dom (f(#)g) by VALUED_1:def 5
.= dom f /\ dom g by VALUED_1:def 4;
A4: now let x be Element of X;
assume x in (dom f /\ dom g);
thus (2(#)(f(#)g)).x = 2*((f(#)g).x) by VALUED_1:6
.= 2*((f.x)*(g.x)) by VALUED_1:5
.= 2*(f.x)*(g.x);
end;
A5: dom ((f+g) to_power 2) = dom (f+g) by MESFUN6C:def 4
.= dom f /\ dom g by VALUED_1:def 1;
A6:dom ((f-g) to_power 2) = dom (f-g) by MESFUN6C:def 4
.= dom f /\ dom g by VALUED_1:12;
A7: dom ((f to_power 2) + 2(#)(f(#)g))
= dom f /\ dom (2(#)(f(#)g)) by A1,VALUED_1:def 1
.= dom f /\ dom g by A3,XBOOLE_1:17,28;
A8: dom ((f to_power 2) - 2(#)(f(#)g))
= dom f /\ dom (2(#)(f(#)g)) by A1,VALUED_1:12
.= dom f /\ dom g by A3,XBOOLE_1:17,28;
A9: dom ((f to_power 2) + 2(#)(f(#)g) + (g to_power 2))
= dom ((f to_power 2) + 2(#)(f(#)g)) /\ dom g by A2,VALUED_1:def 1
.= (dom f) /\ dom (2(#)(f(#)g)) /\ dom g by A1,VALUED_1:def 1
.= (dom f /\ dom g) /\ dom g by A3,XBOOLE_1:17,28
.= dom f /\ dom g by XBOOLE_1:17,28;
A10: dom ((f to_power 2) - 2(#)(f(#)g) + (g to_power 2))
= dom ((f to_power 2) - 2(#)(f(#)g)) /\ dom g by A2,VALUED_1:def 1
.= dom f /\ dom g by A8,XBOOLE_1:17,28;
now let x be Element of X;
assume A11:x in dom f /\ dom g; then
A12:x in dom (f+g) by VALUED_1:def 1;
A13:x in dom f by A11,XBOOLE_0:def 4;
A14:x in dom g by A11,XBOOLE_0:def 4;
A15: x in dom (f-g) by A11,VALUED_1:12;then
A16:x in dom ((f-g) to_power 2) by MESFUN6C:def 4;
A17: ((f+g) to_power 2).x = ((f+g).x) to_power 2 by A11,A5,MESFUN6C:def 4
.= (f.x + g.x) to_power 2 by A12,VALUED_1:def 1
.= (f.x + g.x) ^2 by POWER:46
.= (f.x)^2 + 2*(f.x)*(g.x) + (g.x)^2
.= (f.x) to_power 2 + 2*(f.x)*(g.x) + (g.x)^2 by POWER:46
.= (f.x)to_power 2 + 2*(f.x)*(g.x) + (g.x) to_power 2 by POWER:46
.= (f to_power 2).x + 2*(f.x)*(g.x) + (g.x) to_power 2 by A1,A13
.= (f to_power 2).x + 2*(f.x)*(g.x) + (g to_power 2).x by A2,A14
.= (f to_power 2).x + (2(#)(f(#)g)).x + (g to_power 2).x by A4,A11
.= ((f to_power 2)+ (2(#)(f(#)g))).x + (g to_power 2).x
by A7,A11,VALUED_1:def 1
.= ((f to_power 2)+ (2(#)(f(#)g)) + (g to_power 2)).x
by A9,A11,VALUED_1:def 1;
((f-g) to_power 2).x = ((f-g).x) to_power 2 by A16,MESFUN6C:def 4
.= (f.x - g.x) to_power 2 by A15,VALUED_1:13
.= (f.x - g.x) ^2 by POWER:46
.= (f.x)^2 - 2*(f.x)*(g.x) + (g.x)^2
.= (f.x) to_power 2 - 2*(f.x)*(g.x) + (g.x)^2 by POWER:46
.= (f.x)to_power 2 - 2*(f.x)*(g.x) + (g.x) to_power 2 by POWER:46
.= (f to_power 2).x - 2*(f.x)*(g.x) + (g.x) to_power 2 by A1,A13
.= (f to_power 2).x - 2*(f.x)*(g.x) + (g to_power 2).x by A2,A14
.= (f to_power 2).x - (2(#)(f(#)g)).x + (g to_power 2).x by A4,A11
.= ((f to_power 2) - (2(#)(f(#)g))).x + (g to_power 2).x
by A8,A11,VALUED_1:13
.= ((f to_power 2) - (2(#)(f(#)g)) + (g to_power 2)).x
by A10,A11,VALUED_1:def 1;
hence ((f+g) to_power 2).x
= ((f to_power 2) + (2(#)(f(#)g)) + (g to_power 2)).x&
((f-g) to_power 2).x
=((f to_power 2) - (2(#)(f(#)g)) + (g to_power 2)).x by A17;
end; then
(for x be Element of X st x in dom ((f+g) to_power 2) holds
((f+g) to_power 2).x
= ((f to_power 2) + (2(#)(f(#)g)) + (g to_power 2)).x) &
(for x be Element of X st x in dom ((f-g) to_power 2) holds
((f-g) to_power 2).x
=((f to_power 2) - (2(#)(f(#)g)) + (g to_power 2)).x) by A5,A6;
hence thesis by A5,A9,A10,A6,PARTFUN1:5;
end;
definition let Omega,Sigma,P;
let X be Real-Valued-Random-Variable of Sigma;
assume A1: X is_integrable_on P
& (abs(X) to_power 2) is_integrable_on P2M(P);
func variance (X,P) -> Real means :Def1:
ex Y be Real-Valued-Random-Variable of Sigma,
E be Real-Valued-Random-Variable of Sigma
st E=(Omega --> expect(X,P)) & Y = X-E &
Y is_integrable_on P & abs(Y) to_power 2 is_integrable_on P2M(P) &
it=Integral(P2M(P),abs(Y) to_power 2);
correctness
proof
set S = [#]Sigma;
A3: 1 in REAL by XREAL_0:def 1;
(P2M(P)).S <=1 by PROB_1:35; then
A4: (P2M(P)).S < +infty by XXREAL_0:2,9,A3;
set r = expect(X,P);
set E0= (Omega -->1);
set E = (Omega --> expect(X,P));
A5: dom E0 = Omega & rng E0 c= {1} by FUNCOP_1:13;
reconsider E0 as
Real-Valued-Random-Variable of Sigma by Th4;
A6: R_EAL E0 =chi(S,Omega) by Th3;
A7: dom E = dom E0 by A5,FUNCT_2:def 1;
now let x be object;
assume A8: x in dom E;
hence E.x = r*1 by FUNCOP_1:7
.= r*(E0.x) by A8,FUNCOP_1:7;
end; then
A9: E = r(#) E0 by A7,VALUED_1:def 5;
reconsider E as Real-Valued-Random-Variable of Sigma by Th4;
set Y= X-E;
reconsider Y as Real-Valued-Random-Variable of Sigma;
chi(S,Omega) is_integrable_on (P2M(P)) by A4,MESFUNC7:24;
then
A10: E0 is_integrable_on P2M(P) by A6,MESFUNC6:def 4;
then
A11: r(#) E0 is_integrable_on P2M(P) by MESFUNC6:102;
A12: (-1)(#)( r(#) E0) is_integrable_on P2M(P) by A11,MESFUNC6:102;
A13: X is_integrable_on P2M(P) by A1,RANDOM_1:def 2;
then Y is_integrable_on P2M(P) by A9,A12,MESFUNC6:100;
then
A14: Y is_integrable_on P by RANDOM_1:def 2;
(2*r)(#)X is_integrable_on P2M(P) by A13,MESFUNC6:102;
then
(-1) (#)((2*r)(#)X) is_integrable_on P2M(P) by MESFUNC6:102;
then
A15: (abs(X) to_power 2) - (2*r)(#)X
is_integrable_on P2M(P) by A1,MESFUNC6:100;
A16:
(X to_power 2) - 2(#)((r(#)E0)(#)X) + ((r(#)E0) to_power 2)
=(X to_power 2) -(2*r)(#)X + (r*r)(#)E0
proof
A17:dom (X to_power 2) = dom X by MESFUN6C:def 4;
A18:dom (2(#)((r(#)E0)(#)X)) = dom ((r(#)E0)(#)X) by VALUED_1:def 5
.= dom (r(#)E0) /\ dom X by VALUED_1:def 4
.= Omega /\ dom X by A5,VALUED_1:def 5;
A19:
dom ((r(#)E0) to_power 2) = dom (r(#)E0) by MESFUN6C:def 4
.= Omega by A5,VALUED_1:def 5;
A20:dom ((r*r)(#)E0) = Omega by A5,VALUED_1:def 5;
A21:
dom ((2*r)(#)X)= dom X by VALUED_1:def 5;
A22:
dom ((X to_power 2) - (2(#)((r(#)E0)(#)X)))
=dom X /\ (Omega /\ dom X) by A17,A18,VALUED_1:12
.=(dom X /\ dom X) /\ Omega by XBOOLE_1:16
.= dom X /\ Omega;
A23:
dom ((X to_power 2) - ((2*r)(#)X))
= dom (X to_power 2) /\ dom ((2*r)(#)X) by VALUED_1:12
.=dom X by A17,A21;
A24:
dom((X to_power 2) - 2(#)((r(#)E0)(#)X) + ((r(#)E0) to_power 2))
=dom ((X to_power 2) - (2(#)((r(#)E0)(#)X)))
/\ dom ((r(#)E0) to_power 2) by VALUED_1:def 1
.=dom X /\( Omega /\ Omega) by A19,A22,XBOOLE_1:16
.= dom X /\ Omega;
then A25:
dom((X to_power 2) - 2(#)((r(#)E0)(#)X) + ((r(#)E0) to_power 2))
=dom((X to_power 2) -(2*r)(#)X + (r*r)(#)E0)
by A20,A23,VALUED_1:def 1;
for x be Element of Omega st x in
dom((X to_power 2) - 2(#)((r(#)E0)(#)X) + ((r(#)E0) to_power 2))
holds
((X to_power 2) - 2(#)((r(#)E0)(#)X) + ((r(#)E0) to_power 2)).x
=((X to_power 2) -(2*r)(#)X + (r*r)(#)E0).x
proof
let x be Element of Omega;
assume A26:
x in dom((X to_power 2) - 2(#)((r(#)E0)(#)X) + ((r(#)E0) to_power 2));
then A27: x in dom X & x in Omega by A24,XBOOLE_0:def 4;
A28:
((X to_power 2) - 2(#)((r(#)E0)(#)X) + ((r(#)E0) to_power 2)).x
=((X to_power 2) - 2(#)((r(#)E0)(#)X)).x + ((r(#)E0) to_power 2).x
by A26,VALUED_1:def 1
.=(X to_power 2).x -( 2(#)((r(#)E0)(#)X)).x + ((r(#)E0) to_power 2).x
by A22,A24,A26,VALUED_1:13
.=(X to_power 2).x -2*(((r(#)E0)(#)X).x) + ((r(#)E0) to_power 2).x
by VALUED_1:6
.=(X to_power 2).x -2*(((r(#)E0).x)*(X.x)) + ((r(#)E0) to_power 2).x
by VALUED_1:5
.=(X to_power 2).x -2*((r*(E0.x))*(X.x)) + ((r(#)E0) to_power 2).x
by VALUED_1:6
.=(X to_power 2).x -2*((r*(1))*(X.x)) + ((r(#)E0) to_power 2).x
by FUNCOP_1:7
.=(X to_power 2).x -(2*r)*(X.x)+ (((r(#)E0).x) to_power 2)
by A19,MESFUN6C:def 4
.=(X to_power 2).x -(2*r)*(X.x)+ ((r*(E0.x)) to_power 2)
by VALUED_1:6
.=(X to_power 2).x -(2*r)*(X.x)+ ((r*1) to_power 2) by FUNCOP_1:7
.=(X to_power 2).x -(2*r)*(X.x)+ r^2 by POWER:46
.=(X to_power 2).x -(2*r)*(X.x)+ r*r;
((X to_power 2) -(2*r)(#)X + (r*r)(#)E0).x
=((X to_power 2) -(2*r)(#)X).x + ((r*r)(#)E0).x
by A26,A25,VALUED_1:def 1
.=(X to_power 2).x -((2*r)(#)X).x + ((r*r)(#)E0).x
by A23,A27,VALUED_1:13
.=(X to_power 2).x -(2*r)*(X.x) + ((r*r)(#)E0).x by VALUED_1:6
.=(X to_power 2).x -(2*r)*(X.x) + (r*r)*(E0.x) by VALUED_1:6
.=(X to_power 2).x -(2*r)*(X.x) + (r*r)*(1) by FUNCOP_1:7
.=(X to_power 2).x -(2*r)*(X.x) + r*r;
hence thesis by A28;
end;
hence thesis by A25,PARTFUN1:5;
end;
A29: (abs(Y) to_power 2) =((X- (r(#)E0)) to_power 2) by Th5,A9
.= (X to_power 2) - 2(#)((r(#)E0)(#)X)
+ ((r(#)E0) to_power 2) by Th6
.= (abs(X) to_power 2) -(2*r)(#)X + (r*r)(#)E0 by Th5,A16;
A30: (r*r)(#)E0 is_integrable_on P2M(P) by A10,MESFUNC6:102; then
(abs(Y) to_power 2) is_integrable_on P2M(P) by A15,A29,MESFUNC6:100; then
-infty < Integral(P2M(P),abs(Y) to_power 2)
& Integral(P2M(P),abs(Y) to_power 2) < +infty by MESFUNC6:90;
then Integral(P2M(P),abs(Y) to_power 2) is Element of REAL by XXREAL_0:14;
hence thesis by A30,A15,A29,A14,MESFUNC6:100;
end;
end;
begin :: Chebyshev's inequality
theorem
for Omega,Sigma,P,r for X be Real-Valued-Random-Variable of Sigma st
0 < r & X is nonnegative & X is_integrable_on P &
(abs(X) to_power 2) is_integrable_on P2M(P) holds
P.({t where t is Element of Omega :
r <= |. X.t - expect(X,P) qua Complex .| })
<= variance(X,P)/( r to_power 2)
proof
let Omega,Sigma,P,r;
let X be Real-Valued-Random-Variable of Sigma;
assume
A1: 0 < r & X is nonnegative & X is_integrable_on P &
(abs(X) to_power 2) is_integrable_on P2M(P);
A2:{t where t is Element of Omega : r <= |. X.t - expect(X,P) qua Complex .| }
c=
{t where t is Element of Omega :
(r to_power 2) <= ( |. X.t - expect(X,P) qua Complex.|) to_power 2 }
proof
let s be object;
assume s in {t where t is Element of Omega :
r <= |. X.t - expect(X,P) qua Complex .| };
then A3: ex ss be Element of Omega st
s=ss & r <= |. X.ss - expect(X,P) qua Complex.|;
A4: r^2 = (r to_power 2) & (|. X.s - expect(X,P) qua Complex.|)^2
= ( |. X.s - expect(X,P) qua Complex.|) to_power 2 by POWER:46;
r^2 <= (|. X.s - expect(X,P) qua Complex.|)^2 by A1,A3,SQUARE_1:15;
hence thesis by A3,A4;
end;
{t where t is Element of Omega :
(r to_power 2) <= ( |. X.t - expect(X,P) qua Complex.|) to_power 2 } c=
{t where t is Element of Omega : r <= |. X.t - expect(X,P) qua Complex .|}
proof
let s be object;
assume s in {t where t is Element of Omega :
(r to_power 2) <= ( |. X.t - expect(X,P) qua Complex .|) to_power 2 };
then A5: ex ss be Element of Omega st s=ss &
(r to_power 2) <= ( |. X.ss - expect(X,P) qua Complex .|) to_power 2;
A6: 0<= |. X.s - expect(X,P) qua Complex .| by COMPLEX1:46;
r^2 = (r to_power 2) & (|. X.s - expect(X,P) qua Complex .|)^2
= ( |. X.s - expect(X,P) qua Complex .|) to_power 2 by POWER:46;
then r <= |. X.s - expect(X,P) qua Complex .| by A6,A5,SQUARE_1:47;
hence thesis by A5;
end; then
A7: {t where t is Element of Omega
: r <= |. X.t - expect(X,P) qua Complex .| }
= {t where t is Element of Omega :
(r to_power 2) <= ( |. X.t - expect(X,P) qua Complex .|) to_power 2 }
by A2,XBOOLE_0:def 10;
consider Y be Real-Valued-Random-Variable of Sigma,
E be Real-Valued-Random-Variable of Sigma such that
A8: E=(Omega --> expect(X,P)) & Y= X-E & Y is_integrable_on P &
abs(Y) to_power 2 is_integrable_on P2M(P) &
variance(X,P)=Integral(P2M(P),abs(Y) to_power 2) by Def1,A1;
reconsider Z = abs(Y) to_power 2
as Real-Valued-Random-Variable of Sigma by RANDOM_1:23;
A9: Z is_integrable_on P by A8,RANDOM_1:def 2;
then
A10: P.({t where t is Element of Omega : (r to_power 2) <= Z.t } )
<= expect (Z,P)/(r to_power 2) by A1,POWER:34,RANDOM_1:36;
A11: expect (Z,P)=variance(X,P) by A8,A9,RANDOM_1:def 3;
A12:dom X = Omega by FUNCT_2:def 1;
A13:dom (Omega --> expect(X,P))= Omega by FUNCOP_1:13;
A14:dom (X-(Omega --> expect(X,P)))
=(dom X) /\ (dom (Omega --> expect(X,P))) by VALUED_1:12
.=Omega by A12,A13; then
A15:dom(|.X-(Omega --> expect(X,P)).|) =Omega by VALUED_1:def 11;
then
A16:dom((|.X-(Omega --> expect(X,P)).|) to_power 2) =Omega
by MESFUN6C:def 4;
A17:{t where t is Element of Omega :
(r to_power 2) <= ( |. X.t - expect(X,P) qua Complex .|) to_power 2 } c=
{t where t is Element of Omega : (r to_power 2) <= Z.t }
proof
let s be object;
assume s in {t where t is Element of Omega :
(r to_power 2) <= ( |. X.t - expect(X,P) qua Complex .|) to_power 2 };
then A18:ex ss be Element of Omega st s=ss &
(r to_power 2) <= ( |. X.ss - expect(X,P) qua Complex .|) to_power 2;
then Z.s=((|.X-(Omega --> expect(X,P)).|).s) to_power 2
by A16,A8,MESFUN6C:def 4
.=(|.(X -(Omega --> expect(X,P))).s qua Complex.|) to_power 2
by A15,A18,VALUED_1:def 11
.=(|.X.s -(Omega --> expect(X,P)).s qua Complex.|) to_power 2
by A14,A18,VALUED_1:13
.=(|.X.s - expect(X,P) qua Complex.|) to_power 2 by A18,FUNCOP_1:7;
hence thesis by A18;
end;
{t where t is Element of Omega : (r to_power 2) <= Z.t }
c= {t where t is Element of Omega :
(r to_power 2) <= ( |. X.t - expect(X,P) qua Complex .|) to_power 2 }
proof
let s be object;
assume s in {t where t is Element of Omega : (r to_power 2) <= Z.t };
then A19: ex ss be Element of Omega st s=ss & (r to_power 2) <= Z.ss;
then Z.s=((|.X-(Omega --> expect(X,P)).|).s) to_power 2
by A16,A8,MESFUN6C:def 4
.=(|.(X -(Omega --> expect(X,P))).s qua Complex.|) to_power 2
by A15,A19,VALUED_1:def 11
.=(|.X.s -(Omega --> expect(X,P)).s qua Complex.|) to_power 2
by A14,A19,VALUED_1:13
.=(|.X.s - expect(X,P) qua Complex.|) to_power 2 by A19,FUNCOP_1:7;
hence thesis by A19;
end;
hence thesis by A11,A10,A7,A17,XBOOLE_0:def 10;
end;
begin :: Product Probability
theorem Th8:
for Omega be non empty finite set, f be Function of Omega,REAL,
P be Function of bool Omega, REAL st
(for x be set st x c= Omega holds 0 <= P.x & P.x <= 1) &
P.Omega = 1 & for z be finite Subset of Omega
holds P.z = setopfunc(z,Omega,REAL,f,addreal)
holds P is Probability of Trivial-SigmaField Omega
proof
let Omega be non empty finite set,
f be Function of Omega,REAL,
P be Function of bool Omega, REAL;
assume that
A1: for x be set st x c= Omega holds 0 <= P.x & P.x <= 1 and
A2: P.Omega = 1 and
A3: for z be finite Subset of Omega
holds P.z = setopfunc(z,Omega,REAL,f,addreal);
A4: for A,B being Event of Trivial-SigmaField (Omega)
st A misses B holds P.(A \/ B) = P.A + (P.B qua Real)
proof
let A,B be Event of Trivial-SigmaField (Omega);
assume
A5: A misses B;
reconsider A0 =A,B0=B as finite Subset of Omega;
A6: Omega = dom f by FUNCT_2:def 1;
thus P.(A \/ B) = setopfunc((A0 \/ B0),Omega,REAL,f,addreal) by A3
.= (addreal).(setopfunc(A0,Omega,REAL,f,addreal),
setopfunc(B0,Omega,REAL,f,addreal)) by A5,A6,BHSP_5:14
.= (addreal).(setopfunc(A0,Omega,REAL,f,addreal),(P.B)) by A3
.= (addreal).((P.A),(P.B)) by A3
.= (P.A) + ((P.B) qua Real) by BINOP_2:def 9;
end;
A7: for A being Event of Trivial-SigmaField (Omega) holds 0 <= P.A by A1;
for ASeq being SetSequence of Trivial-SigmaField (Omega) st ASeq is
non-ascending holds P * ASeq is convergent & lim (P * ASeq) = P.(
Intersection ASeq)
proof
let ASeq being SetSequence of Trivial-SigmaField (Omega);
assume ASeq is non-ascending;
then consider N be Nat such that
A8: for m be Nat st N<=m holds Intersection ASeq = ASeq.m
by RANDOM_1:15;
now
let m be Nat;
assume
A9: N <= m;
m in NAT by ORDINAL1:def 12;
then m in dom ASeq by FUNCT_2:def 1;
hence (P * ASeq).m = P.(ASeq.m) by FUNCT_1:13
.= P.(Intersection ASeq) by A8,A9;
end;
hence thesis by PROB_1:1;
end;
hence thesis by A7,A4,A2,PROB_1:def 8;
end;
Lm1:
for Omega1, Omega2 be non empty finite set, P1 be Probability of
Trivial-SigmaField (Omega1), P2 be Probability of
Trivial-SigmaField (Omega2)
ex Q be Function of [:Omega1,Omega2:],REAL
st for x,y be set st x in Omega1 & y in Omega2
holds Q.(x,y) = (P1.{x})*(P2.{y})
proof
let Omega1, Omega2 be non empty finite set, P1 be Probability of
Trivial-SigmaField (Omega1), P2 be Probability of
Trivial-SigmaField (Omega2);
deffunc Q0(object,object)= (P1.{$1})*(P2.{$2});
consider f being Function such that
A1: dom f =
[:Omega1, Omega2:] & for x,y be object st x in Omega1 & y in Omega2
holds f.(x,y) = Q0(x,y) from FUNCT_3:sch 2;
for z be object st z in [:Omega1,Omega2:] holds f.z in REAL
proof
let z be object;
assume z in [:Omega1,Omega2:]; then
consider x,y be object such that
A2: x in Omega1 & y in Omega2 & z =[x,y] by ZFMISC_1:def 2;
f.z =f.(x,y) by A2
.=Q0(x,y) by A1,A2;
hence f.z in REAL by XREAL_0:def 1;
end;
then
reconsider f as Function of [:Omega1,Omega2:],REAL by A1,FUNCT_2:3;
take f;
thus thesis by A1;
end;
Lm2:
for Omega1, Omega2 be non empty finite set, P1 be Probability of
Trivial-SigmaField (Omega1), P2 be Probability of
Trivial-SigmaField (Omega2),
Q1,Q2 be Function of [:Omega1,Omega2:],REAL
st (for x,y be set st x in Omega1 & y in Omega2
holds Q1.(x,y) = (P1.{x})*(P2.{y}) ) &
(for x,y be set st x in Omega1 & y in Omega2
holds Q2.(x,y) = (P1.{x})*(P2.{y}) )
holds Q1=Q2
proof
let Omega1, Omega2 be non empty finite set, P1 be Probability of
Trivial-SigmaField (Omega1), P2 be Probability of
Trivial-SigmaField (Omega2),
Q1,Q2 be Function of [:Omega1,Omega2:],REAL;
assume A1: (for x,y be set st x in Omega1 & y in Omega2
holds Q1.(x,y) = (P1.{x})*(P2.{y}) ) &
(for x,y be set st x in Omega1 & y in Omega2
holds Q2.(x,y) = (P1.{x})*(P2.{y}) );
A2: dom Q1 = [:Omega1,Omega2:] &
dom Q2 = [:Omega1,Omega2:] by FUNCT_2:def 1;
now let z be object;
assume z in dom Q1;
then consider x,y be object such that
A3: x in Omega1 & y in Omega2 & z = [x,y] by ZFMISC_1:def 2;
thus Q1.z= Q1.(x,y) by A3
.= (P1.{x})*(P2.{y}) by A3,A1
.= Q2.(x,y) by A3,A1
.=Q2.z by A3;
end;
hence thesis by A2,FUNCT_1:2;
end;
Lm3:
for Omega1, Omega2 be non empty finite set, P1 be Probability of
Trivial-SigmaField (Omega1), P2 be Probability of
Trivial-SigmaField (Omega2),
Q be Function of [:Omega1,Omega2:],REAL
ex P be Function of (bool [:Omega1,Omega2:]),REAL st
for z be finite Subset of [:Omega1,Omega2:]
holds P.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal)
proof
let Omega1, Omega2 be non empty finite set, P1 be Probability of
Trivial-SigmaField (Omega1), P2 be Probability of
Trivial-SigmaField (Omega2),
Q be Function of [:Omega1,Omega2:],REAL;
defpred PF[object,object] means
ex z be finite Subset of [:Omega1,Omega2:]
st $1=z &
$2 = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal);
A1: for x be object st x in bool [:Omega1,Omega2:]
holds ex y be object st y in REAL & PF[x,y]
proof
let x be object;
assume x in bool [:Omega1,Omega2:];
then reconsider z=x as finite Subset of [:Omega1,Omega2:];
setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal) in REAL;
hence thesis;
end;
consider P be Function of (bool [:Omega1,Omega2:]),REAL such that
A2:for x be object st x in (bool [:Omega1,Omega2:]) holds PF[x,P.x]
from FUNCT_2:sch 1(A1);
take P;
thus for z be finite Subset of [:Omega1,Omega2:]
holds P.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal)
proof
let z be finite Subset of [:Omega1,Omega2:];
ex z1 be finite Subset of [:Omega1,Omega2:] st z=z1 &
P.z= setopfunc(z1,[:Omega1,Omega2:],REAL,Q,addreal) by A2;
hence P.z= setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal);
end;
end;
Lm4:
for Omega1, Omega2 be non empty finite set, P1 be Probability of
Trivial-SigmaField (Omega1), P2 be Probability of
Trivial-SigmaField (Omega2),
Q be Function of [:Omega1,Omega2:],REAL
for P1,P2 be Function of (bool [:Omega1,Omega2:]),REAL st
(for z be finite Subset of [:Omega1,Omega2:]
holds P1.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal)) &
(for z be finite Subset of [:Omega1,Omega2:]
holds P2.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal))
holds P1=P2
proof
let Omega1, Omega2 be non empty finite set, P1 be Probability of
Trivial-SigmaField (Omega1), P2 be Probability of
Trivial-SigmaField (Omega2),
Q be Function of [:Omega1,Omega2:],REAL;
let P1,P2 be Function of (bool [:Omega1,Omega2:]),REAL;
assume A1:
for z be finite Subset of [:Omega1,Omega2:]
holds P1.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal);
assume A2:
for z be finite Subset of [:Omega1,Omega2:]
holds P2.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal);
now let x be object;
assume x in bool [:Omega1,Omega2:];
then reconsider z=x as finite Subset of [:Omega1,Omega2:];
thus P1.x = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal) by A1
.= P2.x by A2;
end;
hence P1=P2 by FUNCT_2:12;
end;
Lm5:
for DK, DX be non empty set, F be Function of DX, DK,
p,q be FinSequence of DX,
fp,fq be FinSequence of DK st fp=F*p & fq=F*q holds F*(p^q) = fp^fq
proof
let DK, DX be non empty set,
F be Function of DX, DK,
p,q be FinSequence of DX,
fp,fq be FinSequence of DK;
assume A1:fp=F*p & fq=F*q;
then A2: dom fp = dom p & dom fq = dom q by FINSEQ_3:120;
A3: len fp =len p & len fq =len q by A1,FINSEQ_3:120; then
A4: dom (fp^fq)=Seg (len p + len q) by FINSEQ_1:def 7;
A5: dom (F*(p^q))= dom (p^q) by FINSEQ_3:120
.=Seg (len p + len q) by FINSEQ_1:def 7;
for x be object st x in dom (F*(p^q)) holds (fp^fq).x=(F*(p^q)).x
proof
let x be object;
assume A6: x in dom (F*(p^q));
then reconsider n=x as Element of NAT;
A7: 1<= n & n <= len p + len q by A6,A5,FINSEQ_1:1;
A8: (F*(p^q)).n = F.((p^q).n) by A6,FINSEQ_3:120;
per cases;
suppose n <= len p;
then n in Seg (len p) by A7; then
A9: n in dom p by FINSEQ_1:def 3;
hence (F*(p^q)).x =F.((p.n)) by A8,FINSEQ_1:def 7
.=fp.n by A1,A9,A2,FINSEQ_3:120
.= (fp^fq).x by A9,A2,FINSEQ_1:def 7;
end;
suppose A10: not n <= len p; then
len p < n & n <=len (p^q) by A7,FINSEQ_1:22; then
A11: (p^q).n=q.(n-len p) by FINSEQ_1:24;
A12: n-len p <= len p+ len q - len p by A7,XREAL_1:9;
A13: len p - len p < n - len p by A10,XREAL_1:9;
A14: n-len p is Element of NAT by A13,INT_1:3; then
1<=n-len p by A13,NAT_1:14; then
n-len p in Seg len q by A12,A14;
then
A15: n-len p in dom q by FINSEQ_1:def 3;
A16:len fp < n & n <= len (fp^fq) by A3,A10,A7,FINSEQ_1:22;
thus (F*(p^q)).x =fq.(n-len p) by A1,A15,A2,A11,A8,FINSEQ_3:120
.= (fp^fq).x by A16,A3,FINSEQ_1:24;
end;
end;
hence thesis by A4,A5,FUNCT_1:2;
end;
theorem Th9:
for DX be non empty set, F be Function of DX,REAL,
Y be finite Subset of DX holds
ex p being FinSequence of DX st p is one-to-one &
rng p = Y & setopfunc(Y,DX,REAL,F,addreal)=Sum(Func_Seq(F,p))
proof
let DX be non empty set,
F be Function of DX,REAL,
Y be finite Subset of DX;
consider p being FinSequence of DX such that
A1: p is one-to-one & rng p = Y & setopfunc(Y,DX,REAL,F,addreal)
= (addreal) "**" Func_Seq(F,p) by BHSP_5:def 5;
Sum(Func_Seq(F,p)) = (addreal) "**" Func_Seq(F,p);
hence thesis by A1;
end;
theorem Th10:
for DX be non empty set, F be Function of DX,REAL, Y be finite Subset of DX,
p being FinSequence of DX
st p is one-to-one & rng p = Y holds
setopfunc(Y,DX,REAL,F,addreal)=Sum(Func_Seq(F,p)) by BHSP_5:def 5;
Lm6:
for p be Function st dom p = Seg 1 holds p = <*p.1*>
proof
let p be Function;
assume A1:dom p = Seg 1; then
A3: rng p = {p.1} by FINSEQ_1:2,FUNCT_1:4;
p is FinSequence-like by A1;
hence thesis by A3,A1,FINSEQ_1:38;
end;
theorem Th11:
for DX1,DX2 be non empty set, F1 be Function of DX1,REAL,
F2 be Function of DX2,REAL,
G be Function of [:DX1,DX2:], REAL,
Y1 be non empty finite Subset of DX1 holds
for p1 being FinSequence of DX1 st
p1 is one-to-one & rng p1 = Y1 holds
for p2 being FinSequence of DX2,
p3 being FinSequence of [:DX1,DX2:],
Y2 be non empty finite Subset of DX2,
Y3 be finite Subset of [:DX1,DX2:] st
p2 is one-to-one & rng p2 = Y2 &
p3 is one-to-one & rng p3 = Y3 & Y3= [:Y1,Y2:] &
for x,y be set st x in Y1 & y in Y2
holds G.(x,y)= (F1.x)*(F2.y) holds
Sum(Func_Seq(G,p3))= Sum(Func_Seq(F1,p1))*Sum(Func_Seq(F2,p2))
proof
let DX1,DX2 be non empty set,
F1 be Function of DX1,REAL,
F2 be Function of DX2,REAL,
G be Function of [:DX1,DX2:],REAL,
Y1 be non empty finite Subset of DX1;
let p1 be FinSequence of DX1;
assume
A1: p1 is one-to-one & rng p1 = Y1;
defpred F[Nat] means for p2 being FinSequence of DX2,
p3 being FinSequence of [:DX1,DX2:],
Y2 be non empty finite Subset of DX2,
Y3 be finite Subset of [:DX1,DX2:] st
len p2=$1 & p2 is one-to-one & rng p2 = Y2 &
p3 is one-to-one & rng p3 = Y3 & Y3= [:Y1,Y2:] &
for x,y be set st x in Y1 & y in Y2 holds G.(x,y)= (F1.x)*(F2.y)
holds
Sum(Func_Seq(G,p3))= Sum(Func_Seq(F1,p1))*Sum(Func_Seq(F2,p2));
consider erp1 be object such that
A2: erp1 in (rng p1) by A1,XBOOLE_0:def 1;
A3:ex x be object st x in dom p1 & erp1 = p1.x by A2,FUNCT_1:def 3;
A4: F[0]
proof
let p2 be FinSequence of DX2,
p3 be FinSequence of [:DX1,DX2:],
Y2 be non empty finite Subset of DX2,
Y3 be finite Subset of [:DX1,DX2:];
assume
A5: len p2=0 & p2 is one-to-one & rng p2 = Y2 &
p3 is one-to-one & rng p3 = Y3 &
Y3= [:Y1,Y2:] & for x,y be set st x in Y1 & y in Y2
holds G.(x,y)= (F1.x)*(F2.y);
then p2 = {};
hence Sum(Func_Seq(G,p3))
= Sum(Func_Seq(F1,p1))*Sum(Func_Seq(F2,p2)) by A5;
end;
A6: F[1]
proof
let p2 be FinSequence of DX2,
p3 be FinSequence of [:DX1,DX2:],
Y2 be non empty finite Subset of DX2,
Y3 be finite Subset of [:DX1,DX2:];
assume
A7: len p2=1 & p2 is one-to-one & rng p2 = Y2 &
p3 is one-to-one & rng p3 = Y3 &
Y3= [:Y1,Y2:] &
for x,y be set st x in Y1 & y in Y2
holds G.(x,y)= (F1.x)*(F2.y);
then A8:p2=<*(p2.1)*> by FINSEQ_1:40;
then A9:Y2={p2.1} by A7,FINSEQ_1:38;
set w = p2.1;
set z = (F2*p2).1;
dom F2 = DX2 by FUNCT_2:def 1;
then rng p2 c= dom F2;
then dom (F2*p2) =dom p2 by RELAT_1:27;
then A10:dom (F2*p2) =Seg 1 by A8,FINSEQ_1:38;
then Func_Seq(F2,p2)=<*z*> by Lm6; then
A11: Sum(Func_Seq(F2,p2)) = z by RVSUM_1:73;
A12: Y3= [:Y1,{w}:] by A7,A8,FINSEQ_1:38;
A13:len p1 =card(Y1) by A1,FINSEQ_4:62;
A14: len p3 = card (rng p3) by A7,FINSEQ_4:62
.=card(Y1) by A12,A7,CARD_1:69;
A15: dom p1=Seg (card(Y1)) by A13,FINSEQ_1:def 3
.= dom p3 by A14,FINSEQ_1:def 3;
deffunc Q33F(Nat) = [p1.$1,w ];
consider q3 be FinSequence such that
A16: len q3 = len p3 and
A17: for k be Nat st k in dom q3 holds q3.k=Q33F(k) from FINSEQ_1:sch 2;
A18: dom q3 = Seg(len p3) by A16,FINSEQ_1:def 3;
A19: dom p3 = Seg len p3 by FINSEQ_1:def 3;
now
let k be Nat;
assume
A20: k in dom q3; then
A21: p1.k in Y1 by A1,A18,A19,A15,FUNCT_1:3;
p2.1 in Y2 by A9,TARSKI:def 1;
then [ p1.k,w ] in [:Y1,Y2:] by A21,ZFMISC_1:87;
hence q3.k in [:Y1,Y2:] by A20,A17;
end;
then
q3 is FinSequence of [:Y1,Y2:] by FINSEQ_2:12; then
A22: rng q3 c= [:Y1,Y2:] by FINSEQ_1:def 4;
[:Y1,Y2:] c= [:DX1,DX2:] by ZFMISC_1:96;
then
rng q3 c= [:DX1,DX2:] by A22;
then
reconsider q3 as FinSequence of [:DX1,DX2:] by FINSEQ_1:def 4;
now let x1,x2 be object;
assume A23:x1 in dom q3 & x2 in dom q3 & q3.x1=q3.x2;
then
A24: x1 in dom p1 & x2 in dom p1 by A16,A19,A15,FINSEQ_1:def 3;
reconsider n1=x1,n2=x2 as Element of NAT by A23;
[p1.n1,w] = q3.n1 by A17,A23
.=[p1.n2,w] by A17,A23; then
p1.n1=p1.n2 by XTUPLE_0:1;
hence x1=x2 by A1,A24,FUNCT_1:def 4;
end;
then
A25:q3 is one-to-one by FUNCT_1:def 4;
A26: rng q3 = [:Y1,Y2:]
proof
now let z be object;
assume z in [:Y1,Y2:];
then consider y1,y2 be object such that
A27: y1 in Y1 & y2 in Y2 & z=[y1,y2] by ZFMISC_1:def 2;
consider n1 be object such that
A28: n1 in dom p1 & y1=p1.n1 by A1,A27,FUNCT_1:def 3;
reconsider n1 as Element of NAT by A28;
A29:n1 in dom q3 by A28,A16,A19,A15,FINSEQ_1:def 3;
y2=w by A9,A27,TARSKI:def 1;
then q3.n1=z by A27,A28,A17,A29;
hence z in rng q3 by A29,FUNCT_1:3;
end; then
[:Y1,Y2:] c= rng q3;
hence thesis by A22,XBOOLE_0:def 10;
end;
then consider P being Permutation of dom p3 such that
A30:
q3 = p3*P & dom P = dom p3 & rng P = dom p3 by A25,A7,BHSP_5:1;
A31: Func_Seq(G,q3) = Func_Seq(G,p3)*P by A30,RELAT_1:36;
dom G = [:DX1,DX2:] by FUNCT_2:def 1;then
rng p3 c= dom G; then
dom Func_Seq(G,p3) = dom p3 by RELAT_1:27;
then
A32: Sum(Func_Seq(G,q3)) = Sum(Func_Seq(G,p3)) by A31,FINSOP_1:7;
A33: dom G =[:DX1,DX2:] by FUNCT_2:def 1;
dom F1=DX1 by FUNCT_2:def 1;
then
A34: dom(F1*p1) = dom p1 by A1,RELAT_1:27
.=Seg (len p1) by FINSEQ_1:def 3;
A35: dom (G*q3) = dom q3 by A33,A26,RELAT_1:27
.=Seg (len p1) by A13,A14,A16,FINSEQ_1:def 3;
then
A36: dom (G*q3) = dom (z (#)(F1*p1) ) by A34,VALUED_1:def 5;
now let x be object;
assume A37: x in dom (G*q3);
then reconsider nx=x as Element of NAT;
dom (G*q3) = dom q3 by A33,A26,RELAT_1:27
.=Seg (len q3) by FINSEQ_1:def 3; then
A38: nx in dom q3 by A37,FINSEQ_1:def 3;
1 <= nx & nx <= len p1 by A37,A35,FINSEQ_1:1; then
A39:p1/.nx=p1.nx by FINSEQ_4:15;
A40:
q3.nx = [ p1.nx, w ] by A17,A38;
A41:nx in dom p1 by A37,A35,FINSEQ_1:def 3; then
A42: q3.nx = [ p1/.nx, w ] by A40,PARTFUN1:def 6;
p1.nx in Y1 by A41,A1,FUNCT_1:3; then
A43:
p1/.nx in Y1 & w in Y2 by A41,A9,PARTFUN1:def 6,TARSKI:def 1;
1 in dom(F2*p2) by A10; then
A44: z =F2.w by FUNCT_1:12;
thus (G*q3).x =G.(p1/.nx,w) by A42,A37,FUNCT_1:12
.=F1.(p1/.nx) * z by A44,A7,A43
.= ((F1*p1).nx) *z by A39,A35,A34,A37,FUNCT_1:12
.= (z (#)(F1*p1)).x by VALUED_1:6;
end; then
Func_Seq(G,q3) = z * (Func_Seq(F1,p1)) by A36,FUNCT_1:2;
hence thesis by A11,A32,RVSUM_1:87;
end;
A45: for n be Nat st F[n] holds F[n+1]
proof
let n be Nat;
assume A46: F[n];
now per cases;
case n=0;
hence F[n+1] by A6;
end;
case A47:n>0;
now let p2 be FinSequence of DX2,
p3 be FinSequence of [:DX1,DX2:],
Y2 be non empty finite Subset of DX2,
Y3 be finite Subset of [:DX1,DX2:];
assume
A48: len p2=n+1 & p2 is one-to-one & rng p2 = Y2 &
p3 is one-to-one & rng p3 = Y3 &
Y3= [:Y1,Y2:] &
for x,y be set st x in Y1 & y in Y2
holds G.(x,y)= (F1.x)*(F2.y);
set lb = len p1;
set la = len p2;
deffunc FG1(Nat)
= [ p1.(($1-'1) mod lb + 1), p2.(($1-'1) div lb + 1) ];
consider FG be FinSequence such that
A49: len FG = la*lb and
A50: for k be Nat st k in dom FG holds FG.k=FG1(k)
from FINSEQ_1:sch 2;
A51: dom FG = Seg(la*lb) by A49,FINSEQ_1:def 3;
A52: dom p1= Seg lb by FINSEQ_1:def 3;
A53: now
reconsider lap=la,lbp=lb as Nat;
let k be Nat;
set i=(k-'1) div lb + 1;
set j=(k-'1) mod lb + 1;
assume k in dom FG; then
A54: k in Seg (la*lb) by A49,FINSEQ_1:def 3; then
A55: k <= la*lb by FINSEQ_1:1;
then (k -' 1) <= (la*lb -' 1) by NAT_D:42;
then
A56: (k -' 1) div lb <= (la*lb -' 1) div lb by NAT_2:24;
1 <= k by A54,FINSEQ_1:1;
then
A57: lbp divides (lap*lbp) & 1 <= la*lb by A55,NAT_D:def 3
,XXREAL_0:2;
A58: lb <> 0 by A54;
then lb >= (0 qua Nat)+1 by NAT_1:13;
then ((lap*lbp) -' 1) div lbp = ((lap*lbp) div lbp) - 1 by A57,
NAT_2:15;
then
A59: (k -' 1) div lb + 1 <= la*lb div lb by A56,XREAL_1:19;
reconsider la,lb as Nat;
i >= (0 qua Nat)+1 & i <= la by A58,A59,NAT_D:18,XREAL_1:6;
then i in Seg la;
hence i in dom p2 by FINSEQ_1:def 3;
(k -' 1) mod lb < lb by A58,NAT_D:1;
then j >= (0 qua Nat)+1 & j <= lb by NAT_1:13;
then j in Seg lb;
hence j in dom p1 by FINSEQ_1:def 3;
end;
now
let k be Nat;
set i=(k-'1) div lb + 1;
set j=(k-'1) mod lb + 1;
assume
A60: k in dom FG;
then
A61: p2.i in rng p2 by A53,FUNCT_1:3;
p1.j in rng p1 by A53,A60,FUNCT_1:3;
then [ p1.j,p2.i ] in [:DX1,DX2:] by A61,ZFMISC_1:87;
hence FG.k in [:DX1,DX2:] by A50,A60;
end;
then reconsider q3=FG as FinSequence of [:DX1,DX2:] by FINSEQ_2:12;
A62:len p1 =card(Y1) by A1,FINSEQ_4:62;
now let x1,x2 be object;
assume A63:x1 in dom q3 & x2 in dom q3 & q3.x1=q3.x2;
then
A64:x1 in Seg (len q3) & x2 in Seg (len q3) by FINSEQ_1:def 3;
reconsider n1=x1,n2=x2 as Element of NAT by A63;
A65: q3.n1=[ p1.((n1-'1) mod lb + 1), p2.((n1-'1) div lb + 1) ]
by A50,A63;
A66: q3.n2=[ p1.((n2-'1) mod lb + 1), p2.((n2-'1) div lb + 1) ]
by A50,A63;
then A67:p1.((n1-'1) mod lb + 1) = p1.((n2-'1) mod lb + 1)
by A63,A65,XTUPLE_0:1;
(n1-'1) mod lb + 1 in dom p1 &
(n2-'1) mod lb + 1 in dom p1 by A63,A53; then
A68: (n1-'1) mod lb + 1 = (n2-'1) mod lb + 1
by A1,A67,FUNCT_1:def 4;
A69:p2.((n1-'1) div lb + 1) = p2.((n2-'1) div lb + 1)
by A63,A65,A66,XTUPLE_0:1;
(n1-'1) div lb + 1 in dom p2 &
(n2-'1) div lb + 1 in dom p2 by A63,A53; then
A70: (n1-'1) div lb + 1 = (n2-'1) div lb + 1
by A48,A69,FUNCT_1:def 4;
n1=n2
proof
A71: 1<=n1 & n1 <=len q3 by A64,FINSEQ_1:1;
A72: 1<=n2 & n2 <=len q3 by A64,FINSEQ_1:1;
0 < lb by A52,A3;
then A73:
(n1-'1) = lb*((n1-'1) div lb) + ((n1-'1) mod lb)&
(n2-'1) = lb*((n1-'1) div lb) + ((n1-'1) mod lb)
by A68,A70,NAT_D:2;
A74: n1-'1 +1= n1 +1 -'1 by A71,NAT_D:38
.= n1 by NAT_D:34;
n2-'1 +1= n2 +1 -'1 by A72,NAT_D:38
.= n2 by NAT_D:34;
hence thesis by A73,A74;
end;
hence x1=x2;
end;
then
A75:q3 is one-to-one by FUNCT_1:def 4;
A76: rng q3 = [:Y1,Y2:]
proof
now let z be object;
assume z in [:Y1,Y2:]; then
consider y1,y2 be object such that
A77: y1 in Y1 & y2 in Y2 & z=[y1,y2] by ZFMISC_1:def 2;
consider n1 be object such that
A78: n1 in dom p1 & y1=p1.n1 by A1,A77,FUNCT_1:def 3;
A79: n1 in Seg (len p1) by A78,FINSEQ_1:def 3;
reconsider n1 as Element of NAT by A78;
consider n2 be object such that
A80: n2 in dom p2 & y2=p2.n2 by A48,A77,FUNCT_1:def 3;
A81: n2 in Seg (len p2) by A80,FINSEQ_1:def 3;
reconsider n2 as Element of NAT by A80;
A82: 1<=n1 & n1 <=len p1 by A79,FINSEQ_1:1;
A83: 1<=n2 & n2 <=len p2 by A81,FINSEQ_1:1;
reconsider n11 = n1-1 as Element of NAT by A82,INT_1:5;
reconsider n21 = n2-1 as Element of NAT by A83,INT_1:5;
set k1=n11 + lb*n21;
A84: n11 <= len p1 -1 by A82,XREAL_1:9;
len p1 -1 < len p1 by XREAL_1:44;
then
A85: n11 < len p1 by A84,XXREAL_0:2;
A86: k1 div lb = n11 div lb + n21 by A62,NAT_D:61
.= (0 qua Nat) + n21 by A85,NAT_D:27
.=n21;
A87: k1 mod lb = n11 mod lb by NAT_D:61
.=n11 by A85,NAT_D:24;
set k=k1+1;
A88:1 <=k by NAT_1:14;
A89:k-'1 =k-1 by NAT_1:14,XREAL_1:233
.=k1;
then A90: n1=(k-'1) mod lb + 1 by A87;
A91: n2=(k-'1) div lb + 1 by A89,A86;
A92: n11+1 + lb*n21 <= len p1 + lb*n21 by A82,XREAL_1:6;
n21 <= len p2 -1 by A83,XREAL_1:9;
then lb*n21 <= lb*(len p2 -1) by XREAL_1:64;
then
len p1 + lb*n21 <= len p1 +lb*(len p2 -1) by XREAL_1:6;
then
k<= lb*la by A92,XXREAL_0:2;
then k in Seg (len FG) by A49,A88; then
A93:k in dom FG by FINSEQ_1:def 3;
then q3.k =z by A77,A78,A80,A50,A90,A91;
hence z in rng q3 by A93,FUNCT_1:3;
end;
then
A94: [:Y1,Y2:] c= rng q3;
now let z be object;
assume z in rng q3;
then consider n1 be object such that
A95: n1 in dom q3 & z=q3.n1 by FUNCT_1:def 3;
reconsider n1 as Element of NAT by A95;
A96:z= [ p1.((n1-'1) mod lb + 1), p2.((n1-'1) div lb + 1) ]
by A95,A50;
A97: p1.((n1-'1) mod lb + 1) in Y1 by A1,A95,A53,FUNCT_1:3;
(n1-'1) div lb + 1 in dom p2 by A95,A53;
then
p2.((n1-'1) div lb + 1) in Y2 by A48,FUNCT_1:3;
hence z in [:Y1,Y2:] by A96,A97,ZFMISC_1:def 2;
end; then
rng q3 c= [:Y1,Y2:];
hence thesis by A94,XBOOLE_0:def 10;
end;
set q30=q3|(lb*n);
lb*n <=lb*la by A48,NAT_1:11,XREAL_1:64;
then A98: len q30=lb*n by A49,FINSEQ_1:17;
set q31=q3 /^ (lb*n);
A99: q3=q30^q31 by RFINSEQ:8;
set p20=p2|n;
A100:len p20=n by A48,FINSEQ_3:53;
then
A101:dom p20 is non empty by A47,FINSEQ_1:def 3;
A102: p20 is one-to-one by A48,FUNCT_1:52;
reconsider Y20 = rng p20
as non empty finite Subset of DX2 by A101,RELAT_1:42;
A103: q30 is one-to-one by A75,FUNCT_1:52;
A104: rng q30 = [:Y1,Y20:]
proof
now let z be object;
assume z in [:Y1,Y20:];
then
consider y1,y2 be object such that
A105: y1 in Y1 & y2 in Y20 & z=[y1,y2] by ZFMISC_1:def 2;
consider n1 be object such that
A106: n1 in dom p1 & y1=p1.n1 by A1,A105,FUNCT_1:def 3;
A107:n1 in Seg len p1 by A106,FINSEQ_1:def 3;
reconsider n1 as Element of NAT by A106;
consider n2 be object such that
A108: n2 in dom p20 & y2=p20.n2 by A105,FUNCT_1:def 3;
A109:n2 in Seg (len p20) by A108,FINSEQ_1:def 3;
reconsider n2 as Element of NAT by A108;
A110: y2=p2.n2 by A108,FUNCT_1:47;
A111: 1<=n1 & n1 <=len p1 by A107,FINSEQ_1:1;
A112: 1<=n2 & n2 <=len p20 by A109,FINSEQ_1:1;
reconsider n11 = n1-1 as Element of NAT by A111,INT_1:5;
reconsider n21 = n2-1 as Element of NAT by A112,INT_1:5;
set k1=n11 + lb*n21;
A113: n11 <= len p1 -1 by A111,XREAL_1:9;
len p1 -1 < len p1 by XREAL_1:44;
then
A114: n11 < len p1 by A113,XXREAL_0:2;
A115: k1 div lb = n11 div lb + n21 by A62,NAT_D:61
.= (0 qua Nat) + n21 by A114,NAT_D:27
.=n21;
A116: k1 mod lb = n11 mod lb by NAT_D:61
.=n11 by A114,NAT_D:24;
set k=k1+1;
A117:1 <=k by NAT_1:14;
A118:k-'1 =k-1 by NAT_1:14,XREAL_1:233
.=k1;
then A119: n1=(k-'1) mod lb + 1 by A116;
A120: n2=(k-'1) div lb + 1 by A118,A115;
A121:
n11+1 + lb*n21 <= len p1 + lb*n21 by A111,XREAL_1:6;
n21 <= len p20 -1 by A112,XREAL_1:9;
then lb*n21 <= lb*(len p20 -1) by XREAL_1:64;
then
len p1 + lb*n21 <= len p1 +lb*(len p20 -1) by XREAL_1:6;
then
k<= lb*n by A121,A100,XXREAL_0:2;
then k in Seg len q30 by A117,A98;
then
A122:k in dom q30 by FINSEQ_1:def 3;
then
A123: k in dom q3 by RELAT_1:57;
q30.k =q3.k by A122,FUNCT_1:47
.=z by A105,A106,A110,A50,A123,A119,A120;
hence z in rng q30 by A122,FUNCT_1:3;
end;
then
A124: [:Y1,Y20:] c= rng q30;
now let z be object;
assume z in rng q30; then
consider n1 be object such that
A125: n1 in dom q30 & z=q30.n1 by FUNCT_1:def 3;
A126:n1 in Seg (len q30) by A125,FINSEQ_1:def 3;
reconsider n1 as Element of NAT by A125;
A127: n1 in dom q3 by A125,RELAT_1:57;
z=q3.n1 by A125,FUNCT_1:47; then
A128:z= [ p1.((n1-'1) mod lb + 1), p2.((n1-'1) div lb + 1) ]
by A50,A127;
A129: p1.((n1-'1) mod lb + 1) in Y1 by A1,A127,A53,FUNCT_1:3;
A130: 1<=n1 & n1 <=lb*n by A126,A98,FINSEQ_1:1;
A131: lb divides lb*n by INT_1:def 3;
A132: 1 <=lb by A62,NAT_1:14;
1 <=lb*n by A62,A47,NAT_1:14; then
A133: ( (lb*n)-' 1) div lb =(lb*n) div lb -1
by A131,A132,NAT_2:15
.=n-1 by A62;
n1-'1 <= (lb*n)-' 1 by A130,NAT_D:42; then
(n1-'1) div lb <= ( (lb*n)-' 1 ) div lb by NAT_2:24; then
A134: (n1-'1) div lb + 1 <= ( n-1) + 1 by A133,XREAL_1:6;
(n1-'1) div lb + 1 in dom p2 by A127,A53; then
(n1-'1) div lb + 1 in Seg len p2 by FINSEQ_1:def 3; then
1<=(n1-'1) div lb + 1 & (n1-'1) div lb + 1 <=n
by A134,FINSEQ_1:1; then
A135:(n1-'1) div lb + 1 in Seg n;
(n1-'1) div lb + 1 in dom p2 by A127,A53; then
A136:(n1-'1) div lb + 1 in dom p20 by A135,RELAT_1:57; then
p20.((n1-'1) div lb + 1) in Y20 by FUNCT_1:3; then
p2.((n1-'1) div lb + 1) in Y20 by A136,FUNCT_1:47;
hence z in [:Y1,Y20:] by A128,A129,ZFMISC_1:def 2;
end; then
rng q30 c= [:Y1,Y20:];
hence thesis by A124,XBOOLE_0:def 10;
end;
now let x,y be set;
assume A137:x in Y1 & y in Y20;
Y20 c= rng p2 by RELAT_1:70;
hence G.(x,y)= (F1.x)*(F2.y) by A48,A137;
end;
then A138: Sum(Func_Seq(G,q30))
= Sum(Func_Seq(F1,p1))*Sum(Func_Seq(F2,p20)) by A46,A102,A103,A104,A100
;
dom F1=DX1 by FUNCT_2:def 1; then
A139: dom(F1*p1) = dom p1 by A1,RELAT_1:27
.=Seg (len p1) by FINSEQ_1:def 3;
A140: dom G = [:DX1,DX2:] by FUNCT_2:def 1;
len q3 = n*lb + lb by A48,A49; then
A141: n*lb <= len q3 by NAT_1:11; then
A142: len q31 = (len q3) - (lb*n) by RFINSEQ:def 1
.= lb by A48,A49;
A143: [:Y1,Y2:] c= [:DX1,DX2:] & rng q31 c= rng q3
by A48,FINSEQ_5:33; then
A144: dom (G*q31) = dom q31 by A140,RELAT_1:27
.=Seg (len p1) by A142,FINSEQ_1:def 3; then
A145: dom (G*q31) = dom (((Func_Seq(F2,p2))/.(n+1)) (#)(F1*p1))
by A139,VALUED_1:def 5;
now let x be object;
assume A146: x in dom (G*q31);
then reconsider nx=x as Element of NAT;
A147:dom (G*q31) = dom q31 by A140,A143,RELAT_1:27
.=Seg (len q31) by FINSEQ_1:def 3;
A148: 1 <= nx <= len p1 by A146,A144,FINSEQ_1:1; then
A149:p1/.nx=p1.nx by FINSEQ_4:15;
A150:1 <= n+1 <= len p2 by A48,XREAL_1:31;
then A151:n+1 in Seg (len p2);
then A152:n+1 in dom p2 by FINSEQ_1:def 3;
A153:p2/.(n+1)= p2.(n+1) by A150,FINSEQ_4:15;
dom F2 = DX2 by FUNCT_2:def 1;
then rng p2 c= dom F2;
then
A154: n+1 in dom (F2*p2) by A152,RELAT_1:27;
A155:F2.(p2/.(n + 1))= (F2*p2).(n+1) by A152,A153,FUNCT_1:13
.= ((Func_Seq(F2,p2))/.(n+1)) by A154,PARTFUN1:def 6;
A156: 1 <= nx & nx <= lb by A147,A146,A142,FINSEQ_1:1;
then
A157:nx+lb*n <= lb + lb*n by XREAL_1:6;
A158:nx <= nx+lb*n by NAT_1:11;
then 1<= nx+lb*n & nx+lb*n <= lb*la
by A157,A48,A156,XXREAL_0:2; then
nx+lb*n in dom FG by A51; then
A159:q3.(nx+lb*n) = [ p1.(((nx+lb*n)-'1) mod lb + 1),
p2.(((nx+lb*n)-'1) div lb + 1) ] by A50;
A160:nx in dom q31 by A147,A146,FINSEQ_1:def 3;
A161:(nx+lb*n)-'1 =(nx+lb*n)-1
by A158,A156,XREAL_1:233,XXREAL_0:2
.=(nx-1) +lb*n
.=(nx-'1) +lb*n by A148,XREAL_1:233;
nx-1 < nx by XREAL_1:44;
then
nx-1 < lb by A156,XXREAL_0:2;
then
A162: (nx-'1) < lb by A148,XREAL_1:233;
A163:((nx-'1) +lb*n) div lb +1
= (nx-'1) div lb + n +1 by A62,NAT_D:61
.= (0 qua Nat) + n+1 by A162,NAT_D:27;
A164:((nx-'1) +lb*n) mod lb +1 = (nx-'1) mod lb +1 by NAT_D:61
.=(nx-'1) +1 by A162,NAT_D:24
.=nx-1 +1 by A148,XREAL_1:233;
A165:nx in dom p1 & (n + 1) in dom p2 by A146,A144,A151,
FINSEQ_1:def 3;
then
p1/.nx = p1.nx & p2.(n + 1)= p2/.(n + 1) by PARTFUN1:def 6;
then
A166: q31.nx = [ p1/.nx, p2/.(n + 1) ]
by A160,A159,A141,A161,A163,A164,RFINSEQ:def 1;
p1.nx in Y1 & p2.(n + 1) in Y2 by A165,A48,A1,FUNCT_1:3; then
A167: p1/.nx in Y1 & p2/.(n + 1) in Y2 by A165,PARTFUN1:def 6;
thus (G*q31).x =G.(p1/.nx, p2/.(n + 1)) by A166,A146,FUNCT_1:12
.=F1.(p1/.nx ) * F2.(p2/.(n + 1)) by A48,A167
.= ((F1*p1).nx) *((Func_Seq(F2,p2))/.(n+1))
by A155,A149,A139,A146,A144,FUNCT_1:12
.= (((Func_Seq(F2,p2))/.(n+1)) (#)(F1*p1) ).x by VALUED_1:6;
end;
then Func_Seq(G,q31) =
((Func_Seq(F2,p2))/.(n+1)) * (Func_Seq(F1,p1)) by A145,FUNCT_1:2;
then
A168: Sum(Func_Seq(G,q31)) = Sum(Func_Seq(F1,p1))
*((Func_Seq(F2,p2))/.(n+1)) by RVSUM_1:87;
A169: Func_Seq(G,q3) = Func_Seq(G,q30) ^ Func_Seq(G,q31) by A99,Lm5;
dom F2 = DX2 by FUNCT_2:def 1;
then rng p2 c= dom F2;
then dom (F2*p2) =dom p2 by RELAT_1:27;
then dom (Func_Seq(F2,p2)) = Seg(len p2) by FINSEQ_1:def 3;
then
A170: len (Func_Seq(F2,p2)) = n+1 by A48,FINSEQ_1:def 3;
(Func_Seq(F2,p2)) | n = Func_Seq(F2,p20) by RELAT_1:83;
then A171: Func_Seq(F2,p2) = (Func_Seq(F2,p20))
^ <* (Func_Seq(F2,p2))/.(n+1) *> by A170,FINSEQ_5:21;
A172: Sum(Func_Seq(G,q3))
=Sum(Func_Seq(G,q30)) + Sum(Func_Seq(G,q31)) by A169,RVSUM_1:75
.= Sum(Func_Seq(F1,p1))*(Sum(Func_Seq(F2,p20))
+ (Func_Seq(F2,p2))/.(n+1) ) by A138,A168
.= Sum(Func_Seq(F1,p1))* Sum(Func_Seq(F2,p2)) by A171,RVSUM_1:74;
consider P being Permutation of dom p3 such that
A173:
q3 = p3*P & dom P = dom p3 & rng P = dom p3 by A75,A76,A48,BHSP_5:1;
A174: Func_Seq(G,q3) = Func_Seq(G,p3)*P by A173,RELAT_1:36;
dom G = [:DX1,DX2:] by FUNCT_2:def 1;then
rng p3 c= dom G;then
dom Func_Seq(G,p3) = dom p3 by RELAT_1:27;
hence
Sum(Func_Seq(G,p3)) = Sum(Func_Seq(F1,p1))* Sum(Func_Seq(F2,p2))
by A172,A174,FINSOP_1:7;
end;
hence F[n+1];
end;
end;
hence F[n+1];
end;
A175: for n be Nat holds F[n] from NAT_1:sch 2(A4,A45);
now let p2 be FinSequence of DX2,
p3 be FinSequence of [:DX1,DX2:],
Y2 be non empty finite Subset of DX2,
Y3 be finite Subset of [:DX1,DX2:];
assume A176:
p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 &
Y3= [:Y1,Y2:] &
for x,y be set st x in Y1 & y in Y2 holds G.(x,y)= (F1.x)*(F2.y);
len p2 is Element of NAT;
hence Sum(Func_Seq(G,p3))= Sum(Func_Seq(F1,p1))*Sum(Func_Seq(F2,p2))
by A175,A176;
end;
hence thesis;
end;
theorem Th12:
for DX1,DX2 be non empty set, F1 be Function of DX1,REAL,
F2 be Function of DX2,REAL,
G be Function of [:DX1,DX2:], REAL,
Y1 be non empty finite Subset of DX1,
Y2 be non empty finite Subset of DX2,
Y3 be finite Subset of [:DX1,DX2:] st Y3= [:Y1,Y2:] &
for x,y be set st x in Y1 & y in Y2 holds G.(x,y)= (F1.x)*(F2.y)
holds
setopfunc(Y3,[:DX1,DX2:],REAL,G,addreal)
=setopfunc(Y1,DX1,REAL,F1,addreal) * setopfunc(Y2,DX2,REAL,F2,addreal)
proof
let DX1,DX2 be non empty set,
F1 be Function of DX1,REAL,
F2 be Function of DX2,REAL,
G be Function of [:DX1,DX2:],REAL,
Y1 be non empty finite Subset of DX1,
Y2 be non empty finite Subset of DX2,
Y3 be finite Subset of [:DX1,DX2:];
assume A1:
Y3= [:Y1,Y2:] & for x,y be set st x in Y1 & y in Y2
holds G.(x,y)= (F1.x)*(F2.y);
consider p1 being FinSequence of DX1 such that
A2: p1 is one-to-one & rng p1 = Y1 & setopfunc(Y1,DX1,REAL,F1,addreal)
=Sum(Func_Seq(F1,p1)) by Th9;
consider p2 being FinSequence of DX2 such that
A3: p2 is one-to-one & rng p2 = Y2 & setopfunc(Y2,DX2,REAL,F2,addreal)
=Sum(Func_Seq(F2,p2)) by Th9;
consider p3 being FinSequence of [:DX1,DX2:] such that
A4: p3 is one-to-one & rng p3 = Y3 &
setopfunc(Y3,[:DX1,DX2:],REAL,G,addreal)
=Sum(Func_Seq(G,p3)) by Th9;
thus thesis by A1,A2,A3,A4,Th11;
end;
theorem Th13:
for DX be non empty set, F be Function of DX,REAL,
Y be finite Subset of DX st
for x be set st x in Y holds 0<= F.x holds
0 <= setopfunc(Y,DX,REAL,F,addreal)
proof
let DX be non empty set,
F be Function of DX,REAL,
Y be finite Subset of DX;
assume A1:for x be set st x in Y holds 0<= F.x;
consider p being FinSequence of DX such that
A2: p is one-to-one & rng p = Y &
setopfunc(Y,DX,REAL,F,addreal) =Sum(Func_Seq(F,p)) by Th9;
now let i be Nat;
assume A3: i in dom (Func_Seq(F,p));
then
A4: (Func_Seq(F,p)).i = F.(p.i) by FUNCT_1:12;
i in dom p by A3,FUNCT_1:11;
hence 0 <= (Func_Seq(F,p)).i by A4,A1,A2,FUNCT_1:3;
end;
hence thesis by A2,RVSUM_1:84;
end;
theorem Th14:
for DX be non empty set, F be Function of DX,REAL,
Y1,Y2 be finite Subset of DX st
Y1 c= Y2 & for x be set st x in Y2 holds 0<= F.x holds
setopfunc(Y1,DX,REAL,F,addreal)
<= setopfunc(Y2,DX,REAL,F,addreal)
proof
let DX be non empty set, F be Function of DX,REAL,
Y1,Y2 be finite Subset of DX;
assume A1:
Y1 c= Y2 & for x be set st x in Y2 holds 0<= F.x;
consider p1 being FinSequence of DX such that
A2: p1 is one-to-one & rng p1 = Y1 & setopfunc(Y1,DX,REAL,F,addreal)
=Sum(Func_Seq(F,p1)) by Th9;
reconsider Y3 = Y2 \ Y1 as finite Subset of DX;
consider p2 being FinSequence of DX such that
A3: p2 is one-to-one & rng p2 = Y3 &
setopfunc(Y3,DX,REAL,F,addreal)=Sum(Func_Seq(F,p2)) by Th9;
now let i be Nat;
assume A4: i in dom (Func_Seq(F,p2)); then
A5: (Func_Seq(F,p2)).i = F.(p2.i) by FUNCT_1:12;
i in dom p2 by A4,FUNCT_1:11; then
A6: p2.i in Y3 by A3,FUNCT_1:3;
Y3 c= Y2 by XBOOLE_1:36;
hence 0 <= (Func_Seq(F,p2)).i by A5,A1,A6;
end; then
A7: 0 <= Sum(Func_Seq(F,p2)) by RVSUM_1:84;
reconsider p3=p1^p2 as FinSequence of DX;
A8: rng p3 = rng p1 \/ rng p2 by FINSEQ_1:31
.=Y1 \/ Y2 by A3,A2,XBOOLE_1:39
.=Y2 by A1,XBOOLE_1:12;
rng p1 misses rng p2 by A2,A3,XBOOLE_1:79;
then
p3 is one-to-one by A2,A3,FINSEQ_3:91;
then A9: setopfunc(Y2,DX,REAL,F,addreal)
=Sum(Func_Seq(F,p3)) by A8,Th10;
A10: Func_Seq(F,p3)= Func_Seq(F,p1) ^ Func_Seq(F,p2) by Lm5;
Sum(Func_Seq(F,p1)) + (0 qua Real)
<= Sum(Func_Seq(F,p1)) + Sum(Func_Seq(F,p2)) by A7,XREAL_1:6;
hence thesis by A2,A10,A9,RVSUM_1:75;
end;
theorem Th15:
for Omega be non empty finite set,
P be Probability of Trivial-SigmaField (Omega),
Y be non empty finite Subset of Omega,
f be Function of Omega,REAL
ex G being FinSequence of REAL, s being FinSequence of Y
st
len G = card (Y) & s is one-to-one
& rng s = Y & len s = card (Y)
& (for n being Nat st n in dom G holds G.n
= (f.(s.n)) * P.{s.n})
& Integral(P2M(P),f|Y) = Sum G
proof
let Omega be non empty finite set,
P be Probability of Trivial-SigmaField (Omega),
Y be non empty finite Subset of Omega,
f be Function of Omega,REAL;
set YN= Omega \ Y;
A1:
dom (YN --> 0) =YN & rng (YN --> 0) c=REAL by FUNCOP_1:13;
A2:
dom (f +* (YN --> 0))= dom f \/ dom (YN --> 0) by FUNCT_4:def 1
.=Omega \/ YN by A1,FUNCT_2:def 1
.=Omega by XBOOLE_1:12;
rng (f +* (YN --> 0)) c= REAL;
then reconsider g= f +* (YN --> 0) as Function of Omega,REAL
by A2,FUNCT_2:2;
consider G being
FinSequence of REAL, s being FinSequence of Omega such that
A3: 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 = g.(s.n) * P.{s.n})
& Integral(P2M(P),g) = Sum G by RANDOM_1:13;
reconsider g as Real-Valued-Random-Variable
of Trivial-SigmaField (Omega) by RANDOM_1:29;
A4:dom g = Omega by FUNCT_2:def 1;
g is_integrable_on P by RANDOM_1:30; then
A5: g is_integrable_on P2M(P) by RANDOM_1:def 2;
A6: Y misses YN by XBOOLE_1:79;
A7: Integral(P2M(P),g|(Y \/ YN)) =
Integral(P2M(P),g|Y) + Integral(P2M(P),g|YN)
by A5,MESFUNC6:92,XBOOLE_1:79;
Y \/ YN = Y \/ Omega by XBOOLE_1:39
.= Omega by XBOOLE_1:12;
then A8: g|(Y \/ YN) = g;
A9: g|Y = (f|Y) by A1,A6,FUNCT_4:72;
A10: dom (g|YN) = YN by A4,RELAT_1:62;
reconsider zz=0 as R_eal by XXREAL_0:def 1;
A11: for x be object st x in dom (g|YN) holds (g|YN).x = 0
proof
let x be object;
assume A12:x in dom (g|YN);
then A13:x in YN & (g|YN).x = g.x by A4,FUNCT_1:47,RELAT_1:62;
g.x=(YN --> 0).x by A12,A1,A10,FUNCT_4:13;
hence thesis by A13,FUNCOP_1:7;
end;
then
Integral(P2M(P),g|YN) = zz * (P2M(P)).(YN) by A10,MESFUNC6:97
.= 0;
then
A14: Integral(P2M(P),g) = Integral(P2M P,(f|Y)) by A9,A7,A8,XXREAL_3:4;
set N1= s" Y;
s is Function of dom s, rng s by FUNCT_2:1;then
N1 is finite Subset of dom s by FUNCT_2:39;then
reconsider N1 as finite Subset of Seg len G
by A3,FINSEQ_1:def 3;
rng canFS N1 c= N1 by FINSEQ_1:def 4;
then
rng canFS N1 c= Seg len G by XBOOLE_1:1;
then
A15:canFS N1 is FinSequence of Seg len G by FINSEQ_1:def 4;
dom s = Seg len G by A3,FINSEQ_1:def 3;
then
A16:s is Function of Seg (len G),Omega by A3,FUNCT_2:1;
then reconsider t1= s*canFS(N1)
as FinSequence of Omega by A15,FINSEQ_2:32;
A17:rng t1 = s.:(rng canFS N1) by RELAT_1:127
.=s.: N1 by FUNCT_2:def 3
.=Y by A3,FUNCT_1:77;
set N2= Seg (len G) \ N1;
reconsider N2 as finite Subset of Seg len G by XBOOLE_1:36;
rng canFS N2 c= N2 by FINSEQ_1:def 4;
then rng canFS N2 c= Seg len G by XBOOLE_1:1;
then
canFS N2 is FinSequence of Seg len G by FINSEQ_1:def 4;
then
reconsider t2= s*canFS(N2) as FinSequence of Omega by A16,FINSEQ_2:32;
reconsider t=t1 ^ t2 as FinSequence of Omega;
A18: rng (canFS(N1)) =N1 by FUNCT_2:def 3;
A19:rng (canFS(N2)) =N2 by FUNCT_2:def 3;
A20: N1 is finite Subset of dom s &
N2 is finite Subset of (dom s) by A3,FINSEQ_1:def 3;
rng (s|N1) misses rng (s|N2) by Th1,A3,XBOOLE_1:79;
then rng t1 misses rng (s|N2) by A18,Th2,XBOOLE_1:63;
then A21:rng t1 misses rng t2 by A19,Th2,XBOOLE_1:63;
then A22: t is one-to-one by A3,FINSEQ_3:91;
len (canFS(N1)) = card N1 by FINSEQ_1:93;then
A23:dom (canFS(N1))= Seg(card N1) by FINSEQ_1:def 3;
rng (canFS(N1)) is Subset of dom s by A20,FUNCT_2:def 3;then
dom t1 = Seg(card N1) by A23,RELAT_1:27;then
A24:len t1 = card N1 by FINSEQ_1:def 3;
len canFS N2 = card N2 by FINSEQ_1:93;then
A25:dom canFS N2 = Seg card N2 by FINSEQ_1:def 3;
rng canFS N2 is Subset of dom s by A20,FUNCT_2:def 3;then
dom t2 = Seg card N2 by A25,RELAT_1:27;then
A26:len t2 = card N2 by FINSEQ_1:def 3;
A27:N1 \/ N2 = (Seg len G) \/ N1 by XBOOLE_1:39
.= Seg len G by XBOOLE_1:12
.= dom s by A3,FINSEQ_1:def 3;
dom t = Seg (len t1 + len t2) by FINSEQ_1:def 7
.=Seg(card (N1 \/ N2)) by A24,A26,CARD_2:40,XBOOLE_1:79;
then
A28:len t = card (N1 \/ N2) by FINSEQ_1:def 3;
then
A29:len t = len s by A27,CARD_1:62;
A30:Seg len s = Seg len t by A28,A27,CARD_1:62;
A31: dom s = Seg(len s) by FINSEQ_1:def 3
.=dom t by A30,FINSEQ_1:def 3;
A32:card dom t = card Omega by A3,A29,CARD_1:62;
t is Function of dom t, Omega by FINSEQ_2:26;then
t is onto by A22,A32,FINSEQ_4:63; then
rng s = rng t by A3,FUNCT_2:def 3; then
consider PN being Permutation of dom s such that
A33: t = s*PN & dom PN = dom s & rng PN = dom s by A3,A22,BHSP_5:1;
defpred FF1[object,object] means
( t.$1 in Y implies $2 = (f.(t.$1)) * P.{t.$1}) &
( (not t.$1 in Y) implies $2 = (g.(t.$1)) * P.{t.$1});
A34:now let k be Nat;
assume k in Seg card Omega;
now per cases;
suppose t.k in Y;
hence ex x being Real st FF1[k,x];
end;
suppose not t.k in Y;
hence ex x being Real st FF1[k,x];
end;
end;
then consider x being Real such that
A35: FF1[k,x];
reconsider x as Element of REAL by XREAL_0:def 1;
take x;
thus FF1[k,x] by A35;
end;
consider F be FinSequence of REAL such that
A36: dom F = Seg card (Omega) and
A37: for n be Nat st n in Seg card (Omega)
holds FF1[n,F.n] from FINSEQ_1:sch 5(A34);
A38: dom s = Seg (len G) by A3,FINSEQ_1:def 3
.= dom G by FINSEQ_1:def 3;
then A39: dom(G*PN) = dom PN by A33,RELAT_1:27;
A40: dom F =dom s by A3,A36,FINSEQ_1:def 3;
now let x be object;
assume A41: x in dom F;
then reconsider nx=x as Element of NAT;
A42: nx in dom t by A41,A3,A36,A31,FINSEQ_1:def 3;
A43:t.nx =s.(PN.nx) by A33,A41,A40,A31,FUNCT_1:12;
PN.nx in dom G by A38,A42,A33,FUNCT_1:11; then
A44: G.(PN.nx) = g.(s.(PN.nx)) * P.{s.(PN.nx)} by A3;
now per cases;
suppose A45:t.nx in Y;
hence F.nx = (f.(t.nx)) * P.{t.nx} by A37,A36,A41
.= ((f|Y).(s.(PN.nx))) * P.{s.(PN.nx)} by A43,A45,FUNCT_1:49
.= (g.(s.(PN.nx))) * P.{s.(PN.nx)} by A45,A43,A9,FUNCT_1:49
.= (G*PN).nx by A40,A41,A33,A44,FUNCT_1:13;
end;
suppose not t.nx in Y;
hence F.nx = (g.(s.(PN.nx))) * P.{s.(PN.nx)} by A43,A37,A36,A41
.= (G*PN).nx by A40,A41,A33,A44,FUNCT_1:13;
end;
end;
hence F.x=(G*PN).x;
end;
then
F=G*PN by A33,A39,A40,FUNCT_1:2;
then A46: Sum G = Sum F by A38,FINSOP_1:7;
reconsider t1 as FinSequence of Y by A17,FINSEQ_1:def 4;
set F1 = F | len t1;
set F2 = F /^ len t1;
A47: F = F1^F2 by RFINSEQ:8;
A48: len t1 = card Y by A17,A3,FINSEQ_4:62;
A49: len F = card Omega by A36,FINSEQ_1:def 3;
A50:len F = len t by A29,A3,A36,FINSEQ_1:def 3;
A51: len t= len t1 + len t2 by FINSEQ_1:22;
then
A52:len t1 <= len t by NAT_1:11;
then
A53: len F2 = len F - len t1 by A50,RFINSEQ:def 1
.= len t2 by A51,A50;
then A54: dom F2 = Seg len t2 by FINSEQ_1:def 3
.= dom ((len t2) |->0) by FUNCOP_1:13;
now let m be Nat;
assume A55: m in dom F2;
then A56:m in Seg len t2 by A53,FINSEQ_1:def 3;
then
A57: m in dom t2 by FINSEQ_1:def 3;
A58: 1 <= m & m <= len t2 by A56,FINSEQ_1:1;
m <= m+len t1 by NAT_1:11;
then
1<= m+len t1 & m+len t1 <= len t by A51,A58,XREAL_1:6,XXREAL_0:2;
then
A59: m+len t1 in Seg card (Omega) by A3,A29;
A60: t.(m+len t1) = t2.m by A57,FINSEQ_1:def 7;
A61: rng t1 /\ rng t2 = {} by A21,XBOOLE_0:def 7;
A62: t2.m in rng t2 by A57,FUNCT_1:3;
then
not t2.m in rng t1 by A61,XBOOLE_0:def 4;
then A63: t2.m in dom (g|YN) by A10,A17,A62,XBOOLE_0:def 5;
then A64: g.(t2.m) = (g|YN).(t2.m) by FUNCT_1:47
.= 0 by A11,A63;
not t.(m+len t1) in Y by A17,A61,A62,A60,XBOOLE_0:def 4;
then
A65:F.(m+len t1) = (g.(t.(m+len t1))) * P.{t.(m+len t1)} by A37,A59
.= 0 by A64,A60;
thus F2.m = F.(m+len t1) by A50,A52,A55,RFINSEQ:def 1
.= ((len t2) |->0).m by A56,A65,FINSEQ_2:57;
end; then
A66: F2 = ((len t2) |->0) by A54,FINSEQ_1:13;
Segm card Y c= Segm card Omega by CARD_1:11; then
A67: card(Y) <= card Omega by NAT_1:39;
A68: Sum(F) = Sum F1 + Sum F2 by A47,RVSUM_1:75
.= Sum F1 + (0 qua Real) by A66,RVSUM_1:81
.= Sum F1;
A69: len F1 = card Y by A49,A48,A67,FINSEQ_1:59;
for n being Nat st n in dom F1 holds F1.n = (f.(t1.n)) * P.{t1.n}
proof
let n be Nat;
assume n in dom F1; then
A70: n in Seg (len t1) by A69,A48,FINSEQ_1:def 3; then
A71:n in dom t1 by FINSEQ_1:def 3;
then
A72: t.n=t1.n by FINSEQ_1:def 7;
then
A73: t.n in Y by A17,A71,FUNCT_1:3;
A74:Seg len t1 c= Seg card(Omega) by A48,A67,FINSEQ_1:5;
thus F1.n = F.n by A70,FUNCT_1:49
.= (f.(t1.n)) * P.{t1.n} by A72,A74,A70,A37,A73;
end;
hence thesis by A69,A48,A17,A68,A46,A3,A14;
end;
reconsider jj=1 as R_eal by XXREAL_0:def 1;
Lm7:
for Omega1, Omega2 be non empty finite set, P1 be Probability of
Trivial-SigmaField (Omega1), P2 be Probability of
Trivial-SigmaField (Omega2),
Q be Function of [:Omega1,Omega2:],REAL,
P be Function of (bool [:Omega1,Omega2:]),REAL,
Y1 be non empty finite Subset of Omega1,
Y2 be non empty finite Subset of Omega2 st
(for x,y be set st x in Omega1 & y in Omega2
holds Q.(x,y) = (P1.{x})*(P2.{y}) ) &
(for z be finite Subset of [:Omega1,Omega2:]
holds P.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal)) holds
P.([:Y1,Y2:]) = (P1.Y1)*(P2.Y2)
proof
let Omega1, Omega2 be non empty finite set, P1 be Probability of
Trivial-SigmaField (Omega1), P2 be Probability of
Trivial-SigmaField (Omega2),
Q be Function of [:Omega1,Omega2:],REAL,
P be Function of (bool [:Omega1,Omega2:]),REAL,
Y1 be non empty finite Subset of Omega1,
Y2 be non empty finite Subset of Omega2;
assume A1:
(for x,y be set st x in Omega1 & y in Omega2
holds Q.(x,y) = (P1.{x})*(P2.{y}) ) &
(for z be finite Subset of [:Omega1,Omega2:]
holds P.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal));
deffunc FF1(object)=P1.{$1};
A2: for x be object st x in Y1 holds FF1(x) in REAL by XREAL_0:def 1;
consider F1 being Function of Y1,REAL such that
A3: for x be object st x in Y1 holds F1.x = FF1(x) from FUNCT_2:sch 2(A2);
deffunc FF2(object)=P2.{$1};
A4: for x be object st x in Y2 holds FF2(x) in REAL by XREAL_0:def 1;
consider F2 being Function of Y2,REAL such that
A5: for x be object st x in Y2 holds F2.x = FF2(x) from FUNCT_2:sch 2(A4);
for x being object st x in {{},1} holds x in REAL
by XREAL_0:def 1;
then
A6:{{},1} c=REAL;
A7:dom chi(Y1,Omega1) = Omega1 &
rng chi(Y1,Omega1) c= {{},1} by FUNCT_3:39,def 3;then
chi(Y1,Omega1) is Function of Omega1,{{},1}
by FUNCT_2:def 1,RELSET_1:4; then
reconsider f1= chi(Y1,Omega1) as Function of Omega1,REAL
by A6,FUNCT_2:7;
A8: dom (f1|Y1) = dom f1 /\ Y1 by RELAT_1:61
.=Y1 by A7,XBOOLE_1:28;
for x be object st x in dom (f1|Y1) holds (f1|Y1).x = 1
proof
let x be object;
assume A9: x in dom (f1|Y1);
then (f1|Y1).x = f1.x by FUNCT_1:47
.= 1 by A9,A8,FUNCT_3:def 3;
hence thesis;
end;
then A10:Integral(P2M(P1),f1|Y1) = jj * (P2M(P1)).(dom (f1|Y1))
by MESFUNC6:97
.= 1 * (P1.Y1) by A8,EXTREAL1:1
.= P1.Y1;
consider G1 being FinSequence of REAL, s1 being FinSequence of Y1
such that
A11: len G1 = card (Y1) & s1 is one-to-one & rng s1 = Y1 & len s1 = card (Y1)
& (for n being Nat st n in dom G1 holds G1.n
= (f1.(s1.n)) * P1.{s1.n})
& Integral(P2M(P1),f1|Y1) = Sum G1 by Th15;
Y1 c= Y1; then
reconsider YY1=Y1 as finite Subset of Y1;
dom F1=Y1 by FUNCT_2:def 1; then
A12: dom(F1*s1) = dom s1 by A11,RELAT_1:27;
A13: dom G1 = Seg len s1 by A11,FINSEQ_1:def 3
.=dom s1 by FINSEQ_1:def 3;
now let x be object;
assume A14: x in dom G1;
then reconsider nx=x as Element of NAT;
A15:s1.nx in Y1 by A11,A13,A14,FUNCT_1:3;
thus G1.x = (f1.(s1.nx)) * P1.{s1.nx} by A11,A14
.= 1*P1.{s1.nx} by A15,FUNCT_3:def 3
.= F1.(s1.nx) by A3,A11,A13,A14,FUNCT_1:3
.=(F1*s1).x by A13,A14,FUNCT_1:13;
end;
then
G1=Func_Seq(F1,s1) by A12,A13,FUNCT_1:2;
then
A16:setopfunc(YY1,Y1,REAL,F1,addreal) =Sum G1 by A11,Th10;
A17:dom chi(Y2,Omega2) = Omega2 &
rng chi(Y2,Omega2) c= {{},1} by FUNCT_3:39,def 3;then
chi(Y2,Omega2) is Function of Omega2,{{},1} by FUNCT_2:def 1,RELSET_1:4;
then reconsider f2=chi(Y2,Omega2)
as Function of Omega2,REAL by A6,FUNCT_2:7;
A18: dom (f2|Y2) = dom f2 /\ Y2 by RELAT_1:61
.=Y2 by A17,XBOOLE_1:28;
for x be object st x in dom (f2|Y2) holds (f2|Y2).x = 1
proof
let x be object;
assume A19: x in dom (f2|Y2);
then (f2|Y2).x = f2.x by FUNCT_1:47
.= 1 by A19,A18,FUNCT_3:def 3;
hence thesis;
end;
then
A20:Integral(P2M(P2),f2|Y2) = jj * (P2M(P2)).Y2 by A18,MESFUNC6:97
.= 1 * (P2.Y2) by EXTREAL1:1
.= P2.Y2;
consider G2 being FinSequence of REAL, s2 being FinSequence of Y2
such that
A21: len G2 = card (Y2) & s2 is one-to-one & rng s2 = Y2 & len s2 = card (Y2)
& (for n being Nat st n in dom G2 holds G2.n
= (f2.(s2.n)) * P2.{s2.n})
& Integral(P2M(P2),f2|Y2) = Sum G2 by Th15;
Y2 c= Y2; then
reconsider YY2=Y2 as finite Subset of Y2;
dom F2=Y2 by FUNCT_2:def 1; then
A22: dom(F2*s2) = dom s2 by A21,RELAT_1:27;
A23: dom G2= Seg (len s2) by A21,FINSEQ_1:def 3
.=dom s2 by FINSEQ_1:def 3;
now let x be object;
assume A24: x in dom G2; then
reconsider nx=x as Element of NAT;
A25:s2.nx in Y2 by A21,A23,A24,FUNCT_1:3;
thus G2.x = (f2.(s2.nx)) * P2.{s2.nx} by A21,A24
.= 1*P2.{s2.nx} by A25,FUNCT_3:def 3
.= F2.(s2.nx) by A5,A21,A23,A24,FUNCT_1:3
.=(F2*s2).x by A23,A24,FUNCT_1:13;
end; then
G2 = Func_Seq(F2,s2) by A22,A23,FUNCT_1:2; then
A26:setopfunc(YY2,Y2,REAL,F2,addreal) =Sum G2 by A21,Th10;
reconsider Y3= [:Y1,Y2:] as finite Subset of [:Y1,Y2:]
by ZFMISC_1:96;
reconsider Y33= [:Y1,Y2:] as finite Subset of [:Omega1,Omega2:]
by ZFMISC_1:96;
A27: [:Y1,Y2:] c= [:Omega1,Omega2:] by ZFMISC_1:96;
then
reconsider Q0=Q|[:Y1,Y2:] as Function of [:Y1,Y2:],REAL by FUNCT_2:32;
A28: now let x,y be set;
assume A29: x in Y1 & y in Y2; then
[x,y] in [:Y1,Y2:] by ZFMISC_1:def 2;
then [x,y] in dom Q0 by FUNCT_2:def 1;
hence Q0.(x,y) =Q.(x,y) by FUNCT_1:47
.= (P1.{x})*(P2.{y}) by A1,A29
.= (F1.x)*(P2.{y}) by A29,A3
.= (F1.x)*(F2.y) by A29,A5;
end;
consider pp1 being FinSequence of [:Y1,Y2:] such that
A30: pp1 is one-to-one & rng pp1 = Y3 & setopfunc(Y3,[:Y1,Y2:],REAL,Q0,addreal)
= addreal "**" Func_Seq(Q0,pp1) by BHSP_5:def 5;
A31:rng pp1 c= [:Omega1,Omega2:] by A27;
then reconsider pp2=pp1
as FinSequence of [:Omega1,Omega2:] by FINSEQ_1:def 4;
rng pp1 c= dom Q by A31,FUNCT_2:def 1;
then A32: dom(Q*pp1)= dom pp1 by RELAT_1:27;
A33: dom Q0=[:Y1,Y2:] by FUNCT_2:def 1;
for x be object st x in dom (Q0*pp1) holds (Q0*pp1).x=(Q*pp1).x
proof
let x be object;
assume x in dom (Q0*pp1);
then A34:(Q0*pp1).x =Q0.(pp1.x) &x in dom pp1 by FUNCT_1:11,12;
then (pp1.x) in rng pp1 by FUNCT_1:3;
then Q0.(pp1.x)=Q.(pp1.x) by FUNCT_1:49;
hence thesis by A34,FUNCT_1:13;
end;then
A35: Func_Seq(Q0,pp1) = Func_Seq(Q,pp2)
by A33,A32,A31,FUNCT_1:2,RELAT_1:27;
A36:
setopfunc(Y3,[:Y1,Y2:],REAL,Q0,addreal)
= setopfunc(Y33,[:Omega1,Omega2:],REAL,Q,addreal)
by A30,A35,BHSP_5:def 5;
thus P.([:Y1,Y2:] ) = setopfunc(Y33,[:Omega1,Omega2:],REAL,Q,addreal) by A1
.= (P1.Y1)*(P2.Y2) by A20,A21,A10,A11,A26,A16,Th12,A28,A36;
end;
Lm8:
for Omega1, Omega2 be non empty finite set,
P1 be Probability of Trivial-SigmaField Omega1,
P2 be Probability of Trivial-SigmaField Omega2,
Q be Function of [:Omega1,Omega2:],REAL,
P be Function of (bool [:Omega1,Omega2:]),REAL st
(for x,y be set st x in Omega1 & y in Omega2
holds Q.(x,y) = (P1.{x})*(P2.{y}) ) &
(for z be finite Subset of [:Omega1,Omega2:]
holds P.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal)) holds
P.([:Omega1,Omega2:]) = 1
proof
let Omega1, Omega2 be non empty finite set, P1 be Probability of
Trivial-SigmaField (Omega1), P2 be Probability of
Trivial-SigmaField (Omega2),
Q be Function of [:Omega1,Omega2:],REAL,
P be Function of (bool [:Omega1,Omega2:]),REAL;
assume A1:
(for x,y be set st x in Omega1 & y in Omega2
holds Q.(x,y) = (P1.{x})*(P2.{y}) ) &
(for z be finite Subset of [:Omega1,Omega2:]
holds P.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal));
deffunc FF1(object)=P1.{$1};
A2: for x be object st x in Omega1 holds FF1(x) in REAL by XREAL_0:def 1;
consider F1 being Function of Omega1,REAL such that
A3: for x be object st x in Omega1 holds F1.x = FF1(x)
from FUNCT_2:sch 2(A2);
deffunc FF2(object)=P2.{$1};
A4: for x be object st x in Omega2 holds FF2(x) in REAL by XREAL_0:def 1;
consider F2 being Function of Omega2,REAL such that
A5: for x be object st x in Omega2 holds F2.x = FF2(x)
from FUNCT_2:sch 2(A4);
A6:dom (Omega1-->1) = Omega1 by FUNCOP_1:13;
rng (Omega1-->1) c=REAL; then
reconsider f1=(Omega1-->1) as Function of Omega1,REAL by A6,FUNCT_2:2;
for x be object st x in dom (Omega1-->1) holds (Omega1-->1).x = 1
by FUNCOP_1:7; then
A7:Integral(P2M(P1),f1) = jj * ((P2M(P1)).(Omega1))
by A6,MESFUNC6:97
.=1 *(P1.(Omega1)) by EXTREAL1:1
.= 1 by PROB_1:def 8;
consider G1 being FinSequence of REAL,
s1 being FinSequence of Omega1 such that
A8: len G1 = card (Omega1) & s1 is one-to-one
& rng s1 = Omega1 & len s1 = card (Omega1)
& (for n being Nat st n in dom G1 holds G1.n
= (f1.(s1.n)) * P1.{s1.n})
& Integral(P2M(P1),f1) = Sum G1 by RANDOM_1:13;
Omega1 c= Omega1; then
reconsider Y1=Omega1 as finite Subset of Omega1;
dom F1=Y1 by FUNCT_2:def 1; then
A9: dom(F1*s1) = dom s1 by A8,RELAT_1:27;
A10: dom G1= Seg (len s1) by A8,FINSEQ_1:def 3
.=dom s1 by FINSEQ_1:def 3;
now let x be object;
assume A11: x in dom G1; then
reconsider nx=x as Element of NAT;
thus G1.x = (f1.(s1.nx)) * P1.{s1.nx} by A8,A11
.= 1*P1.{s1.nx} by A8,A10,A11,FUNCOP_1:7,FUNCT_1:3
.= F1.(s1.nx) by A3,A8,A10,A11,FUNCT_1:3
.= (F1*s1).x by A10,A11,FUNCT_1:13;
end; then
G1=Func_Seq(F1,s1) by A9,A10,FUNCT_1:2; then
A12:setopfunc(Y1,Omega1,REAL,F1,addreal)=1 by A7,A8,Th10;
A13:dom (Omega2-->1) = Omega2 by FUNCOP_1:13;
rng (Omega2-->1) c= REAL;then
reconsider f2=(Omega2-->1) as Function of Omega2,REAL by A13,FUNCT_2:2;
for x be object st x in dom (Omega2-->1) holds (Omega2-->1).x = 1
by FUNCOP_1:7; then
A14:Integral(P2M(P2),f2) = jj * ((P2M(P2)).(Omega2)) by A13,MESFUNC6:97
.= 1 *(P2.(Omega2)) by EXTREAL1:1
.= 1 by PROB_1:def 8;
consider G2 being FinSequence of REAL, s2 being FinSequence of Omega2
such that
A15: len G2 = card (Omega2) & s2 is one-to-one
& rng s2 = Omega2 & len s2 = card (Omega2)
& (for n being Nat st n in dom G2 holds G2.n
= (f2.(s2.n)) * P2.{s2.n})
& Integral(P2M(P2),f2) = Sum G2 by RANDOM_1:13;
Omega2 c= Omega2; then
reconsider Y2=Omega2 as finite Subset of Omega2;
dom F2=Y2 by FUNCT_2:def 1; then
A16: dom(F2*s2) = dom s2 by A15,RELAT_1:27;
A17: dom G2= Seg (len s2) by A15,FINSEQ_1:def 3
.=dom s2 by FINSEQ_1:def 3;
now let x be object;
assume A18: x in dom G2;
then reconsider nx=x as Element of NAT;
thus G2.x = (f2.(s2.nx)) * P2.{s2.nx} by A15,A18
.= 1*P2.{s2.nx} by A15,A17,A18,FUNCOP_1:7,FUNCT_1:3
.= F2.(s2.nx) by A5,A15,A17,A18,FUNCT_1:3
.=(F2*s2).x by A17,A18,FUNCT_1:13;
end; then
A19:G2 =Func_Seq(F2,s2) by A16,A17,FUNCT_1:2;
reconsider Y3= [:Y1,Y2:] as finite Subset of [:Omega1,Omega2:]
by ZFMISC_1:96;
A20: now let x,y be set;
assume A21: x in Y1 & y in Y2;
hence Q.(x,y)= (P1.{x})*(P2.{y}) by A1
.= (F1.x)*(P2.{y}) by A21,A3
.= (F1.x)*(F2.y) by A21,A5;
end;
thus P.([:Omega1,Omega2:] )
= setopfunc(Y3,[:Omega1,Omega2:],REAL,Q,addreal) by A1
.=setopfunc(Y1,Omega1,REAL,F1,addreal) *
setopfunc(Y2,Omega2,REAL,F2,addreal) by Th12,A20
.= 1 by A19,A14,A15,Th10,A12;
end;
Lm9:
for Omega1, Omega2 be non empty finite set,
P1 be Probability of Trivial-SigmaField Omega1,
P2 be Probability of Trivial-SigmaField Omega2,
Q be Function of [:Omega1,Omega2:],REAL,
P be Function of bool [:Omega1,Omega2:],REAL st
(for x,y be set st x in Omega1 & y in Omega2
holds Q.(x,y) = (P1.{x})*(P2.{y})) &
(for z be finite Subset of [:Omega1,Omega2:]
holds P.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal)) holds
for x be set st x c= [:Omega1,Omega2:]
holds 0 <= P.x & P.x <= 1
proof
let Omega1, Omega2 be non empty finite set, P1 be Probability of
Trivial-SigmaField (Omega1), P2 be Probability of
Trivial-SigmaField (Omega2),
Q be Function of [:Omega1,Omega2:],REAL,
P be Function of (bool [:Omega1,Omega2:]),REAL;
assume A1:
(for x,y be set st x in Omega1 & y in Omega2
holds Q.(x,y) = (P1.{x})*(P2.{y}) ) &
(for z be finite Subset of [:Omega1,Omega2:]
holds P.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal));
set Y12 = [:Omega1,Omega2:];
Y12 c= Y12; then
reconsider Y12 as finite Subset of [:Omega1,Omega2:];
A2:now let z be set;
assume z in [:Omega1,Omega2:]; then
consider x,y be object such that
A3: x in Omega1 & y in Omega2 & z=[x,y] by ZFMISC_1:def 2;
for xx be object st xx in {x} holds xx in Omega1 by A3,TARSKI:def 1;then
A4: {x} is Event of Trivial-SigmaField (Omega1)&
for xx be object st xx in {y} holds xx in Omega2
by A3,TARSKI:def 1,def 3;then
A5:{y} is Event of Trivial-SigmaField (Omega2) by TARSKI:def 3;
A6: Q.z=Q.(x,y) by A3
.= (P1.{x})*(P2.{y}) by A3,A1;
0 <= (P1.{x}) & 0 <= (P2.{y}) by A4,A5,PROB_1:def 8;
hence 0 <= Q.z by A6;
end;
let x be set;
assume x c= [:Omega1,Omega2:]; then
reconsider Y=x as finite Subset of [:Omega1,Omega2:];
for z be set st z in Y holds 0 <=Q.z by A2; then
0<= setopfunc(Y,[:Omega1,Omega2:],REAL,Q,addreal) by Th13;
hence 0<= P.x by A1;
A7: setopfunc(Y,[:Omega1,Omega2:],REAL,Q,addreal) <=
setopfunc(Y12,[:Omega1,Omega2:],REAL,Q,addreal) by A2,Th14;
setopfunc(Y12,[:Omega1,Omega2:],REAL,Q,addreal)=P.([:Omega1,Omega2:]) by A1;
then setopfunc(Y,[:Omega1,Omega2:],REAL,Q,addreal) <= 1 by A7,A1,Lm8;
hence P.x <= 1 by A1;
end;
definition
let Omega1, Omega2 be non empty finite set,
P1 be Probability of Trivial-SigmaField Omega1,
P2 be Probability of Trivial-SigmaField Omega2;
func Product-Probability (Omega1,Omega2,P1,P2)
-> Probability of Trivial-SigmaField ([:Omega1,Omega2:]) means :Def2:
ex Q be Function of [:Omega1,Omega2:],REAL st
(for x,y be set st x in Omega1 & y in Omega2
holds Q.(x,y) = (P1.{x})*(P2.{y}) ) &
(for z be finite Subset of [:Omega1,Omega2:]
holds it.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal));
existence
proof
consider Q be Function of [:Omega1,Omega2:],REAL such that
A1: for x,y be set st x in Omega1 & y in Omega2
holds Q.(x,y) = (P1.{x})*(P2.{y}) by Lm1;
consider P be Function of (bool [:Omega1,Omega2:]),REAL such that
A2: for z be finite Subset of [:Omega1,Omega2:]
holds P.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal) by Lm3;
A3: for x be set st x c= [:Omega1,Omega2:]
holds 0 <= P.x & P.x <= 1 by Lm9,A1,A2;
P.([:Omega1,Omega2:]) = 1 by A1,A2,Lm8;
then P is Probability of Trivial-SigmaField ([:Omega1,Omega2:])
by A2,A3,Th8;
hence thesis by A1,A2;
end;
uniqueness
proof
let PP1,PP2 be Probability of Trivial-SigmaField ([:Omega1,Omega2:]);
assume
A4: ex Q1 be Function of [:Omega1,Omega2:],REAL st
(for x,y be set st x in Omega1 & y in Omega2
holds Q1.(x,y) = (P1.{x})*(P2.{y}) ) &
(for z be finite Subset of [:Omega1,Omega2:]
holds PP1.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q1,addreal));
assume
A5: ex Q2 be Function of [:Omega1,Omega2:],REAL st
(for x,y be set st x in Omega1 & y in Omega2
holds Q2.(x,y) = (P1.{x})*(P2.{y}) ) &
(for z be finite Subset of [:Omega1,Omega2:]
holds PP2.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q2,addreal));
consider Q1 be Function of [:Omega1,Omega2:],REAL such that
A6: (for x,y be set st x in Omega1 & y in Omega2
holds Q1.(x,y) = (P1.{x})*(P2.{y}) ) &
(for z be finite Subset of [:Omega1,Omega2:]
holds PP1.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q1,addreal)) by A4;
consider Q2 be Function of [:Omega1,Omega2:],REAL such that
A7: (for x,y be set st x in Omega1 & y in Omega2
holds Q2.(x,y) = (P1.{x})*(P2.{y}) ) &
(for z be finite Subset of [:Omega1,Omega2:]
holds PP2.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q2,addreal)) by A5;
Q1=Q2 by A6,A7,Lm2;
hence PP1=PP2 by Lm4,A6,A7;
end;
end;
theorem Th16:
for Omega1, Omega2 be non empty finite set,
P1 be Probability of Trivial-SigmaField Omega1,
P2 be Probability of Trivial-SigmaField Omega2,
Y1 be non empty finite Subset of Omega1,
Y2 be non empty finite Subset of Omega2 holds
Product-Probability (Omega1,Omega2,P1,P2).([:Y1,Y2:]) = (P1.Y1)*(P2.Y2)
proof
let Omega1, Omega2 be non empty finite set,
P1 be Probability of Trivial-SigmaField (Omega1),
P2 be Probability of Trivial-SigmaField (Omega2),
Y1 be non empty finite Subset of Omega1,
Y2 be non empty finite Subset of Omega2;
set P=Product-Probability (Omega1,Omega2,P1,P2);
consider Q be Function of [:Omega1,Omega2:],REAL such that
A1: (for x,y be set st x in Omega1 & y in Omega2
holds Q.(x,y) = (P1.{x})*(P2.{y}) ) &
(for z be finite Subset of [:Omega1,Omega2:]
holds P.z = setopfunc(z,[:Omega1,Omega2:],REAL,Q,addreal)) by Def2;
thus P.([:Y1,Y2:]) = (P1.Y1)*(P2.Y2) by Lm7,A1;
end;
theorem
for Omega1, Omega2 be non empty finite set,
P1 be Probability of Trivial-SigmaField (Omega1),
P2 be Probability of Trivial-SigmaField (Omega2),
y1, y2 be set st y1 in Omega1 & y2 in Omega2 holds
Product-Probability (Omega1,Omega2,P1,P2).({[y1,y2]})
= (P1.{y1})*(P2.{y2})
proof
let Omega1, Omega2 be non empty finite set,
P1 be Probability of Trivial-SigmaField Omega1,
P2 be Probability of Trivial-SigmaField Omega2,
y1, y2 be set;
assume
A1: y1 in Omega1 & y2 in Omega2; then
A2: {y1} is finite Subset of Omega1 by ZFMISC_1:31;
for yy be object st yy in {y2} holds yy in Omega2 by A1,TARSKI:def 1;
then
A3: {y2} is finite Subset of Omega2 by TARSKI:def 3;
[:{y1},{y2}:] = {[y1,y2]} by ZFMISC_1:29;
hence Product-Probability (Omega1,Omega2,P1,P2).({[y1,y2]})
= (P1.{y1})*(P2.{y2}) by Th16,A2,A3;
end;
begin :: Algebra of Real Valued Random Variables
definition
let Omega be non empty set;
let Sigma be SigmaField of Omega;
func Real-Valued-Random-Variables-Set Sigma
-> non empty Subset of RAlgebra Omega equals
the set of all f where f is Real-Valued-Random-Variable of Sigma;
correctness
proof
A1: the set of all f where f
is Real-Valued-Random-Variable of Sigma is non empty
proof
set g = the Real-Valued-Random-Variable of Sigma;
g in the set of all f where f
is Real-Valued-Random-Variable of Sigma;
hence thesis;
end;
the set of all f where f is Real-Valued-Random-Variable of Sigma
c= Funcs(Omega,REAL)
proof
let x be object;
assume x in the set of all f where f
is Real-Valued-Random-Variable of Sigma;
then consider f be Real-Valued-Random-Variable of Sigma such that
A2: x=f;
thus thesis by A2,FUNCT_2:8;
end;
hence thesis by A1;
end;
end;
Lm10:
Real-Valued-Random-Variables-Set Sigma is additively-linearly-closed
multiplicatively-closed
proof
set W = Real-Valued-Random-Variables-Set Sigma;
set V = RAlgebra Omega;
A1: for v,u be Element of V st v in W & u in W
holds v * u in W
proof
let v,u be Element of V such that
A2: v in W and
A3: u in W;
consider u1 be Real-Valued-Random-Variable of Sigma such that
A4: u1=u by A3;
reconsider h = v*u as Element of Funcs(Omega,REAL);
consider v1 be Real-Valued-Random-Variable of Sigma such that
A5: v1=v by A2;
dom v1 /\ dom u1 = Omega /\ dom u1 by FUNCT_2:def 1; then
A6: (ex f being Function st h = f & dom f = Omega & rng f c= REAL) &
dom v1 /\ dom u1 = Omega /\ Omega by FUNCT_2:def 1,def 2;
for x be object st x in dom h
holds h.x = v1.x *(u1.x qua Complex) by A5,A4,FUNCSDOM:2;
then v*u=v1(#)u1 by A6,VALUED_1:def 4;
hence thesis;
end;
for v,u be Element of V st v in W & u in W holds v + u in W
proof
let v,u be Element of V such that
A7: v in W and
A8: u in W;
consider u1 be Real-Valued-Random-Variable of Sigma such that
A9: u1=u by A8;
reconsider h = v+u as Element of Funcs(Omega,REAL);
consider v1 be Real-Valued-Random-Variable of Sigma such that
A10: v1=v by A7;
dom v1 /\ dom u1 = Omega /\ dom u1 by FUNCT_2:def 1;
then
A11: (ex f being Function st h = f & dom f = Omega & rng f c= REAL)&
dom v1 /\ dom u1 = Omega /\ Omega by FUNCT_2:def 1,def 2;
for x be object st x in dom h
holds h.x = v1.x + (u1.x qua Real) by A10,A9,FUNCSDOM:1;
then v+u=v1+u1 by A11,VALUED_1:def 1;
hence thesis;
end; then
A12: W is add-closed by IDEAL_1:def 1;
A13: RAlgebra Omega is RealLinearSpace by C0SP1:7;
for v be Element of V st v in W holds -v in W
proof
let v be Element of V;
assume v in W; then
consider v1 be Real-Valued-Random-Variable of Sigma such that
A14: v1=v;
A15: (-v1) is Real-Valued-Random-Variable of Sigma by RANDOM_1:20;
reconsider h = -v as Element of Funcs(Omega,REAL);
A16: h=(-1)*v by A13,RLVECT_1:16;
A17: now let x be object;
assume x in dom h;
then reconsider y=x as Element of Omega;
thus h.x = (-1)*(v1.y) by A16,A14,FUNCSDOM:4
.= -(v1.x qua Real);
end;
(ex f being Function st h = f & dom f = Omega & rng f c= REAL)
& dom v1 = Omega by FUNCT_2:def 1,def 2;
then -v=-v1 by A17,VALUED_1:9;
hence thesis by A15;
end; then
A18: W is having-inverse by C0SP1:def 1;
for a be Real, u be Element of V st u in W holds a * u in W
proof
let a be Real, u be Element of V;
assume u in W; then
consider u1 be Real-Valued-Random-Variable of Sigma such that
A19: u1=u;
reconsider h = a*u as Element of Funcs(Omega,REAL);
A20: (ex f being Function st h = f & dom f = Omega
& rng f c= REAL) & dom u1 = Omega by FUNCT_2:def 1,def 2;
for x be object st x in dom h holds h.x = a*(u1.x) by A19,FUNCSDOM:4;
then a*u=a(#)u1 by A20,VALUED_1:def 5;
hence thesis;
end;
hence Real-Valued-Random-Variables-Set Sigma
is additively-linearly-closed by A12,A18,C0SP1:def 10;
reconsider g = RealFuncUnit Omega as Function of Omega,REAL;
g is Real-Valued-Random-Variable of Sigma by Th4;
then 1.V in W;
hence thesis by A1,C0SP1:def 4;
end;
registration let Omega,Sigma;
cluster Real-Valued-Random-Variables-Set Sigma
-> additively-linearly-closed multiplicatively-closed;
coherence by Lm10;
end;
definition
let Omega,Sigma;
func R_Algebra_of_Real-Valued-Random-Variables Sigma -> Algebra equals
AlgebraStr (# Real-Valued-Random-Variables-Set Sigma,
mult_(Real-Valued-Random-Variables-Set Sigma,RAlgebra Omega),
Add_(Real-Valued-Random-Variables-Set Sigma,RAlgebra Omega),
Mult_(Real-Valued-Random-Variables-Set Sigma,RAlgebra Omega),
One_(Real-Valued-Random-Variables-Set Sigma,RAlgebra Omega),
Zero_(Real-Valued-Random-Variables-Set Sigma,RAlgebra Omega) #);
coherence by C0SP1:6;
end;
registration let Omega, Sigma;
cluster R_Algebra_of_Real-Valued-Random-Variables Sigma -> scalar-unital;
coherence
proof
let v be VECTOR of R_Algebra_of_Real-Valued-Random-Variables Sigma;
reconsider v1=v as VECTOR of RAlgebra Omega by TARSKI:def 3;
R_Algebra_of_Real-Valued-Random-Variables
Sigma is Subalgebra of RAlgebra Omega by C0SP1:6;
then 1 * v = 1*v1 by C0SP1:8;
hence 1 * v = v by FUNCSDOM:12;
end;
end;