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 )
then A2:
Prob * A is summable
by SERIES_1:def 2;
A3:
for n being Nat holds 0 <= (Prob * (Partial_Intersection (superior_setsequence A))) . n
A5:
Intersection (Partial_Intersection (superior_setsequence A)) = Intersection (superior_setsequence A)
by PROB_3:29;
Partial_Intersection (superior_setsequence A) is non-ascending
by PROB_3:27;
then A7:
( lim (Prob * (Partial_Intersection (superior_setsequence A))) = Prob . (Intersection (Partial_Intersection (superior_setsequence A))) & Prob * (Partial_Intersection (superior_setsequence A)) is convergent )
by PROB_1:def 8;
A8:
for A being SetSequence of Sigma
for n, s being 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 Nat holds (Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . nlet n,
s be
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;
dom (Prob * (A ^\ s)) = NAT
by FUNCT_2:def 1;
then A11:
(Prob * (A ^\ s)) . 0 = Prob . ((A ^\ s) . 0)
by FUNCT_1:12;
A12:
Prob . ((Partial_Union (A ^\ s)) . 0) = Prob . ((A ^\ s) . 0)
by PROB_3:def 2;
dom (Prob * (Partial_Union (A ^\ s))) = NAT
by FUNCT_2:def 1;
then A14:
S1[
0 ]
by A12, A11, A9, FUNCT_1:12;
A15:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
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, ORDINAL1:def 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
Nat holds
S1[
k]
from NAT_1:sch 2(A14, A15);
hence
(Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . n
;
verum
end;
A24:
for k being Nat holds Partial_Sums ((Prob * A) ^\ k) is convergent
A25:
for A being SetSequence of Sigma
for n being Nat holds Prob * (A ^\ n) = (Prob * A) ^\ n
A28:
for n being Nat holds Partial_Sums (Prob * (A ^\ n)) is convergent
A29:
for n being Nat holds lim (Prob * (Partial_Union (A ^\ n))) <= lim (Partial_Sums (Prob * (A ^\ n)))
A32:
for n being Nat holds Prob . (Union (A ^\ n)) <= lim (Partial_Sums (Prob * (A ^\ n)))
A33:
for n being Nat holds Prob . (Union (A ^\ n)) <= Sum (Prob * (A ^\ n))
A34:
for n being Nat holds (Prob * (superior_setsequence A)) . n <= (Sum_Shift_Seq (Prob,A)) . n
A38:
0 <= lim (Prob * (Partial_Intersection (superior_setsequence A)))
by A7, A3, SEQ_2:17;
A39:
( Sum_Shift_Seq (Prob,A) is convergent implies lim (Prob * (Partial_Intersection (superior_setsequence A))) <= lim (Sum_Shift_Seq (Prob,A)) )
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 A50:
Partial_Sums (Prob * A) is
convergent
;
( 0 = lim (Sum_Shift_Seq (Prob,A)) & Sum_Shift_Seq (Prob,A) is convergent )
A52:
for
n being
Nat holds
(Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (Partial_Sums (Prob * A)) . n
A53:
for
n,
m being
Nat holds
|.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).|
proof
let n,
m be
Nat;
|.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).|
A54:
((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n) = ((Partial_Sums (Prob * A)) . m) - ((Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))))
by A52;
((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 A52, A54;
then A56:
((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n) = (Sum ((Prob * A) ^\ (n + 1))) - (Sum ((Prob * A) ^\ (m + 1)))
;
A57:
for
A being
SetSequence of
Sigma for
n being
Element of
NAT holds
Prob * (A ^\ n) = (Prob * A) ^\ n
A60:
for
n being
Nat holds
((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = Sum ((Prob * A) ^\ (n + 1))
A62:
|.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((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) . 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)
;
|.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).|then A63:
- 0 > - ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m))
;
|.((((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 A63, ABSVALUE:def 1;
hence
|.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).|
;
verum end; end;
end;
hence
|.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).|
by A62;
verum
end;
A65:
( ( for
sr being
Real st
0 < sr holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| < sr ) implies for
sr being
Real st
0 < sr holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr )
proof
assume A66:
for
sr being
Real st
0 < sr holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| < sr
;
for sr being Real st 0 < sr holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr
let sr be
Real;
( 0 < sr implies ex n being Nat st
for m being Nat st n <= m holds
|.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr )
assume A67:
0 < sr
;
ex n being Nat st
for m being Nat st n <= m holds
|.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr
consider n being
Nat such that A68:
for
m being
Nat st
n <= m holds
|.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| < sr
by A66, A67;
take
n
;
for m being Nat st n <= m holds
|.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr
let m be
Nat;
( n <= m implies |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr )
assume A69:
n <= m
;
|.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr
|.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).|
by A53;
hence
|.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr
by A68, A69;
verum
end;
A70:
(
Partial_Sums (Prob * A) is
convergent &
(Sum_Shift_Seq (Prob,A)) ^\ 1 is
convergent )
by A50, A65, SEQ_4:41;
A71:
dom (((Sum_Shift_Seq (Prob,A)) ^\ 1) + (Partial_Sums (Prob * A))) = NAT
by FUNCT_2:def 1;
consider B being
Real_Sequence such that A72:
B = ((Sum_Shift_Seq (Prob,A)) ^\ 1) + (Partial_Sums (Prob * A))
;
reconsider SP =
Sum (Prob * A) as
Element of
REAL by XREAL_0:def 1;
set B1 =
NAT --> SP;
A74:
for
n being
Nat holds
(NAT --> SP) . n = B . n
proof
let n be
Nat;
(NAT --> SP) . n = B . n
A75:
for
n being
Nat holds
((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = Sum ((Prob * A) ^\ (n + 1))
A81:
((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = Sum ((Prob * A) ^\ (n + 1))
by A75;
Sum (Prob * A) = ((Partial_Sums (Prob * A)) . n) + (Sum ((Prob * A) ^\ (n + 1)))
by A50, SERIES_1:15, SERIES_1:def 2;
then
(NAT --> SP) . n = ((Partial_Sums (Prob * A)) . n) + (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)
by A81, FUNCOP_1:7, ORDINAL1:def 12;
hence
(NAT --> SP) . n = B . n
by A71, A72, VALUED_1:def 1, ORDINAL1:def 12;
verum
end;
A82:
lim (NAT --> SP) = lim B
A83:
Sum (Prob * A) =
(NAT --> SP) . 1
.=
lim B
by A82, SEQ_4:26
;
lim B = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (lim (Partial_Sums (Prob * A)))
by A72, A70, SEQ_2:6;
then
Sum (Prob * A) = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (Sum (Prob * A))
by A83, SERIES_1:def 3;
hence
(
0 = lim (Sum_Shift_Seq (Prob,A)) &
Sum_Shift_Seq (
Prob,
A) is
convergent )
by A70, SEQ_4:21, SEQ_4:22;
verum
end;
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, A1; verum