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

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

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

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;
let n be Nat; :: thesis: (Prob * A) . n >= 0

A4: n in NAT by ORDINAL1:def 12;

dom (Prob * A) = NAT by FUNCT_2:def 1;

then (Prob * A) . n = Prob . (A . n) by FUNCT_1:12, A4;

hence (Prob * A) . n >= 0 by PROB_1:def 8; :: thesis: verum

end;A4: n in NAT by ORDINAL1:def 12;

dom (Prob * A) = NAT by FUNCT_2:def 1;

then (Prob * A) . n = Prob . (A . n) by FUNCT_1:12, A4;

hence (Prob * A) . n >= 0 by PROB_1:def 8; :: thesis: verum

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