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;
A10:
(Partial_Sums (Prob * (A ^\ s))) . 0 = (Prob * (A ^\ s)) . 0
by SERIES_1:def 1;
A11:
dom (Prob * (A ^\ s)) = NAT
by FUNCT_2:def 1;
A12:
(Prob * (A ^\ s)) . 0 = Prob . ((A ^\ s) . 0)
by A11, FUNCT_1:12;
A13:
Prob . ((Partial_Union (A ^\ s)) . 0) = Prob . ((A ^\ s) . 0)
by PROB_3:def 2;
A14:
dom (Prob * (Partial_Union (A ^\ s))) = NAT
by FUNCT_2:def 1;
A15:
S1[
0 ]
by A14, A13, A12, A10, FUNCT_1:12;
A16:
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 A17:
(Prob * (Partial_Union (A ^\ s))) . k <= (Partial_Sums (Prob * (A ^\ s))) . k
;
S1[k + 1]
A18:
dom (Prob * (Partial_Union (A ^\ s))) = NAT
by FUNCT_2:def 1;
A20:
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 A21:
(Prob * (A ^\ s)) . (k + 1) = Prob . ((A ^\ s) . (k + 1))
by FUNCT_1:12;
A22:
(
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;
A23:
(
(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;
A24:
(
(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;
A25:
Prob . ((Partial_Union (A ^\ s)) . (k + 1)) <= (Partial_Sums (Prob * (A ^\ s))) . (k + 1)
by A20, A21, A22, A18, A17, A23, A24, 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 A25, FUNCT_1:12;
verum
end;
for
k being
Element of
NAT holds
S1[
k]
from NAT_1:sch 1(A15, A16);
hence
(Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . n
;
verum
end;
A26:
for k being Element of NAT holds Partial_Sums ((Prob * A) ^\ k) is convergent
A27:
for A being SetSequence of Sigma
for n being Element of NAT holds Prob * (A ^\ n) = (Prob * A) ^\ n
A30:
for n being Element of NAT holds Partial_Sums (Prob * (A ^\ n)) is convergent
A31:
for n being Element of NAT holds lim (Prob * (Partial_Union (A ^\ n))) <= lim (Partial_Sums (Prob * (A ^\ n)))
A34:
for n being Element of NAT holds Prob . (Union (A ^\ n)) <= lim (Partial_Sums (Prob * (A ^\ n)))
A35:
for n being Element of NAT holds Prob . (Union (A ^\ n)) <= Sum (Prob * (A ^\ n))
A36:
for n being Element of NAT holds (Prob * (Union_Shift_Seq A)) . n <= (Sum_Shift_Seq (Prob,A)) . n
A40:
0 <= lim (Prob * (Partial_Intersection (Union_Shift_Seq A)))
by A7, A3, SEQ_2:17;
A41:
( Sum_Shift_Seq (Prob,A) is convergent implies lim (Prob * (Partial_Intersection (Union_Shift_Seq A))) <= lim (Sum_Shift_Seq (Prob,A)) )
A50:
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 A51:
Partial_Sums (Prob * A) is
convergent
;
( 0 = lim (Sum_Shift_Seq (Prob,A)) & Sum_Shift_Seq (Prob,A) is convergent )
then A52:
Prob * A is
summable
by SERIES_1:def 2;
A53:
for
n being
Element of
NAT holds
(Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (Partial_Sums (Prob * A)) . n
A54:
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))
A55:
((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n) = ((Partial_Sums (Prob * A)) . m) - ((Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))))
by A53;
A56:
((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 A53, A55;
A57:
((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n) = (Sum ((Prob * A) ^\ (n + 1))) - (Sum ((Prob * A) ^\ (m + 1)))
by A56;
A58:
for
A being
SetSequence of
Sigma for
n being
Element of
NAT holds
Prob * (A ^\ n) = (Prob * A) ^\ n
A61:
for
n being
Element of
NAT holds
((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = Sum ((Prob * A) ^\ (n + 1))
A64:
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 A65:
- 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 A65, 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 A64;
verum
end;
A67:
( ( 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 A68:
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 A69:
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 A70:
for
m being
Element of
NAT st
n <= m holds
abs (((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)) < sr
by A68, A69;
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 A71:
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 A71, A54;
hence
abs ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)) < sr
by A70, A71;
verum
end;
A72:
(
Partial_Sums (Prob * A) is
convergent &
(Sum_Shift_Seq (Prob,A)) ^\ 1 is
convergent )
by A51, A67, SEQ_4:41;
A73:
dom (((Sum_Shift_Seq (Prob,A)) ^\ 1) + (Partial_Sums (Prob * A))) = NAT
by FUNCT_2:def 1;
consider B being
Real_Sequence such that A74:
B = ((Sum_Shift_Seq (Prob,A)) ^\ 1) + (Partial_Sums (Prob * A))
;
set B1 =
NAT --> (Sum (Prob * A));
A75:
Prob * A is
summable
by A51, SERIES_1:def 2;
A76:
for
n being
Element of
NAT holds
(NAT --> (Sum (Prob * A))) . n = B . n
A83:
lim (NAT --> (Sum (Prob * A))) = lim B
A84:
Sum (Prob * A) =
(NAT --> (Sum (Prob * A))) . 1
by FUNCOP_1:7
.=
lim B
by A83, SEQ_4:26
;
A85:
lim B = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (lim (Partial_Sums (Prob * A)))
by A74, A72, SEQ_2:6;
Sum (Prob * A) = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (Sum (Prob * A))
by A84, A85, SERIES_1:def 3;
hence
(
0 = lim (Sum_Shift_Seq (Prob,A)) &
Sum_Shift_Seq (
Prob,
A) is
convergent )
by A72, SEQ_4:21, SEQ_4:22;
verum
end;
( lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )
by A1, A50;
hence
( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )
by A5, A7, A40, A41, PROB_2:def 1; verum