:: Borel-Cantelli Lemma
:: by Peter Jaeger
::
:: Received January 31, 2011
:: Copyright (c) 2011 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 not k is even & 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 b₁ being Real_Sequence st
for d being Nat holds b₁ . d = Sum ((- (s . d)) rExpSeq)

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for d being Nat holds b₁ . d = Sum ((- (s . d)) rExpSeq) ) & ( for d being Nat holds b₂ . d = Sum ((- (s . d)) rExpSeq) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines JSum BOR_CANT:def 1 :
for s, b₂ being Real_Sequence holds
( b₂ = JSum s iff for d being Nat holds b₂ . 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 b₁ being sequence of NAT st
for n being Element of NAT holds b₁ . n = IFGT (n,n1,(n + n2),n)

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st ( for n being Element of NAT holds b₁ . n = IFGT (n,n1,(n + n2),n) ) & ( for n being Element of NAT holds b₂ . n = IFGT (n,n1,(n + n2),n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Special_Function BOR_CANT:def 2 :
for n1, n2 being Element of NAT
for b₃ being sequence of NAT holds
( b₃ = Special_Function (n1,n2) iff for n being Element of NAT holds b₃ . 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 b₁ being sequence of NAT st
for n being Element of NAT holds b₁ . n = n + k

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st ( for n being Element of NAT holds b₁ . n = n + k ) & ( for n being Element of NAT holds b₂ . n = n + k ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Special_Function2 BOR_CANT:def 3 :
for k being Element of NAT
for b₂ being sequence of NAT holds
( b₂ = Special_Function2 k iff for n being Element of NAT holds b₂ . 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 b₁ being sequence of NAT st
for n being Element of NAT holds b₁ . n = IFGT (n,k,0,1)

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st ( for n being Element of NAT holds b₁ . n = IFGT (n,k,0,1) ) & ( for n being Element of NAT holds b₂ . n = IFGT (n,k,0,1) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Special_Function3 BOR_CANT:def 4 :
for k being Element of NAT
for b₂ being sequence of NAT holds
( b₂ = Special_Function3 k iff for n being Element of NAT holds b₂ . 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 b₁ being sequence of NAT st
for n being Element of NAT holds b₁ . n = IFGT (n,(n1 + 1),(n + n2),n)

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st ( for n being Element of NAT holds b₁ . n = IFGT (n,(n1 + 1),(n + n2),n) ) & ( for n being Element of NAT holds b₂ . n = IFGT (n,(n1 + 1),(n + n2),n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines Special_Function4 BOR_CANT:def 5 :
for n1, n2 being Element of NAT
for b₃ being sequence of NAT holds
( b₃ = Special_Function4 (n1,n2) iff for n being Element of NAT holds b₃ . 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;

definition

let X be set ;
let s be Element of NAT ;
let A be SetSequence of X;
func Shift_Seq (A,s) -> SetSequence of X equals :: BOR_CANT:def 6
A ^\ s;
correctness
coherence
A ^\ s is SetSequence of X;
;

end;

:: deftheorem defines Shift_Seq BOR_CANT:def 6 :
for X being set
for s being Element of NAT
for A being SetSequence of X holds Shift_Seq (A,s) = A ^\ s;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let s be Element of NAT ;
let A be SetSequence of Sigma;
func @Shift_Seq (A,s) -> SetSequence of Sigma equals :: BOR_CANT:def 7
Shift_Seq (A,s);
coherence
Shift_Seq (A,s) is SetSequence of Sigma

proof end;

end;

:: deftheorem defines @Shift_Seq BOR_CANT:def 7 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for s being Element of NAT
for A being SetSequence of Sigma holds @Shift_Seq (A,s) = Shift_Seq (A,s);

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 * (@Shift_Seq (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 (@Shift_Seq (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 :Def8: :: BOR_CANT:def 8
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 Def8 defines is_all_independent_wrt BOR_CANT:def 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 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 (@Shift_Seq (A,((n1 + n2) + 1)))) . ((n - n1) - 1))) = ((Partial_Product (Prob * (@Complement A))) . n1) * ((Partial_Product (Prob * (@Shift_Seq (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 :Def9: :: BOR_CANT:def 9
for n being Element of NAT holds it . n = Union (Shift_Seq (A,n));
existence
ex b₁ being SetSequence of X st
for n being Element of NAT holds b₁ . n = Union (Shift_Seq (A,n))

proof end;

uniqueness
for b₁, b₂ being SetSequence of X st ( for n being Element of NAT holds b₁ . n = Union (Shift_Seq (A,n)) ) & ( for n being Element of NAT holds b₂ . n = Union (Shift_Seq (A,n)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines Union_Shift_Seq BOR_CANT:def 9 :
for X being set
for A, b₃ being SetSequence of X holds
( b₃ = Union_Shift_Seq A iff for n being Element of NAT holds b₃ . n = Union (Shift_Seq (A,n)) );

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let A be SetSequence of Sigma;
func @Union_Shift_Seq A -> SetSequence of Sigma equals :: BOR_CANT:def 10
Union_Shift_Seq A;
coherence
Union_Shift_Seq A is SetSequence of Sigma

proof end;

end;

:: deftheorem defines @Union_Shift_Seq BOR_CANT:def 10 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being SetSequence of Sigma holds @Union_Shift_Seq A = Union_Shift_Seq A;

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 11
@Intersection (@Union_Shift_Seq A);
correctness
coherence
@Intersection (@Union_Shift_Seq A) is Event of Sigma;
;

end;

:: deftheorem defines @lim_sup BOR_CANT:def 11 :
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 :Def12: :: BOR_CANT:def 12
for n being Element of NAT holds it . n = Intersection (Shift_Seq (A,n));
existence
ex b₁ being SetSequence of X st
for n being Element of NAT holds b₁ . n = Intersection (Shift_Seq (A,n))

proof end;

uniqueness
for b₁, b₂ being SetSequence of X st ( for n being Element of NAT holds b₁ . n = Intersection (Shift_Seq (A,n)) ) & ( for n being Element of NAT holds b₂ . n = Intersection (Shift_Seq (A,n)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines Intersect_Shift_Seq BOR_CANT:def 12 :
for X being set
for A, b₃ being SetSequence of X holds
( b₃ = Intersect_Shift_Seq A iff for n being Element of NAT holds b₃ . n = Intersection (Shift_Seq (A,n)) );

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let A be SetSequence of Sigma;
func @Intersect_Shift_Seq A -> SetSequence of Sigma equals :: BOR_CANT:def 13
Intersect_Shift_Seq A;
coherence
Intersect_Shift_Seq A is SetSequence of Sigma

proof end;

end;

:: deftheorem defines @Intersect_Shift_Seq BOR_CANT:def 13 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being SetSequence of Sigma holds @Intersect_Shift_Seq A = Intersect_Shift_Seq A;

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 14
Union (@Intersect_Shift_Seq A);
correctness
coherence
Union (@Intersect_Shift_Seq A) is Event of Sigma;
by PROB_1:58;

end;

:: deftheorem defines @lim_inf BOR_CANT:def 14 :
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 :Def15: :: BOR_CANT:def 15
for n being Element of NAT holds it . n = Sum (Prob * (@Shift_Seq (A,n)));
existence
ex b₁ being Real_Sequence st
for n being Element of NAT holds b₁ . n = Sum (Prob * (@Shift_Seq (A,n)))

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Element of NAT holds b₁ . n = Sum (Prob * (@Shift_Seq (A,n))) ) & ( for n being Element of NAT holds b₂ . n = Sum (Prob * (@Shift_Seq (A,n))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines Sum_Shift_Seq BOR_CANT:def 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
for b₅ being Real_Sequence holds
( b₅ = Sum_Shift_Seq (Prob,A) iff for n being Element of NAT holds b₅ . n = Sum (Prob * (@Shift_Seq (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 (Shift_Seq (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 * (@Shift_Seq (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;