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 holds

( ( Partial_Sums (Prob * A) is convergent implies ( Prob . (lim_sup A) = 0 & Prob . (lim_inf (Complement A)) = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( 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 holds

( ( Partial_Sums (Prob * A) is convergent implies ( Prob . (lim_sup A) = 0 & Prob . (lim_inf (Complement A)) = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 ) ) )

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma holds

( ( Partial_Sums (Prob * A) is convergent implies ( Prob . (lim_sup A) = 0 & Prob . (lim_inf (Complement A)) = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 ) ) )

let A be SetSequence of Sigma; :: thesis: ( ( Partial_Sums (Prob * A) is convergent implies ( Prob . (lim_sup A) = 0 & Prob . (lim_inf (Complement A)) = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 ) ) )

A1: ( Partial_Sums (Prob * A) is convergent implies Prob . (lim_inf (Complement A)) = 1 )

Prob . (lim_sup A) = 0

( Prob . (lim_inf (Complement B)) = 0 & Prob . (lim_sup B) = 1 )

for Prob being Probability of Sigma

for A being SetSequence of Sigma holds

( ( Partial_Sums (Prob * A) is convergent implies ( Prob . (lim_sup A) = 0 & Prob . (lim_inf (Complement A)) = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( 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 holds

( ( Partial_Sums (Prob * A) is convergent implies ( Prob . (lim_sup A) = 0 & Prob . (lim_inf (Complement A)) = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 ) ) )

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma holds

( ( Partial_Sums (Prob * A) is convergent implies ( Prob . (lim_sup A) = 0 & Prob . (lim_inf (Complement A)) = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 ) ) )

let A be SetSequence of Sigma; :: thesis: ( ( Partial_Sums (Prob * A) is convergent implies ( Prob . (lim_sup A) = 0 & Prob . (lim_inf (Complement A)) = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 ) ) )

A1: ( Partial_Sums (Prob * A) is convergent implies Prob . (lim_inf (Complement A)) = 1 )

proof

A5:
for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds
assume A2:
Partial_Sums (Prob * A) is convergent
; :: thesis: Prob . (lim_inf (Complement A)) = 1

A3: Prob . (lim_inf (Complement A)) = Prob . (@lim_inf (Complement A)) by Th15;

for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds

( Prob . (@lim_inf (Complement A)) = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )

end;A3: Prob . (lim_inf (Complement A)) = Prob . (@lim_inf (Complement A)) by Th15;

for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds

( Prob . (@lim_inf (Complement A)) = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )

proof

hence
Prob . (lim_inf (Complement A)) = 1
by A2, A3; :: thesis: verum
let A be SetSequence of Sigma; :: thesis: ( Partial_Sums (Prob * A) is convergent implies ( Prob . (@lim_inf (Complement A)) = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) )

assume A4: Partial_Sums (Prob * A) is convergent ; :: thesis: ( Prob . (@lim_inf (Complement A)) = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )

( (Prob . (@lim_sup A)) + (Prob . (@lim_inf (Complement A))) = 0 + (Prob . (@lim_inf (Complement A))) & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) by A4, Th13;

hence ( Prob . (@lim_inf (Complement A)) = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) by Th15; :: thesis: verum

end;assume A4: Partial_Sums (Prob * A) is convergent ; :: thesis: ( Prob . (@lim_inf (Complement A)) = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )

( (Prob . (@lim_sup A)) + (Prob . (@lim_inf (Complement A))) = 0 + (Prob . (@lim_inf (Complement A))) & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) by A4, Th13;

hence ( Prob . (@lim_inf (Complement A)) = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) by Th15; :: thesis: verum

Prob . (lim_sup A) = 0

proof

for B being SetSequence of Sigma st B is_all_independent_wrt Prob & Partial_Sums (Prob * B) is divergent_to+infty holds
let A be SetSequence of Sigma; :: thesis: ( Partial_Sums (Prob * A) is convergent implies Prob . (lim_sup A) = 0 )

assume A6: Partial_Sums (Prob * A) is convergent ; :: thesis: Prob . (lim_sup A) = 0

Prob . (lim_sup A) = Prob . (@lim_sup A) by Th15;

hence Prob . (lim_sup A) = 0 by A6, Th13; :: thesis: verum

end;assume A6: Partial_Sums (Prob * A) is convergent ; :: thesis: Prob . (lim_sup A) = 0

Prob . (lim_sup A) = Prob . (@lim_sup A) by Th15;

hence Prob . (lim_sup A) = 0 by A6, Th13; :: thesis: verum

( Prob . (lim_inf (Complement B)) = 0 & Prob . (lim_sup B) = 1 )

proof

hence
( ( Partial_Sums (Prob * A) is convergent implies ( Prob . (lim_sup A) = 0 & Prob . (lim_inf (Complement A)) = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 ) ) )
by A5, A1; :: thesis: verum
let B be SetSequence of Sigma; :: thesis: ( B is_all_independent_wrt Prob & Partial_Sums (Prob * B) is divergent_to+infty implies ( Prob . (lim_inf (Complement B)) = 0 & Prob . (lim_sup B) = 1 ) )

assume that

A7: B is_all_independent_wrt Prob and

A8: Partial_Sums (Prob * B) is divergent_to+infty ; :: thesis: ( Prob . (lim_inf (Complement B)) = 0 & Prob . (lim_sup B) = 1 )

A9: Prob . (@lim_sup B) = Prob . (lim_sup B) by Th15;

A10: Prob . (@lim_inf (Complement B)) = Prob . (lim_inf (Complement B)) by Th15;

for B being SetSequence of Sigma st B is_all_independent_wrt Prob & Partial_Sums (Prob * B) is divergent_to+infty holds

( Prob . (@lim_inf (Complement B)) = 0 & Prob . (@lim_sup B) = 1 )

end;assume that

A7: B is_all_independent_wrt Prob and

A8: Partial_Sums (Prob * B) is divergent_to+infty ; :: thesis: ( Prob . (lim_inf (Complement B)) = 0 & Prob . (lim_sup B) = 1 )

A9: Prob . (@lim_sup B) = Prob . (lim_sup B) by Th15;

A10: Prob . (@lim_inf (Complement B)) = Prob . (lim_inf (Complement B)) by Th15;

for B being SetSequence of Sigma st B is_all_independent_wrt Prob & Partial_Sums (Prob * B) is divergent_to+infty holds

( Prob . (@lim_inf (Complement B)) = 0 & Prob . (@lim_sup B) = 1 )

proof

hence
( Prob . (lim_inf (Complement B)) = 0 & Prob . (lim_sup B) = 1 )
by A9, A10, A7, A8; :: thesis: verum
let B be SetSequence of Sigma; :: thesis: ( B is_all_independent_wrt Prob & Partial_Sums (Prob * B) is divergent_to+infty implies ( Prob . (@lim_inf (Complement B)) = 0 & Prob . (@lim_sup B) = 1 ) )

assume that

A11: B is_all_independent_wrt Prob and

A12: Partial_Sums (Prob * B) is divergent_to+infty ; :: thesis: ( Prob . (@lim_inf (Complement B)) = 0 & Prob . (@lim_sup B) = 1 )

A13: for Q being SetSequence of Sigma holds Intersect_Shift_Seq Q is non-descending

reconsider CB = Complement B as SetSequence of Sigma ;

A15: Prob . (@lim_inf CB) = lim (Prob * (Intersect_Shift_Seq (Complement B))) by A14, PROB_2:10;

A16: for n being Nat holds (Prob * (Intersect_Shift_Seq (Complement B))) . n = 0

A76: ex n being Nat st (seq_const 0) . n = 0 A77: lim (seq_const 0) = 0 by A76, SEQ_4:25;

A78: ( seq_const 0 is convergent & ex k being Nat st

for n being Nat st k <= n holds

(seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n )

hence ( Prob . (@lim_inf (Complement B)) = 0 & Prob . (@lim_sup B) = 1 ) ; :: thesis: verum

end;assume that

A11: B is_all_independent_wrt Prob and

A12: Partial_Sums (Prob * B) is divergent_to+infty ; :: thesis: ( Prob . (@lim_inf (Complement B)) = 0 & Prob . (@lim_sup B) = 1 )

A13: for Q being SetSequence of Sigma holds Intersect_Shift_Seq Q is non-descending

proof

A14:
Intersect_Shift_Seq (Complement B) is non-descending
by A13;
let Q be SetSequence of Sigma; :: thesis: Intersect_Shift_Seq Q is non-descending

inferior_setsequence Q = Intersect_Shift_Seq Q by Th11;

hence Intersect_Shift_Seq Q is non-descending ; :: thesis: verum

end;inferior_setsequence Q = Intersect_Shift_Seq Q by Th11;

hence Intersect_Shift_Seq Q is non-descending ; :: thesis: verum

reconsider CB = Complement B as SetSequence of Sigma ;

A15: Prob . (@lim_inf CB) = lim (Prob * (Intersect_Shift_Seq (Complement B))) by A14, PROB_2:10;

A16: for n being Nat holds (Prob * (Intersect_Shift_Seq (Complement B))) . n = 0

proof

set B2 = seq_const 0;
let n be Nat; :: thesis: (Prob * (Intersect_Shift_Seq (Complement B))) . n = 0

A17: n in NAT by ORDINAL1:def 12;

dom (Prob * (Intersect_Shift_Seq (Complement B))) = NAT by FUNCT_2:def 1;

then A18: (Prob * (Intersect_Shift_Seq (Complement B))) . n = Prob . ((Intersect_Shift_Seq (Complement B)) . n) by FUNCT_1:12, A17;

(Intersect_Shift_Seq (Complement B)) . n = Intersection ((Complement B) ^\ n) by Def9;

then A19: (Prob * (Intersect_Shift_Seq (Complement B))) . n = Prob . (Intersection (Partial_Intersection ((Complement B) ^\ n))) by A18, PROB_3:29;

Partial_Intersection ((Complement B) ^\ n) is non-ascending by PROB_3:27;

then A20: (Prob * (Intersect_Shift_Seq (Complement B))) . n = lim (Prob * (Partial_Intersection ((Complement B) ^\ n))) by A19, PROB_1:def 8;

A21: for k being Nat holds (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") . k

( lim ((1 + (Partial_Sums (Prob * A))) ") = 0 & (1 + (Partial_Sums (Prob * A))) " is convergent )

then A70: ( Prob * (Partial_Intersection (Complement (B ^\ n))) is convergent & (1 + (Partial_Sums (Prob * (B ^\ n)))) " is convergent ) by A42, A63, PROB_1:def 8;

A71: lim ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") = 0 by A42, A63;

A72: for k being Nat holds 0 <= (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k

Complement (B ^\ n) = (Complement B) ^\ n

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

dom (Prob * (Intersect_Shift_Seq (Complement B))) = NAT by FUNCT_2:def 1;

then A18: (Prob * (Intersect_Shift_Seq (Complement B))) . n = Prob . ((Intersect_Shift_Seq (Complement B)) . n) by FUNCT_1:12, A17;

(Intersect_Shift_Seq (Complement B)) . n = Intersection ((Complement B) ^\ n) by Def9;

then A19: (Prob * (Intersect_Shift_Seq (Complement B))) . n = Prob . (Intersection (Partial_Intersection ((Complement B) ^\ n))) by A18, PROB_3:29;

Partial_Intersection ((Complement B) ^\ n) is non-ascending by PROB_3:27;

then A20: (Prob * (Intersect_Shift_Seq (Complement B))) . n = lim (Prob * (Partial_Intersection ((Complement B) ^\ n))) by A19, PROB_1:def 8;

A21: for k being Nat holds (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") . k

proof

A42:
Partial_Sums (Prob * (B ^\ n)) is divergent_to+infty
let k be Nat; :: thesis: (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") . k

A22: for k being Nat holds B ^\ k is_all_independent_wrt Prob

for n being Nat holds (Partial_Product (Prob * (Complement A))) . n <= ((1 + (Partial_Sums (Prob * A))) . n) "

dom (Prob * (Partial_Intersection (Complement (B ^\ n)))) = NAT by FUNCT_2:def 1;

then (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k = Prob . ((Partial_Intersection (Complement (B ^\ n))) . k) by FUNCT_1:12;

then (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k = (Partial_Product (Prob * (Complement (B ^\ n)))) . k by A22, Th10;

then (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) . k) " by A29;

hence (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") . k by VALUED_1:10; :: thesis: verum

end;A22: for k being Nat holds B ^\ k is_all_independent_wrt Prob

proof

A29:
for A being SetSequence of Sigma
let k be Nat; :: thesis: B ^\ k is_all_independent_wrt Prob

for C being SetSequence of Sigma st ex e being sequence of NAT st

( e is one-to-one & ( for n being Nat holds (B ^\ k) . (e . n) = C . n ) ) holds

for n being Nat holds (Partial_Product (Prob * C)) . n = Prob . ((Partial_Intersection C) . n)

end;for C being SetSequence of Sigma st ex e being sequence of NAT st

( e is one-to-one & ( for n being Nat holds (B ^\ k) . (e . n) = C . n ) ) holds

for n being Nat holds (Partial_Product (Prob * C)) . n = Prob . ((Partial_Intersection C) . n)

proof

hence
B ^\ k is_all_independent_wrt Prob
by Def6; :: thesis: verum
let C be SetSequence of Sigma; :: thesis: ( ex e being sequence of NAT st

( e is one-to-one & ( for n being Nat holds (B ^\ k) . (e . n) = C . n ) ) implies for n being Nat holds (Partial_Product (Prob * C)) . n = Prob . ((Partial_Intersection C) . n) )

given e being sequence of NAT such that A23: e is one-to-one and

A24: for n being Nat holds (B ^\ k) . (e . n) = C . n ; :: thesis: for n being Nat holds (Partial_Product (Prob * C)) . n = Prob . ((Partial_Intersection C) . n)

A25: B ^\ k = B * (Special_Function2 k)

hence for n being Nat holds (Partial_Product (Prob * C)) . n = Prob . ((Partial_Intersection C) . n) by A11, A28; :: thesis: verum

end;( e is one-to-one & ( for n being Nat holds (B ^\ k) . (e . n) = C . n ) ) implies for n being Nat holds (Partial_Product (Prob * C)) . n = Prob . ((Partial_Intersection C) . n) )

given e being sequence of NAT such that A23: e is one-to-one and

A24: for n being Nat holds (B ^\ k) . (e . n) = C . n ; :: thesis: for n being Nat holds (Partial_Product (Prob * C)) . n = Prob . ((Partial_Intersection C) . n)

A25: B ^\ k = B * (Special_Function2 k)

proof

A27:
for n being Nat holds (B * (Special_Function2 k)) . (e . n) = B . (((Special_Function2 k) * e) . n)
for n being object st n in NAT holds

(B ^\ k) . n = (B * (Special_Function2 k)) . n

end;(B ^\ k) . n = (B * (Special_Function2 k)) . n

proof

hence
B ^\ k = B * (Special_Function2 k)
; :: thesis: verum
let n be object ; :: thesis: ( n in NAT implies (B ^\ k) . n = (B * (Special_Function2 k)) . n )

assume n in NAT ; :: thesis: (B ^\ k) . n = (B * (Special_Function2 k)) . n

then reconsider n = n as Element of NAT ;

dom (B * (Special_Function2 k)) = NAT by FUNCT_2:def 1;

then A26: (B * (Special_Function2 k)) . n = B . ((Special_Function2 k) . n) by FUNCT_1:12;

(Special_Function2 k) . n = n + k by Def3;

hence (B ^\ k) . n = (B * (Special_Function2 k)) . n by A26, NAT_1:def 3; :: thesis: verum

end;assume n in NAT ; :: thesis: (B ^\ k) . n = (B * (Special_Function2 k)) . n

then reconsider n = n as Element of NAT ;

dom (B * (Special_Function2 k)) = NAT by FUNCT_2:def 1;

then A26: (B * (Special_Function2 k)) . n = B . ((Special_Function2 k) . n) by FUNCT_1:12;

(Special_Function2 k) . n = n + k by Def3;

hence (B ^\ k) . n = (B * (Special_Function2 k)) . n by A26, NAT_1:def 3; :: thesis: verum

proof

A28:
for n being Nat holds B . (((Special_Function2 k) * e) . n) = C . n
let n be Nat; :: thesis: (B * (Special_Function2 k)) . (e . n) = B . (((Special_Function2 k) * e) . n)

reconsider n = n as Element of NAT by ORDINAL1:def 12;

( dom (B * (Special_Function2 k)) = NAT & dom ((Special_Function2 k) * e) = NAT ) by FUNCT_2:def 1;

then ( (B * (Special_Function2 k)) . (e . n) = B . ((Special_Function2 k) . (e . n)) & ((Special_Function2 k) * e) . n = (Special_Function2 k) . (e . n) ) by FUNCT_1:12;

hence (B * (Special_Function2 k)) . (e . n) = B . (((Special_Function2 k) * e) . n) ; :: thesis: verum

end;reconsider n = n as Element of NAT by ORDINAL1:def 12;

( dom (B * (Special_Function2 k)) = NAT & dom ((Special_Function2 k) * e) = NAT ) by FUNCT_2:def 1;

then ( (B * (Special_Function2 k)) . (e . n) = B . ((Special_Function2 k) . (e . n)) & ((Special_Function2 k) * e) . n = (Special_Function2 k) . (e . n) ) by FUNCT_1:12;

hence (B * (Special_Function2 k)) . (e . n) = B . (((Special_Function2 k) * e) . n) ; :: thesis: verum

proof

(Special_Function2 k) * e is one-to-one
by A23, FUNCT_1:24;
let n be Nat; :: thesis: B . (((Special_Function2 k) * e) . n) = C . n

(B * (Special_Function2 k)) . (e . n) = C . n by A25, A24;

hence B . (((Special_Function2 k) * e) . n) = C . n by A27; :: thesis: verum

end;(B * (Special_Function2 k)) . (e . n) = C . n by A25, A24;

hence B . (((Special_Function2 k) * e) . n) = C . n by A27; :: thesis: verum

hence for n being Nat holds (Partial_Product (Prob * C)) . n = Prob . ((Partial_Intersection C) . n) by A11, A28; :: thesis: verum

for n being Nat holds (Partial_Product (Prob * (Complement A))) . n <= ((1 + (Partial_Sums (Prob * A))) . n) "

proof

reconsider k = k as Element of NAT by ORDINAL1:def 12;
let A be SetSequence of Sigma; :: thesis: for n being Nat holds (Partial_Product (Prob * (Complement A))) . n <= ((1 + (Partial_Sums (Prob * A))) . n) "

let n be Nat; :: thesis: (Partial_Product (Prob * (Complement A))) . n <= ((1 + (Partial_Sums (Prob * A))) . n) "

reconsider n = n as Element of NAT by ORDINAL1:def 12;

A30: (Partial_Product (Prob * (Complement A))) . n <= 1 / (1 + ((Partial_Sums (Prob * A)) . n))

for n being Nat holds 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = ((1 + (Partial_Sums (Prob * A))) . n) "

end;let n be Nat; :: thesis: (Partial_Product (Prob * (Complement A))) . n <= ((1 + (Partial_Sums (Prob * A))) . n) "

reconsider n = n as Element of NAT by ORDINAL1:def 12;

A30: (Partial_Product (Prob * (Complement A))) . n <= 1 / (1 + ((Partial_Sums (Prob * A)) . n))

proof

for A being SetSequence of Sigma
(Partial_Product (Prob * (Complement A))) . n <= (Partial_Product (JSum (Prob * A))) . n
by Th4;

then A31: (Partial_Product (Prob * (Complement A))) . n <= exp_R . (- ((Partial_Sums (Prob * A)) . n)) by Th3;

exp_R . (- ((Partial_Sums (Prob * A)) . n)) <= 1 / (1 + ((Partial_Sums (Prob * A)) . n))

end;then A31: (Partial_Product (Prob * (Complement A))) . n <= exp_R . (- ((Partial_Sums (Prob * A)) . n)) by Th3;

exp_R . (- ((Partial_Sums (Prob * A)) . n)) <= 1 / (1 + ((Partial_Sums (Prob * A)) . n))

proof

hence
(Partial_Product (Prob * (Complement A))) . n <= 1 / (1 + ((Partial_Sums (Prob * A)) . n))
by A31, XXREAL_0:2; :: thesis: verum
A32:
for n being Nat holds (Prob * A) . n >= 0

exp_R . (- x) <= 1 / (1 + x)

end;proof

A33:
for n being Nat holds (Partial_Sums (Prob * A)) . n >= 0
let n be Nat; :: thesis: (Prob * A) . n >= 0

reconsider n = n as Element of 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;

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

end;reconsider n = n as Element of 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;

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

proof

for x being Element of REAL st x >= 0 holds
let n be Nat; :: thesis: (Partial_Sums (Prob * A)) . n >= 0

defpred S_{1}[ Nat] means (Partial_Sums (Prob * A)) . $1 >= 0 ;

(Partial_Sums (Prob * A)) . 0 = (Prob * A) . 0 by SERIES_1:def 1;

then A34: S_{1}[ 0 ]
by A32;

A35: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A34, A35);

hence (Partial_Sums (Prob * A)) . n >= 0 ; :: thesis: verum

end;defpred S

(Partial_Sums (Prob * A)) . 0 = (Prob * A) . 0 by SERIES_1:def 1;

then A34: S

A35: for k being Nat st S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A36: S_{1}[k]
; :: thesis: S_{1}[k + 1]

A37: (Prob * A) . (k + 1) >= 0 by A32;

(Partial_Sums (Prob * A)) . (k + 1) = ((Partial_Sums (Prob * A)) . k) + ((Prob * A) . (k + 1)) by SERIES_1:def 1;

hence S_{1}[k + 1]
by A36, A37; :: thesis: verum

end;assume A36: S

A37: (Prob * A) . (k + 1) >= 0 by A32;

(Partial_Sums (Prob * A)) . (k + 1) = ((Partial_Sums (Prob * A)) . k) + ((Prob * A) . (k + 1)) by SERIES_1:def 1;

hence S

hence (Partial_Sums (Prob * A)) . n >= 0 ; :: thesis: verum

exp_R . (- x) <= 1 / (1 + x)

proof

hence
exp_R . (- ((Partial_Sums (Prob * A)) . n)) <= 1 / (1 + ((Partial_Sums (Prob * A)) . n))
by A33; :: thesis: verum
let x be Element of REAL ; :: thesis: ( x >= 0 implies exp_R . (- x) <= 1 / (1 + x) )

assume A38: x >= 0 ; :: thesis: exp_R . (- x) <= 1 / (1 + x)

end;assume A38: x >= 0 ; :: thesis: exp_R . (- x) <= 1 / (1 + x)

per cases
( x > 0 or x <= 0 )
;

end;

suppose A39:
x > 0
; :: thesis: exp_R . (- x) <= 1 / (1 + x)

A40:
exp_R . (- x) >= 0
by SIN_COS:54;

set z = - x;

A41: (exp_R x) * (exp_R (- x)) = exp_R (x + (- x)) by SIN_COS:50;

(exp_R . (- x)) * (1 + x) <= 1 by Th2, A40, A41, SIN_COS:51, XREAL_1:64;

hence exp_R . (- x) <= 1 / (1 + x) by A39, XREAL_1:77; :: thesis: verum

end;set z = - x;

A41: (exp_R x) * (exp_R (- x)) = exp_R (x + (- x)) by SIN_COS:50;

(exp_R . (- x)) * (1 + x) <= 1 by Th2, A40, A41, SIN_COS:51, XREAL_1:64;

hence exp_R . (- x) <= 1 / (1 + x) by A39, XREAL_1:77; :: thesis: verum

for n being Nat holds 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = ((1 + (Partial_Sums (Prob * A))) . n) "

proof

hence
(Partial_Product (Prob * (Complement A))) . n <= ((1 + (Partial_Sums (Prob * A))) . n) "
by A30; :: thesis: verum
let A be SetSequence of Sigma; :: thesis: for n being Nat holds 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = ((1 + (Partial_Sums (Prob * A))) . n) "

let n be Nat; :: thesis: 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = ((1 + (Partial_Sums (Prob * A))) . n) "

n in NAT by ORDINAL1:def 12;

then 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = 1 / ((1 + (Partial_Sums (Prob * A))) . n) by VALUED_1:2;

then 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = 1 * (((1 + (Partial_Sums (Prob * A))) . n) ") by XCMPLX_0:def 9;

hence 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = ((1 + (Partial_Sums (Prob * A))) . n) " ; :: thesis: verum

end;let n be Nat; :: thesis: 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = ((1 + (Partial_Sums (Prob * A))) . n) "

n in NAT by ORDINAL1:def 12;

then 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = 1 / ((1 + (Partial_Sums (Prob * A))) . n) by VALUED_1:2;

then 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = 1 * (((1 + (Partial_Sums (Prob * A))) . n) ") by XCMPLX_0:def 9;

hence 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = ((1 + (Partial_Sums (Prob * A))) . n) " ; :: thesis: verum

dom (Prob * (Partial_Intersection (Complement (B ^\ n)))) = NAT by FUNCT_2:def 1;

then (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k = Prob . ((Partial_Intersection (Complement (B ^\ n))) . k) by FUNCT_1:12;

then (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k = (Partial_Product (Prob * (Complement (B ^\ n)))) . k by A22, Th10;

then (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) . k) " by A29;

hence (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") . k by VALUED_1:10; :: thesis: verum

proof
end;

A63:
for A being SetSequence of Sigma st Partial_Sums (Prob * A) is divergent_to+infty holds per cases
( n = 0 or n <> 0 )
;

end;

suppose
n <> 0
; :: thesis: Partial_Sums (Prob * (B ^\ n)) is divergent_to+infty

then A43:
n - 1 is Nat
by NAT_1:20;

reconsider y = n - 1 as Element of NAT by A43, ORDINAL1:def 12;

set B2 = NAT --> (- ((Partial_Sums (Prob * B)) . y));

A44: (Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y))) is divergent_to+infty by A12, LIMFUNC1:18;

for r being Real ex q being Nat st

for m being Nat st q <= m holds

r < (Partial_Sums (Prob * (B ^\ n))) . m

end;reconsider y = n - 1 as Element of NAT by A43, ORDINAL1:def 12;

set B2 = NAT --> (- ((Partial_Sums (Prob * B)) . y));

A44: (Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y))) is divergent_to+infty by A12, LIMFUNC1:18;

for r being Real ex q being Nat st

for m being Nat st q <= m holds

r < (Partial_Sums (Prob * (B ^\ n))) . m

proof

hence
Partial_Sums (Prob * (B ^\ n)) is divergent_to+infty
by LIMFUNC1:def 4; :: thesis: verum
let r be Real; :: thesis: ex q being Nat st

for m being Nat st q <= m holds

r < (Partial_Sums (Prob * (B ^\ n))) . m

for r being Real ex q being Nat st

for m being Nat st q <= m holds

r < (Partial_Sums (Prob * (B ^\ n))) . m

for m being Nat st q <= m holds

r < (Partial_Sums (Prob * (B ^\ n))) . m ; :: thesis: verum

end;for m being Nat st q <= m holds

r < (Partial_Sums (Prob * (B ^\ n))) . m

for r being Real ex q being Nat st

for m being Nat st q <= m holds

r < (Partial_Sums (Prob * (B ^\ n))) . m

proof

hence
ex q being Nat st
let r be Real; :: thesis: ex q being Nat st

for m being Nat st q <= m holds

r < (Partial_Sums (Prob * (B ^\ n))) . m

A45: for m being Nat st n <= m holds

((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m = (Partial_Sums (Prob * (B ^\ n))) . (m - n)

for m being Nat st q + n <= m + n holds

r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n)

A61: for m being Nat st q + n <= m + n holds

r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) by A59;

take s = q + n; :: thesis: for m being Nat st s <= m holds

r < (Partial_Sums (Prob * (B ^\ n))) . m

let m be Nat; :: thesis: ( s <= m implies r < (Partial_Sums (Prob * (B ^\ n))) . m )

assume A62: s <= m ; :: thesis: r < (Partial_Sums (Prob * (B ^\ n))) . m

set z = m + n;

((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) = (Partial_Sums (Prob * (B ^\ n))) . ((m + n) - n) by A45, NAT_1:12;

hence r < (Partial_Sums (Prob * (B ^\ n))) . m by A62, A61, NAT_1:12; :: thesis: verum

end;for m being Nat st q <= m holds

r < (Partial_Sums (Prob * (B ^\ n))) . m

A45: for m being Nat st n <= m holds

((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m = (Partial_Sums (Prob * (B ^\ n))) . (m - n)

proof

A59:
ex q being Nat st
let m be Nat; :: thesis: ( n <= m implies ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m = (Partial_Sums (Prob * (B ^\ n))) . (m - n) )

assume n <= m ; :: thesis: ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m = (Partial_Sums (Prob * (B ^\ n))) . (m - n)

then consider knat being Nat such that

A46: m = n + knat by NAT_1:10;

reconsider knat = knat as Nat ;

defpred S_{1}[ Nat] means ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (n + $1) = (Partial_Sums (Prob * (B ^\ n))) . ((n + $1) - n);

A47: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A47, A52);

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (n + knat) = (Partial_Sums (Prob * (B ^\ n))) . ((n + knat) - n) ;

hence ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m = (Partial_Sums (Prob * (B ^\ n))) . (m - n) by A46; :: thesis: verum

end;assume n <= m ; :: thesis: ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m = (Partial_Sums (Prob * (B ^\ n))) . (m - n)

then consider knat being Nat such that

A46: m = n + knat by NAT_1:10;

reconsider knat = knat as Nat ;

defpred S

A47: S

proof

A52:
for k being Nat st S
A48:
n in NAT
by ORDINAL1:def 12;

dom ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) = NAT by FUNCT_2:def 1;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = ((Partial_Sums (Prob * B)) . n) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . n) by VALUED_1:def 1, A48;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = ((Partial_Sums (Prob * B)) . n) + (- ((Partial_Sums (Prob * B)) . (n - 1))) by FUNCOP_1:7, A48;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = ((Partial_Sums (Prob * B)) . n) - ((Partial_Sums (Prob * B)) . (n - 1)) ;

then A49: ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = (((Partial_Sums (Prob * B)) . (n - 1)) + ((Prob * B) . ((n - 1) + 1))) - ((Partial_Sums (Prob * B)) . (n - 1)) by SERIES_1:def 1;

dom (Prob * (B ^\ n)) = NAT by FUNCT_2:def 1;

then A50: (Prob * (B ^\ n)) . 0 = Prob . ((B ^\ n) . 0) by FUNCT_1:12;

A51: (B ^\ n) . 0 = B . (0 + n) by NAT_1:def 3;

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

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = (Prob * (B ^\ n)) . 0 by A51, A50, A49, FUNCT_1:12, A48;

hence S_{1}[ 0 ]
by SERIES_1:def 1; :: thesis: verum

end;dom ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) = NAT by FUNCT_2:def 1;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = ((Partial_Sums (Prob * B)) . n) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . n) by VALUED_1:def 1, A48;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = ((Partial_Sums (Prob * B)) . n) + (- ((Partial_Sums (Prob * B)) . (n - 1))) by FUNCOP_1:7, A48;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = ((Partial_Sums (Prob * B)) . n) - ((Partial_Sums (Prob * B)) . (n - 1)) ;

then A49: ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = (((Partial_Sums (Prob * B)) . (n - 1)) + ((Prob * B) . ((n - 1) + 1))) - ((Partial_Sums (Prob * B)) . (n - 1)) by SERIES_1:def 1;

dom (Prob * (B ^\ n)) = NAT by FUNCT_2:def 1;

then A50: (Prob * (B ^\ n)) . 0 = Prob . ((B ^\ n) . 0) by FUNCT_1:12;

A51: (B ^\ n) . 0 = B . (0 + n) by NAT_1:def 3;

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

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = (Prob * (B ^\ n)) . 0 by A51, A50, A49, FUNCT_1:12, A48;

hence S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

A53: n + k in NAT by ORDINAL1:def 12;

assume A54: S_{1}[k]
; :: thesis: S_{1}[k + 1]

A55: dom ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) = NAT by FUNCT_2:def 1;

((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = ((Partial_Sums (Prob * B)) . ((n + k) + 1)) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . ((n + k) + 1)) by A55, VALUED_1:def 1;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = (((Partial_Sums (Prob * B)) . (n + k)) + ((Prob * B) . ((n + k) + 1))) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . ((n + k) + 1)) by SERIES_1:def 1;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = (((Partial_Sums (Prob * B)) . (n + k)) + ((Prob * B) . ((n + k) + 1))) + (- ((Partial_Sums (Prob * B)) . (n - 1))) ;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = (((Partial_Sums (Prob * B)) . (n + k)) + ((Prob * B) . ((n + k) + 1))) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . (n + k)) by FUNCOP_1:7, A53;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = (((Partial_Sums (Prob * B)) . (n + k)) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . (n + k))) + ((Prob * B) . ((n + k) + 1)) ;

then A56: ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = ((Partial_Sums (Prob * (B ^\ n))) . ((n + k) - n)) + ((Prob * B) . ((n + k) + 1)) by A55, A54, VALUED_1:def 1, A53;

(Prob * (B ^\ n)) . (((n + k) - n) + 1) = (Prob * B) . ((n + k) + 1)_{1}[k + 1]
by A56, SERIES_1:def 1; :: thesis: verum

end;A53: n + k in NAT by ORDINAL1:def 12;

assume A54: S

A55: dom ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) = NAT by FUNCT_2:def 1;

((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = ((Partial_Sums (Prob * B)) . ((n + k) + 1)) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . ((n + k) + 1)) by A55, VALUED_1:def 1;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = (((Partial_Sums (Prob * B)) . (n + k)) + ((Prob * B) . ((n + k) + 1))) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . ((n + k) + 1)) by SERIES_1:def 1;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = (((Partial_Sums (Prob * B)) . (n + k)) + ((Prob * B) . ((n + k) + 1))) + (- ((Partial_Sums (Prob * B)) . (n - 1))) ;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = (((Partial_Sums (Prob * B)) . (n + k)) + ((Prob * B) . ((n + k) + 1))) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . (n + k)) by FUNCOP_1:7, A53;

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = (((Partial_Sums (Prob * B)) . (n + k)) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . (n + k))) + ((Prob * B) . ((n + k) + 1)) ;

then A56: ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = ((Partial_Sums (Prob * (B ^\ n))) . ((n + k) - n)) + ((Prob * B) . ((n + k) + 1)) by A55, A54, VALUED_1:def 1, A53;

(Prob * (B ^\ n)) . (((n + k) - n) + 1) = (Prob * B) . ((n + k) + 1)

proof

hence
S
dom (Prob * (B ^\ n)) = NAT
by FUNCT_2:def 1;

then A57: (Prob * (B ^\ n)) . (((n + k) - n) + 1) = Prob . ((B ^\ n) . (k + 1)) by FUNCT_1:12;

A58: (B ^\ n) . (k + 1) = B . (n + (k + 1)) by NAT_1:def 3;

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

hence (Prob * (B ^\ n)) . (((n + k) - n) + 1) = (Prob * B) . ((n + k) + 1) by A58, A57, FUNCT_1:12; :: thesis: verum

end;then A57: (Prob * (B ^\ n)) . (((n + k) - n) + 1) = Prob . ((B ^\ n) . (k + 1)) by FUNCT_1:12;

A58: (B ^\ n) . (k + 1) = B . (n + (k + 1)) by NAT_1:def 3;

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

hence (Prob * (B ^\ n)) . (((n + k) - n) + 1) = (Prob * B) . ((n + k) + 1) by A58, A57, FUNCT_1:12; :: thesis: verum

then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (n + knat) = (Partial_Sums (Prob * (B ^\ n))) . ((n + knat) - n) ;

hence ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m = (Partial_Sums (Prob * (B ^\ n))) . (m - n) by A46; :: thesis: verum

for m being Nat st q + n <= m + n holds

r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n)

proof

consider q being Nat such that
consider q being Nat such that

A60: for m being Nat st q <= m holds

r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m by A44, LIMFUNC1:def 4;

take q ; :: thesis: for m being Nat st q + n <= m + n holds

r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n)

let m be Nat; :: thesis: ( q + n <= m + n implies r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) )

assume q + n <= m + n ; :: thesis: r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n)

then ( q <= q + n & q + n <= m + n ) by NAT_1:11;

then q <= m + n by XXREAL_0:2;

hence r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) by A60; :: thesis: verum

end;A60: for m being Nat st q <= m holds

r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m by A44, LIMFUNC1:def 4;

take q ; :: thesis: for m being Nat st q + n <= m + n holds

r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n)

let m be Nat; :: thesis: ( q + n <= m + n implies r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) )

assume q + n <= m + n ; :: thesis: r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n)

then ( q <= q + n & q + n <= m + n ) by NAT_1:11;

then q <= m + n by XXREAL_0:2;

hence r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) by A60; :: thesis: verum

A61: for m being Nat st q + n <= m + n holds

r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) by A59;

take s = q + n; :: thesis: for m being Nat st s <= m holds

r < (Partial_Sums (Prob * (B ^\ n))) . m

let m be Nat; :: thesis: ( s <= m implies r < (Partial_Sums (Prob * (B ^\ n))) . m )

assume A62: s <= m ; :: thesis: r < (Partial_Sums (Prob * (B ^\ n))) . m

set z = m + n;

((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) = (Partial_Sums (Prob * (B ^\ n))) . ((m + n) - n) by A45, NAT_1:12;

hence r < (Partial_Sums (Prob * (B ^\ n))) . m by A62, A61, NAT_1:12; :: thesis: verum

for m being Nat st q <= m holds

r < (Partial_Sums (Prob * (B ^\ n))) . m ; :: thesis: verum

( lim ((1 + (Partial_Sums (Prob * A))) ") = 0 & (1 + (Partial_Sums (Prob * A))) " is convergent )

proof

Partial_Intersection (Complement (B ^\ n)) is non-ascending
by PROB_3:27;
let A be SetSequence of Sigma; :: thesis: ( Partial_Sums (Prob * A) is divergent_to+infty implies ( lim ((1 + (Partial_Sums (Prob * A))) ") = 0 & (1 + (Partial_Sums (Prob * A))) " is convergent ) )

A64: for A being SetSequence of Sigma st ( for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (Partial_Sums (Prob * A)) . m ) holds

for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m

then for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (Partial_Sums (Prob * A)) . m by LIMFUNC1:def 4;

then for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m by A64;

then 1 + (Partial_Sums (Prob * A)) is divergent_to+infty by LIMFUNC1:def 4;

hence ( lim ((1 + (Partial_Sums (Prob * A))) ") = 0 & (1 + (Partial_Sums (Prob * A))) " is convergent ) by LIMFUNC1:34; :: thesis: verum

end;A64: for A being SetSequence of Sigma st ( for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (Partial_Sums (Prob * A)) . m ) holds

for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m

proof

assume
Partial_Sums (Prob * A) is divergent_to+infty
; :: thesis: ( lim ((1 + (Partial_Sums (Prob * A))) ") = 0 & (1 + (Partial_Sums (Prob * A))) " is convergent )
let A be SetSequence of Sigma; :: thesis: ( ( for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (Partial_Sums (Prob * A)) . m ) implies for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m )

assume A65: for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (Partial_Sums (Prob * A)) . m ; :: thesis: for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m

let r be Real; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m

consider n being Nat such that

A66: for m being Nat st n <= m holds

r < (Partial_Sums (Prob * A)) . m by A65;

take n ; :: thesis: for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m

for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m

r < (1 + (Partial_Sums (Prob * A))) . m ; :: thesis: verum

end;for m being Nat st n <= m holds

r < (Partial_Sums (Prob * A)) . m ) implies for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m )

assume A65: for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (Partial_Sums (Prob * A)) . m ; :: thesis: for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m

let r be Real; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m

consider n being Nat such that

A66: for m being Nat st n <= m holds

r < (Partial_Sums (Prob * A)) . m by A65;

take n ; :: thesis: for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m

for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m

proof

hence
for m being Nat st n <= m holds
let m be Nat; :: thesis: ( n <= m implies r < (1 + (Partial_Sums (Prob * A))) . m )

A67: m in NAT by ORDINAL1:def 12;

assume n <= m ; :: thesis: r < (1 + (Partial_Sums (Prob * A))) . m

then A68: r < (Partial_Sums (Prob * A)) . m by A66;

A69: (Partial_Sums (Prob * A)) . m < ((Partial_Sums (Prob * A)) . m) + 1 by XREAL_1:29;

(1 + (Partial_Sums (Prob * A))) . m = ((Partial_Sums (Prob * A)) . m) + 1 by VALUED_1:2, A67;

hence r < (1 + (Partial_Sums (Prob * A))) . m by A68, A69, XXREAL_0:2; :: thesis: verum

end;A67: m in NAT by ORDINAL1:def 12;

assume n <= m ; :: thesis: r < (1 + (Partial_Sums (Prob * A))) . m

then A68: r < (Partial_Sums (Prob * A)) . m by A66;

A69: (Partial_Sums (Prob * A)) . m < ((Partial_Sums (Prob * A)) . m) + 1 by XREAL_1:29;

(1 + (Partial_Sums (Prob * A))) . m = ((Partial_Sums (Prob * A)) . m) + 1 by VALUED_1:2, A67;

hence r < (1 + (Partial_Sums (Prob * A))) . m by A68, A69, XXREAL_0:2; :: thesis: verum

r < (1 + (Partial_Sums (Prob * A))) . m ; :: thesis: verum

then for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (Partial_Sums (Prob * A)) . m by LIMFUNC1:def 4;

then for r being Real ex n being Nat st

for m being Nat st n <= m holds

r < (1 + (Partial_Sums (Prob * A))) . m by A64;

then 1 + (Partial_Sums (Prob * A)) is divergent_to+infty by LIMFUNC1:def 4;

hence ( lim ((1 + (Partial_Sums (Prob * A))) ") = 0 & (1 + (Partial_Sums (Prob * A))) " is convergent ) by LIMFUNC1:34; :: thesis: verum

then A70: ( Prob * (Partial_Intersection (Complement (B ^\ n))) is convergent & (1 + (Partial_Sums (Prob * (B ^\ n)))) " is convergent ) by A42, A63, PROB_1:def 8;

A71: lim ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") = 0 by A42, A63;

A72: for k being Nat holds 0 <= (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k

proof

A74:
lim (Prob * (Partial_Intersection (Complement (B ^\ n)))) <= 0
by A70, A21, A71, SEQ_2:18;
let k be Nat; :: thesis: 0 <= (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k

A73: k in NAT by ORDINAL1:def 12;

dom (Prob * (Partial_Intersection (Complement (B ^\ n)))) = NAT by FUNCT_2:def 1;

then (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k = Prob . ((Partial_Intersection (Complement (B ^\ n))) . k) by FUNCT_1:12, A73;

hence 0 <= (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k by PROB_1:def 8; :: thesis: verum

end;A73: k in NAT by ORDINAL1:def 12;

dom (Prob * (Partial_Intersection (Complement (B ^\ n)))) = NAT by FUNCT_2:def 1;

then (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k = Prob . ((Partial_Intersection (Complement (B ^\ n))) . k) by FUNCT_1:12, A73;

hence 0 <= (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k by PROB_1:def 8; :: thesis: verum

Complement (B ^\ n) = (Complement B) ^\ n

proof

hence
(Prob * (Intersect_Shift_Seq (Complement B))) . n = 0
by A72, A70, A74, A20, SEQ_2:17; :: thesis: verum
for k being object st k in NAT holds

(Complement (B ^\ n)) . k = ((Complement B) ^\ n) . k

end;(Complement (B ^\ n)) . k = ((Complement B) ^\ n) . k

proof

hence
Complement (B ^\ n) = (Complement B) ^\ n
; :: thesis: verum
let k be object ; :: thesis: ( k in NAT implies (Complement (B ^\ n)) . k = ((Complement B) ^\ n) . k )

assume k in NAT ; :: thesis: (Complement (B ^\ n)) . k = ((Complement B) ^\ n) . k

then reconsider k = k as Nat ;

A75: (Complement (B ^\ n)) . k = ((B ^\ n) . k) ` by PROB_1:def 2;

((Complement B) ^\ n) . k = (Complement B) . (k + n) by NAT_1:def 3;

then ((Complement B) ^\ n) . k = (B . (k + n)) ` by PROB_1:def 2;

hence (Complement (B ^\ n)) . k = ((Complement B) ^\ n) . k by A75, NAT_1:def 3; :: thesis: verum

end;assume k in NAT ; :: thesis: (Complement (B ^\ n)) . k = ((Complement B) ^\ n) . k

then reconsider k = k as Nat ;

A75: (Complement (B ^\ n)) . k = ((B ^\ n) . k) ` by PROB_1:def 2;

((Complement B) ^\ n) . k = (Complement B) . (k + n) by NAT_1:def 3;

then ((Complement B) ^\ n) . k = (B . (k + n)) ` by PROB_1:def 2;

hence (Complement (B ^\ n)) . k = ((Complement B) ^\ n) . k by A75, NAT_1:def 3; :: thesis: verum

A76: ex n being Nat st (seq_const 0) . n = 0 A77: lim (seq_const 0) = 0 by A76, SEQ_4:25;

A78: ( seq_const 0 is convergent & ex k being Nat st

for n being Nat st k <= n holds

(seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n )

proof

( Prob . (@lim_inf (Complement B)) = 0 & (Prob . (@lim_inf (Complement B))) + (Prob . (@lim_sup B)) = 1 )
by A15, A78, A77, Th15, SEQ_4:19;
ex k being Nat st

for n being Nat st k <= n holds

(seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n

for n being Nat st k <= n holds

(seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n ) ; :: thesis: verum

end;for n being Nat st k <= n holds

(seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n

proof

hence
( seq_const 0 is convergent & ex k being Nat st
A79:
for n being Nat st n >= 0 holds

(seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n

(seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n

thus for n being Nat st 0 <= n holds

(seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n by A79; :: thesis: verum

end;(seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n

proof

take
0
; :: thesis: for n being Nat st 0 <= n holds
let n be Nat; :: thesis: ( n >= 0 implies (seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n )

assume n >= 0 ; :: thesis: (seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n

( (seq_const 0) . n = 0 & (Prob * (Intersect_Shift_Seq (Complement B))) . n = 0 ) by A16;

hence (seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n ; :: thesis: verum

end;assume n >= 0 ; :: thesis: (seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n

( (seq_const 0) . n = 0 & (Prob * (Intersect_Shift_Seq (Complement B))) . n = 0 ) by A16;

hence (seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n ; :: thesis: verum

(seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n

thus for n being Nat st 0 <= n holds

(seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n by A79; :: thesis: verum

for n being Nat st k <= n holds

(seq_const 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n ) ; :: thesis: verum

hence ( Prob . (@lim_inf (Complement B)) = 0 & Prob . (@lim_sup B) = 1 ) ; :: thesis: verum