let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma
for b being Element of B
for f being SetSequence of st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is disjoint_valued holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for B being non empty Subset of Sigma
for b being Element of B
for f being SetSequence of st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is disjoint_valued holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let P be Probability of Sigma; :: thesis: for B being non empty Subset of Sigma
for b being Element of B
for f being SetSequence of st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is disjoint_valued holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let B be non empty Subset of Sigma; :: thesis: for b being Element of B
for f being SetSequence of st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is disjoint_valued holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let b be Element of B; :: thesis: for f being SetSequence of st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is disjoint_valued holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let f be SetSequence of ; :: thesis: ( ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is disjoint_valued implies P . (b /\ (Union f)) = (P . b) * (P . (Union f)) )
assume A0: for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ; :: thesis: ( not f is disjoint_valued or P . (b /\ (Union f)) = (P . b) * (P . (Union f)) )
reconsider b = b as Element of Sigma ;
assume A1: f is disjoint_valued ; :: thesis: P . (b /\ (Union f)) = (P . b) * (P . (Union f))
then A2: seqIntersection b,f is disjoint_valued by DYNKIN:12;
A3: for x being set
for n, m being Element of NAT st n <= m & x in (@Partial_Union f) . n holds
x in (@Partial_Union f) . m
proof
let x be set ; :: thesis: for n, m being Element of NAT st n <= m & x in (@Partial_Union f) . n holds
x in (@Partial_Union f) . m
let n, m be Element of NAT ; :: thesis: ( n <= m & x in (@Partial_Union f) . n implies x in (@Partial_Union f) . m )
assume B0: n <= m ; :: thesis: ( not x in (@Partial_Union f) . n or x in (@Partial_Union f) . m )
assume B1: x in (@Partial_Union f) . n ; :: thesis: x in (@Partial_Union f) . m
reconsider Pf = @Partial_Union f as SetSequence of ;
Pf is non-descending by PROB_3:13;
then Pf . n c= Pf . m by B0, PROB_1:def 7;
hence x in (@Partial_Union f) . m by B1; :: thesis: verum
end;
for n, m being Element of NAT st n <= m holds
(seqIntersection b,(@Partial_Union f)) . n c= (seqIntersection b,(@Partial_Union f)) . m
proof
let n, m be Element of NAT ; :: thesis: ( n <= m implies (seqIntersection b,(@Partial_Union f)) . n c= (seqIntersection b,(@Partial_Union f)) . m )
assume B1: n <= m ; :: thesis: (seqIntersection b,(@Partial_Union f)) . n c= (seqIntersection b,(@Partial_Union f)) . m
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (seqIntersection b,(@Partial_Union f)) . n or x in (seqIntersection b,(@Partial_Union f)) . m )
assume x in (seqIntersection b,(@Partial_Union f)) . n ; :: thesis: x in (seqIntersection b,(@Partial_Union f)) . m
then x in b /\ ((@Partial_Union f) . n) by DYNKIN:def 2;
then ( x in b & x in (@Partial_Union f) . n ) by XBOOLE_0:def 4;
then ( x in b & x in (@Partial_Union f) . m ) by B1, A3;
then x in b /\ ((@Partial_Union f) . m) by XBOOLE_0:def 4;
hence x in (seqIntersection b,(@Partial_Union f)) . m by DYNKIN:def 2; :: thesis: verum
end;
then A4: seqIntersection b,(@Partial_Union f) is non-descending by PROB_1:def 7;
for n being Element of NAT holds (seqIntersection b,f) . n is Event of Sigma
proof
let n be Element of NAT ; :: thesis: (seqIntersection b,f) . n is Event of Sigma
b /\ (f . n) is Event of Sigma ;
hence (seqIntersection b,f) . n is Event of Sigma by DYNKIN:def 2; :: thesis: verum
end;
then reconsider seqIntf = seqIntersection b,f as SetSequence of by PROB_1:57;
reconsider r = P . b as real number ;
A5: P * seqIntf = r (#) (P * f)
proof
now
let n be Element of NAT ; :: thesis: (P * seqIntf) . n = (r (#) (P * f)) . n
thus (P * seqIntf) . n = P . (seqIntf . n) by FUNCT_2:21
.= P . ((f . n) /\ b) by DYNKIN:def 2
.= (P . (f . n)) * (P . b) by A0
.= ((P * f) . n) * r by FUNCT_2:21
.= (r (#) (P * f)) . n by SEQ_1:13 ; :: thesis: verum
end;
hence P * seqIntf = r (#) (P * f) by FUNCT_2:113; :: thesis: verum
end;
for n being Element of NAT holds (@Partial_Union seqIntf) . n = (seqIntersection b,(@Partial_Union f)) . n
proof
let n be Element of NAT ; :: thesis: (@Partial_Union seqIntf) . n = (seqIntersection b,(@Partial_Union f)) . n
defpred S1[ Nat] means (@Partial_Union seqIntf) . $1 = (seqIntersection b,(@Partial_Union f)) . $1;
(@Partial_Union seqIntf) . 0 = seqIntf . 0 by PROB_3:def 2
.= b /\ (f . 0 ) by DYNKIN:def 2
.= b /\ ((@Partial_Union f) . 0 ) by PROB_3:def 2
.= (seqIntersection b,(@Partial_Union f)) . 0 by DYNKIN:def 2 ;
then B0: S1[ 0 ] ;
B1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume C0: (@Partial_Union seqIntf) . k = (seqIntersection b,(@Partial_Union f)) . k ; :: thesis: S1[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def 13;
(@Partial_Union seqIntf) . (k + 1) = ((@Partial_Union seqIntf) . k) \/ (seqIntf . (k + 1)) by PROB_3:def 2
.= (b /\ ((@Partial_Union f) . k)) \/ (seqIntf . (k + 1)) by C0, DYNKIN:def 2
.= (b /\ ((@Partial_Union f) . k)) \/ (b /\ (f . (k + 1))) by DYNKIN:def 2
.= b /\ (((@Partial_Union f) . k) \/ (f . (k + 1))) by XBOOLE_1:23
.= b /\ ((@Partial_Union f) . (k + 1)) by PROB_3:def 2
.= (seqIntersection b,(@Partial_Union f)) . (k + 1) by DYNKIN:def 2 ;
hence S1[k + 1] ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(B0, B1);
 hence (@Partial_Union seqIntf) . n = (seqIntersection b,(@Partial_Union f)) . n ; :: thesis: verum
end;
then A6: P * (seqIntersection b,(@Partial_Union f)) = P * (@Partial_Union seqIntf) by FUNCT_2:113
.= Partial_Sums (P * seqIntf) by A2, PROB_3:49
.= r (#) (Partial_Sums (P * f)) by A5, SERIES_1:12
.= r (#) (P * (@Partial_Union f)) by A1, PROB_3:49 ;
for n being Element of NAT holds (seqIntersection b,(@Partial_Union f)) . n is Event of Sigma
proof
let n be Element of NAT ; :: thesis: (seqIntersection b,(@Partial_Union f)) . n is Event of Sigma
b /\ ((@Partial_Union f) . n) is Event of Sigma ;
hence (seqIntersection b,(@Partial_Union f)) . n is Event of Sigma by DYNKIN:def 2; :: thesis: verum
end;
then reconsider seqIntPf = seqIntersection b,(@Partial_Union f) as SetSequence of by PROB_1:57;
A7: b /\ (Union f) = b /\ (Union (@Partial_Union f)) by PROB_3:17
.= Union seqIntPf by DYNKIN:13 ;
r * (lim (P * (@Partial_Union f))) = lim (P * seqIntPf) by A6, PROB_3:46, SEQ_2:22
.= P . (b /\ (Union f)) by A7, A4, PROB_2:20 ;
hence P . (b /\ (Union f)) = (P . b) * (P . (Union f)) by PROB_3:46; :: thesis: verum