let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma st not Partial_Sums (Prob * A) is convergent & A is_all_independent_wrt Prob holds
( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 )
let Sigma be SigmaField of Omega; :: thesis: for Prob being Probability of Sigma
for A being SetSequence of Sigma st not Partial_Sums (Prob * A) is convergent & A is_all_independent_wrt Prob holds
( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 )
let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma st not Partial_Sums (Prob * A) is convergent & A is_all_independent_wrt Prob holds
( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 )
let A be SetSequence of Sigma; :: thesis: ( not Partial_Sums (Prob * A) is convergent & A is_all_independent_wrt Prob implies ( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 ) )
assume A1: not Partial_Sums (Prob * A) is convergent ; :: thesis: ( not A is_all_independent_wrt Prob or ( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 ) )
assume A2: A is_all_independent_wrt Prob ; :: thesis: ( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 )
A3: for n being Nat holds (Prob * A) . n >= 0
proof
let n be Nat; :: thesis: (Prob * A) . n >= 0
dom (Prob * A) = NAT by FUNCT_2:def 1;
then (Prob * A) . n = Prob . (A . n) by FUNCT_1:12, ORDINAL1:def 12;
hence (Prob * A) . n >= 0 by PROB_1:def 8; :: thesis: verum
end;
A5: ( ( not Prob * A is summable implies not Partial_Sums (Prob * A) is bounded_above ) & not Prob * A is summable ) by A3, A1, SERIES_1:17, SERIES_1:def 2;
Partial_Sums (Prob * A) is divergent_to+infty by A5, A3, LIMFUNC1:29, SERIES_1:16;
hence ( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 ) by A2, Th16; :: thesis: verum