let Omega be non empty set ; for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds
( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )
let Sigma be SigmaField of Omega; for Prob being Probability of Sigma
for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds
( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )
let Prob be Probability of Sigma; for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds
( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )
let A be SetSequence of Sigma; ( Partial_Sums (Prob * A) is convergent implies ( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) )
assume A1:
Partial_Sums (Prob * A) is convergent
; ( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )
A2:
Prob * A is summable
by A1, SERIES_1:def 2;
A3:
for n being Element of NAT holds 0 <= (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n
A5:
Intersection (Partial_Intersection (Union_Shift_Seq A)) = Intersection (Union_Shift_Seq A)
by PROB_3:29;
A6:
Partial_Intersection (Union_Shift_Seq A) is non-ascending
by PROB_3:27;
A7:
( lim (Prob * (Partial_Intersection (Union_Shift_Seq A))) = Prob . (Intersection (Partial_Intersection (Union_Shift_Seq A))) & Prob * (Partial_Intersection (Union_Shift_Seq A)) is convergent )
by A6, PROB_1:def 8;
A8:
for A being SetSequence of Sigma
for n, s being Element of NAT holds (Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . n
proof
let A be
SetSequence of
Sigma;
for n, s being Element of NAT holds (Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . nlet n,
s be
Element of
NAT ;
(Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . n
defpred S1[
set ]
means (Prob * (Partial_Union (A ^\ s))) . $1
<= (Partial_Sums (Prob * (A ^\ s))) . $1;
A9:
(Partial_Sums (Prob * (A ^\ s))) . 0 = (Prob * (A ^\ s)) . 0
by SERIES_1:def 1;
A10:
dom (Prob * (A ^\ s)) = NAT
by FUNCT_2:def 1;
A11:
(Prob * (A ^\ s)) . 0 = Prob . ((A ^\ s) . 0)
by A10, FUNCT_1:12;
A12:
Prob . ((Partial_Union (A ^\ s)) . 0) = Prob . ((A ^\ s) . 0)
by PROB_3:def 2;
A13:
dom (Prob * (Partial_Union (A ^\ s))) = NAT
by FUNCT_2:def 1;
A14:
S1[
0 ]
by A13, A12, A11, A9, FUNCT_1:12;
A15:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A16:
(Prob * (Partial_Union (A ^\ s))) . k <= (Partial_Sums (Prob * (A ^\ s))) . k
;
S1[k + 1]
A17:
dom (Prob * (Partial_Union (A ^\ s))) = NAT
by FUNCT_2:def 1;
A18:
Prob . (((Partial_Union (A ^\ s)) . k) \/ ((A ^\ s) . (k + 1))) <= (Prob . ((Partial_Union (A ^\ s)) . k)) + (Prob . ((A ^\ s) . (k + 1)))
by PROB_1:39;
dom (Prob * (A ^\ s)) = NAT
by FUNCT_2:def 1;
then A19:
(Prob * (A ^\ s)) . (k + 1) = Prob . ((A ^\ s) . (k + 1))
by FUNCT_1:12;
A20:
(
Prob . ((Partial_Union (A ^\ s)) . (k + 1)) <= (Prob . ((Partial_Union (A ^\ s)) . k)) + ((Prob * (A ^\ s)) . (k + 1)) implies
(Prob . ((Partial_Union (A ^\ s)) . (k + 1))) - (Prob . ((Partial_Union (A ^\ s)) . k)) <= (Prob * (A ^\ s)) . (k + 1) )
by XREAL_1:20;
A21:
(
(Prob . ((Partial_Union (A ^\ s)) . (k + 1))) - ((Prob * (A ^\ s)) . (k + 1)) <= Prob . ((Partial_Union (A ^\ s)) . k) &
Prob . ((Partial_Union (A ^\ s)) . k) <= (Partial_Sums (Prob * (A ^\ s))) . k implies
(Prob . ((Partial_Union (A ^\ s)) . (k + 1))) - ((Prob * (A ^\ s)) . (k + 1)) <= (Partial_Sums (Prob * (A ^\ s))) . k )
by XXREAL_0:2;
A22:
(
(Prob . ((Partial_Union (A ^\ s)) . (k + 1))) - ((Prob * (A ^\ s)) . (k + 1)) <= (Partial_Sums (Prob * (A ^\ s))) . k implies
Prob . ((Partial_Union (A ^\ s)) . (k + 1)) <= ((Partial_Sums (Prob * (A ^\ s))) . k) + ((Prob * (A ^\ s)) . (k + 1)) )
by XREAL_1:20;
A23:
Prob . ((Partial_Union (A ^\ s)) . (k + 1)) <= (Partial_Sums (Prob * (A ^\ s))) . (k + 1)
by A18, A19, A20, A17, A16, A21, A22, FUNCT_1:12, PROB_3:def 2, SERIES_1:def 1, XREAL_1:12;
dom (Prob * (Partial_Union (A ^\ s))) = NAT
by FUNCT_2:def 1;
hence
S1[
k + 1]
by A23, FUNCT_1:12;
verum
end;
for
k being
Element of
NAT holds
S1[
k]
from NAT_1:sch 1(A14, A15);
hence
(Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . n
;
verum
end;
A24:
for k being Element of NAT holds Partial_Sums ((Prob * A) ^\ k) is convergent
A25:
for A being SetSequence of Sigma
for n being Element of NAT holds Prob * (A ^\ n) = (Prob * A) ^\ n
A28:
for n being Element of NAT holds Partial_Sums (Prob * (A ^\ n)) is convergent
A29:
for n being Element of NAT holds lim (Prob * (Partial_Union (A ^\ n))) <= lim (Partial_Sums (Prob * (A ^\ n)))
A32:
for n being Element of NAT holds Prob . (Union (A ^\ n)) <= lim (Partial_Sums (Prob * (A ^\ n)))
A33:
for n being Element of NAT holds Prob . (Union (A ^\ n)) <= Sum (Prob * (A ^\ n))
A34:
for n being Element of NAT holds (Prob * (Union_Shift_Seq A)) . n <= (Sum_Shift_Seq (Prob,A)) . n
A38:
0 <= lim (Prob * (Partial_Intersection (Union_Shift_Seq A)))
by A7, A3, SEQ_2:17;
A39:
( Sum_Shift_Seq (Prob,A) is convergent implies lim (Prob * (Partial_Intersection (Union_Shift_Seq A))) <= lim (Sum_Shift_Seq (Prob,A)) )
A48:
for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds
( 0 = lim (Sum_Shift_Seq (Prob,A)) & Sum_Shift_Seq (Prob,A) is convergent )
proof
let A be
SetSequence of
Sigma;
( Partial_Sums (Prob * A) is convergent implies ( 0 = lim (Sum_Shift_Seq (Prob,A)) & Sum_Shift_Seq (Prob,A) is convergent ) )
assume A49:
Partial_Sums (Prob * A) is
convergent
;
( 0 = lim (Sum_Shift_Seq (Prob,A)) & Sum_Shift_Seq (Prob,A) is convergent )
then A50:
Prob * A is
summable
by SERIES_1:def 2;
A51:
for
n being
Element of
NAT holds
(Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (Partial_Sums (Prob * A)) . n
A52:
for
n,
m being
Element of
NAT st
n <= m holds
abs (((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)) = abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n))
proof
let n,
m be
Element of
NAT ;
( n <= m implies abs (((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)) = abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)) )
assume
n <= m
;
abs (((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)) = abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n))
A53:
((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n) = ((Partial_Sums (Prob * A)) . m) - ((Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))))
by A51;
A54:
((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n) = ((Sum (Prob * A)) - (Sum ((Prob * A) ^\ (m + 1)))) - ((Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))))
by A51, A53;
A55:
((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n) = (Sum ((Prob * A) ^\ (n + 1))) - (Sum ((Prob * A) ^\ (m + 1)))
by A54;
A56:
for
A being
SetSequence of
Sigma for
n being
Element of
NAT holds
Prob * (A ^\ n) = (Prob * A) ^\ n
A59:
for
n being
Element of
NAT holds
((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = Sum ((Prob * A) ^\ (n + 1))
A61:
abs (((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)) = abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m))
abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)) = abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n))
proof
per cases
( (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) = 0 or 0 < (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) or (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) < 0 )
;
suppose
0 < (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)
;
abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)) = abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n))then A62:
- 0 > - ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m))
;
abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)) = - ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n))
by A62, ABSVALUE:def 1;
hence
abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)) = abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n))
;
verum end;
end;
hence
abs (((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)) = abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n))
by A61;
verum
end;
A64:
( ( for
sr being
real number st
0 < sr holds
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
abs (((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)) < sr ) implies for
sr being
real number st
0 < sr holds
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)) < sr )
proof
assume A65:
for
sr being
real number st
0 < sr holds
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
abs (((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)) < sr
;
for sr being real number st 0 < sr holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)) < sr
let sr be
real number ;
( 0 < sr implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)) < sr )
assume A66:
0 < sr
;
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)) < sr
consider n being
Element of
NAT such that A67:
for
m being
Element of
NAT st
n <= m holds
abs (((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)) < sr
by A65, A66;
take
n
;
for m being Element of NAT st n <= m holds
abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)) < sr
let m be
Element of
NAT ;
( n <= m implies abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)) < sr )
assume A68:
n <= m
;
abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)) < sr
abs (((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)) = abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n))
by A68, A52;
hence
abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)) < sr
by A67, A68;
verum
end;
A69:
(
Partial_Sums (Prob * A) is
convergent &
(Sum_Shift_Seq (Prob,A)) ^\ 1 is
convergent )
by A49, A64, SEQ_4:41;
A70:
dom (((Sum_Shift_Seq (Prob,A)) ^\ 1) + (Partial_Sums (Prob * A))) = NAT
by FUNCT_2:def 1;
consider B being
Real_Sequence such that A71:
B = ((Sum_Shift_Seq (Prob,A)) ^\ 1) + (Partial_Sums (Prob * A))
;
set B1 =
NAT --> (Sum (Prob * A));
A72:
Prob * A is
summable
by A49, SERIES_1:def 2;
A73:
for
n being
Element of
NAT holds
(NAT --> (Sum (Prob * A))) . n = B . n
A80:
lim (NAT --> (Sum (Prob * A))) = lim B
A81:
Sum (Prob * A) =
(NAT --> (Sum (Prob * A))) . 1
by FUNCOP_1:7
.=
lim B
by A80, SEQ_4:26
;
A82:
lim B = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (lim (Partial_Sums (Prob * A)))
by A71, A69, SEQ_2:6;
Sum (Prob * A) = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (Sum (Prob * A))
by A81, A82, SERIES_1:def 3;
hence
(
0 = lim (Sum_Shift_Seq (Prob,A)) &
Sum_Shift_Seq (
Prob,
A) is
convergent )
by A69, SEQ_4:21, SEQ_4:22;
verum
end;
( lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )
by A1, A48;
hence
( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )
by A5, A7, A38, A39, PROB_2:def 1; verum