:: Borel-Cantelli Lemma
:: by Peter Jaeger
::
:: Received January 31, 2011
:: Copyright (c) 2011-2012 Association of Mizar Users


begin

definition
let D be set ;
let x, y be ext-real number ;
let a, b be Element of D;
:: original: IFGT
redefine func IFGT (x,y,a,b) -> Element of D;
coherence
IFGT (x,y,a,b) is Element of D by XXREAL_0:def 11;
end;

theorem Th1: :: BOR_CANT:1
for k being Element of NAT
for x being Element of REAL st k is odd & x > 0 & x <= 1 holds
(((- x) rExpSeq) . (k + 1)) + (((- x) rExpSeq) . (k + 2)) >= 0
proof end;

theorem Th2: :: BOR_CANT:2
for x being Element of REAL holds 1 + x <= exp_R . x
proof end;

definition
let s be Real_Sequence;
func JSum s -> Real_Sequence means :Def1: :: BOR_CANT:def 1
 for d being Nat holds it . d = Sum ((- (s . d)) rExpSeq);
existence
ex b1 being Real_Sequence st
for d being Nat holds b1 . d = Sum ((- (s . d)) rExpSeq)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for d being Nat holds b1 . d = Sum ((- (s . d)) rExpSeq) ) & ( for d being Nat holds b2 . d = Sum ((- (s . d)) rExpSeq) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines JSum BOR_CANT:def 1 :
for s, b2 being Real_Sequence holds
( b2 = JSum s iff for d being Nat holds b2 . d = Sum ((- (s . d)) rExpSeq) );

theorem Th3: :: BOR_CANT:3
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n being Element of NAT holds (Partial_Product (JSum (Prob * A))) . n = exp_R . (- ((Partial_Sums (Prob * A)) . n))
proof end;

theorem Th4: :: BOR_CANT:4
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n being Element of NAT holds (Partial_Product (Prob * (Complement A))) . n <= (Partial_Product (JSum (Prob * A))) . n
proof end;

definition
let n1, n2 be Element of NAT ;
func Special_Function (n1,n2) -> sequence of NAT means :Def2: :: BOR_CANT:def 2
 for n being Element of NAT holds it . n = IFGT (n,n1,(n + n2),n);
existence
ex b1 being sequence of NAT st
for n being Element of NAT holds b1 . n = IFGT (n,n1,(n + n2),n)
proof end;
uniqueness
for b1, b2 being sequence of NAT st ( for n being Element of NAT holds b1 . n = IFGT (n,n1,(n + n2),n) ) & ( for n being Element of NAT holds b2 . n = IFGT (n,n1,(n + n2),n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Special_Function BOR_CANT:def 2 :
for n1, n2 being Element of NAT
for b3 being sequence of NAT holds
( b3 = Special_Function (n1,n2) iff for n being Element of NAT holds b3 . n = IFGT (n,n1,(n + n2),n) );

definition
let k be Element of NAT ;
func Special_Function2 k -> sequence of NAT means :Def3: :: BOR_CANT:def 3
 for n being Element of NAT holds it . n = n + k;
existence
ex b1 being sequence of NAT st
for n being Element of NAT holds b1 . n = n + k
proof end;
uniqueness
for b1, b2 being sequence of NAT st ( for n being Element of NAT holds b1 . n = n + k ) & ( for n being Element of NAT holds b2 . n = n + k ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Special_Function2 BOR_CANT:def 3 :
for k being Element of NAT
for b2 being sequence of NAT holds
( b2 = Special_Function2 k iff for n being Element of NAT holds b2 . n = n + k );

definition
let k be Element of NAT ;
func Special_Function3 k -> sequence of NAT means :Def4: :: BOR_CANT:def 4
 for n being Element of NAT holds it . n = IFGT (n,k,0,1);
existence
ex b1 being sequence of NAT st
for n being Element of NAT holds b1 . n = IFGT (n,k,0,1)
proof end;
uniqueness
for b1, b2 being sequence of NAT st ( for n being Element of NAT holds b1 . n = IFGT (n,k,0,1) ) & ( for n being Element of NAT holds b2 . n = IFGT (n,k,0,1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Special_Function3 BOR_CANT:def 4 :
for k being Element of NAT
for b2 being sequence of NAT holds
( b2 = Special_Function3 k iff for n being Element of NAT holds b2 . n = IFGT (n,k,0,1) );

definition
let n1, n2 be Element of NAT ;
func Special_Function4 (n1,n2) -> sequence of NAT means :Def5: :: BOR_CANT:def 5
 for n being Element of NAT holds it . n = IFGT (n,(n1 + 1),(n + n2),n);
existence
ex b1 being sequence of NAT st
for n being Element of NAT holds b1 . n = IFGT (n,(n1 + 1),(n + n2),n)
proof end;
uniqueness
for b1, b2 being sequence of NAT st ( for n being Element of NAT holds b1 . n = IFGT (n,(n1 + 1),(n + n2),n) ) & ( for n being Element of NAT holds b2 . n = IFGT (n,(n1 + 1),(n + n2),n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Special_Function4 BOR_CANT:def 5 :
for n1, n2 being Element of NAT
for b3 being sequence of NAT holds
( b3 = Special_Function4 (n1,n2) iff for n being Element of NAT holds b3 . n = IFGT (n,(n1 + 1),(n + n2),n) );

registration
let n1, n2 be Element of NAT ;
cluster Special_Function (n1,n2) -> one-to-one ;
coherence
Special_Function (n1,n2) is one-to-one
proof end;
cluster Special_Function4 (n1,n2) -> one-to-one ;
coherence
Special_Function4 (n1,n2) is one-to-one
proof end;
end;

registration
let n be Element of NAT ;
cluster Special_Function2 n -> one-to-one ;
coherence
Special_Function2 n is one-to-one
proof end;
end;

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let s be Element of NAT ;
let A be SetSequence of Sigma;
cluster A ^\ s -> Sigma -valued ;
coherence
A ^\ s is Sigma -valued ;
end;

theorem Th5: :: BOR_CANT:5
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for n, n1, n2 being Element of NAT holds
( ( for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds
(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ) & ( for A, B, C being SetSequence of Sigma
for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds
(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) ) )
proof end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let Prob be Probability of Sigma;
let A be SetSequence of Sigma;
pred A is_all_independent_wrt Prob means :Def6: :: BOR_CANT:def 6
 for B being SetSequence of Sigma st ex e being sequence of NAT st
( e is one-to-one & ( for n being Element of NAT holds A . (e . n) = B . n ) ) holds
for n being Element of NAT holds (Partial_Product (Prob * B)) . n = Prob . ((Partial_Intersection B) . n);
end;

:: deftheorem Def6 defines is_all_independent_wrt BOR_CANT:def 6 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma holds
( A is_all_independent_wrt Prob iff for B being SetSequence of Sigma st ex e being sequence of NAT st
( e is one-to-one & ( for n being Element of NAT holds A . (e . n) = B . n ) ) holds
for n being Element of NAT holds (Partial_Product (Prob * B)) . n = Prob . ((Partial_Intersection B) . n) );

theorem Th6: :: BOR_CANT:6
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n, n1, n2 being Element of NAT st n > n1 & A is_all_independent_wrt Prob holds
Prob . (((Partial_Intersection (Complement A)) . n1) /\ ((Partial_Intersection (A ^\ ((n1 + n2) + 1))) . ((n - n1) - 1))) = ((Partial_Product (Prob * (Complement A))) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1))
proof end;

theorem Th7: :: BOR_CANT:7
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being SetSequence of Sigma
for n being Element of NAT holds (Partial_Intersection (Complement A)) . n = ((Partial_Union A) . n) `
proof end;

theorem Th8: :: BOR_CANT:8
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n being Element of NAT holds Prob . ((Partial_Intersection (Complement A)) . n) = 1 - (Prob . ((Partial_Union A) . n))
proof end;

definition
let X be set ;
let A be SetSequence of X;
func Union_Shift_Seq A -> SetSequence of X means :Def7: :: BOR_CANT:def 7
 for n being Element of NAT holds it . n = Union (A ^\ n);
existence
ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = Union (A ^\ n)
proof end;
uniqueness
for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = Union (A ^\ n) ) & ( for n being Element of NAT holds b2 . n = Union (A ^\ n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Union_Shift_Seq BOR_CANT:def 7 :
for X being set
for A, b3 being SetSequence of X holds
( b3 = Union_Shift_Seq A iff for n being Element of NAT holds b3 . n = Union (A ^\ n) );

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let A be SetSequence of Sigma;
cluster Union_Shift_Seq A -> Sigma -valued ;
coherence
Union_Shift_Seq A is Sigma -valued
proof end;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let A be SetSequence of Sigma;
func @lim_sup A -> Event of Sigma equals :: BOR_CANT:def 8
 @Intersection (Union_Shift_Seq A);
correctness
coherence
@Intersection (Union_Shift_Seq A) is Event of Sigma;
;
end;

:: deftheorem defines @lim_sup BOR_CANT:def 8 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being SetSequence of Sigma holds @lim_sup A = @Intersection (Union_Shift_Seq A);

definition
let X be set ;
let A be SetSequence of X;
func Intersect_Shift_Seq A -> SetSequence of X means :Def9: :: BOR_CANT:def 9
 for n being Element of NAT holds it . n = Intersection (A ^\ n);
existence
ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = Intersection (A ^\ n)
proof end;
uniqueness
for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = Intersection (A ^\ n) ) & ( for n being Element of NAT holds b2 . n = Intersection (A ^\ n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Intersect_Shift_Seq BOR_CANT:def 9 :
for X being set
for A, b3 being SetSequence of X holds
( b3 = Intersect_Shift_Seq A iff for n being Element of NAT holds b3 . n = Intersection (A ^\ n) );

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let A be SetSequence of Sigma;
cluster Intersect_Shift_Seq A -> Sigma -valued ;
coherence
Intersect_Shift_Seq A is Sigma -valued
proof end;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let A be SetSequence of Sigma;
func @lim_inf A -> Event of Sigma equals :: BOR_CANT:def 10
 Union (Intersect_Shift_Seq A);
correctness
coherence
Union (Intersect_Shift_Seq A) is Event of Sigma;
by PROB_1:26;
end;

:: deftheorem defines @lim_inf BOR_CANT:def 10 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being SetSequence of Sigma holds @lim_inf A = Union (Intersect_Shift_Seq A);

theorem Th9: :: BOR_CANT:9
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being SetSequence of Sigma
for n being Element of NAT holds (Intersect_Shift_Seq (Complement A)) . n = ((Union_Shift_Seq A) . n) `
proof end;

theorem Th10: :: BOR_CANT:10
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n being Element of NAT st A is_all_independent_wrt Prob holds
Prob . ((Partial_Intersection (Complement A)) . n) = (Partial_Product (Prob * (Complement A))) . n
proof end;

theorem Th11: :: BOR_CANT:11
for X being set
for A being SetSequence of X holds
( superior_setsequence A = Union_Shift_Seq A & inferior_setsequence A = Intersect_Shift_Seq A )
proof end;

theorem :: BOR_CANT:12
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being SetSequence of Sigma holds
( superior_setsequence A = Union_Shift_Seq A & inferior_setsequence A = Intersect_Shift_Seq A ) by Th11;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let Prob be Probability of Sigma;
let A be SetSequence of Sigma;
func Sum_Shift_Seq (Prob,A) -> Real_Sequence means :Def11: :: BOR_CANT:def 11
 for n being Element of NAT holds it . n = Sum (Prob * (A ^\ n));
existence
ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = Sum (Prob * (A ^\ n))
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = Sum (Prob * (A ^\ n)) ) & ( for n being Element of NAT holds b2 . n = Sum (Prob * (A ^\ n)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines Sum_Shift_Seq BOR_CANT:def 11 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for b5 being Real_Sequence holds
( b5 = Sum_Shift_Seq (Prob,A) iff for n being Element of NAT holds b5 . n = Sum (Prob * (A ^\ n)) );

theorem Th13: :: BOR_CANT:13
for Omega being 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 )
proof end;

theorem Th14: :: BOR_CANT:14
for Omega being non empty set
for Sigma being SigmaField of Omega holds
( ( for X being set
for A being SetSequence of X
for n being Element of NAT
for x being set holds
( ex k being Element of NAT st x in (A ^\ n) . k iff ex k being Element of NAT st
( k >= n & x in A . k ) ) ) & ( for X being set
for A being SetSequence of X
for x being set holds
( x in Intersection (Union_Shift_Seq A) iff for m being Element of NAT ex n being Element of NAT st
( n >= m & x in A . n ) ) ) & ( for A being SetSequence of Sigma
for x being set holds
( x in @Intersection (Union_Shift_Seq A) iff for m being Element of NAT ex n being Element of NAT st
( n >= m & x in A . n ) ) ) & ( for X being set
for A being SetSequence of X
for x being set holds
( x in Union (Intersect_Shift_Seq A) iff ex n being Element of NAT st
for k being Element of NAT st k >= n holds
x in A . k ) ) & ( for A being SetSequence of Sigma
for x being set holds
( x in Union (Intersect_Shift_Seq A) iff ex n being Element of NAT st
for k being Element of NAT st k >= n holds
x in A . k ) ) & ( for A being SetSequence of Sigma
for x being Element of Omega holds
( x in Union (Intersect_Shift_Seq (Complement A)) iff ex n being Element of NAT st
for k being Element of NAT st k >= n holds
not x in A . k ) ) )
proof end;

theorem Th15: :: BOR_CANT:15
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma holds
( lim_sup A = @lim_sup A & lim_inf A = @lim_inf A & @lim_inf (Complement A) = (@lim_sup A) ` & (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 & (Prob . (lim_inf (Complement A))) + (Prob . (lim_sup A)) = 1 )
proof end;

theorem Th16: :: BOR_CANT:16
for Omega being non empty set
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 ) ) )
proof end;

theorem Th17: :: BOR_CANT:17
for Omega being non empty set
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 )
proof end;

theorem :: BOR_CANT:18
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma st A is_all_independent_wrt Prob holds
( ( Prob . (lim_inf (Complement A)) = 0 or Prob . (lim_inf (Complement A)) = 1 ) & ( Prob . (lim_sup A) = 0 or Prob . (lim_sup A) = 1 ) )
proof end;

theorem :: BOR_CANT:19
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n1, n being Element of NAT holds (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)
proof end;

theorem :: BOR_CANT:20
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n being Element of NAT holds Prob . ((Intersect_Shift_Seq (Complement A)) . n) = 1 - (Prob . ((Union_Shift_Seq A) . n))
proof end;

theorem :: BOR_CANT:21
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n being Element of NAT holds
( ( Complement A is_all_independent_wrt Prob implies Prob . ((Partial_Intersection A) . n) = (Partial_Product (Prob * A)) . n ) & ( A is_all_independent_wrt Prob implies 1 - (Prob . ((Partial_Union A) . n)) = (Partial_Product (Prob * (Complement A))) . n ) )
proof end;