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

definition

let D be set ;
let x, y be ExtReal;
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 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 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 Nat holds (Partial_Product (Prob * (Complement A))) . n <= (Partial_Product (JSum (Prob * A))) . n

proof end;

definition

let n1, n2 be Nat;

func Special_Function (n1,n2) -> sequence of NAT means :Def2: :: BOR_CANT:def 2
for n being Nat holds it . n = IFGT (n,n1,(n + n2),n);

existence
ex b₁ being sequence of NAT st
for n being Nat holds b₁ . n = IFGT (n,n1,(n + n2),n)

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st ( for n being Nat holds b₁ . n = IFGT (n,n1,(n + n2),n) ) & ( for n being 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 Nat
for b₃ being sequence of NAT holds
( b₃ = Special_Function (n1,n2) iff for n being Nat holds b₃ . n = IFGT (n,n1,(n + n2),n) );

definition

let k be Nat;

func Special_Function2 k -> sequence of NAT means :Def3: :: BOR_CANT:def 3
for n being Nat holds it . n = n + k;

existence
ex b₁ being sequence of NAT st
for n being Nat holds b₁ . n = n + k

proof end;

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

proof end;

end;

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

definition

let k be Nat;

func Special_Function3 k -> sequence of NAT means :Def4: :: BOR_CANT:def 4
for n being Nat holds it . n = IFGT (n,k,0,1);

existence
ex b₁ being sequence of NAT st
for n being Nat holds b₁ . n = IFGT (n,k,0,1)

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st ( for n being Nat holds b₁ . n = IFGT (n,k,0,1) ) & ( for n being 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 Nat
for b₂ being sequence of NAT holds
( b₂ = Special_Function3 k iff for n being Nat holds b₂ . n = IFGT (n,k,0,1) );

definition

let n1, n2 be Nat;

func Special_Function4 (n1,n2) -> sequence of NAT means :Def5: :: BOR_CANT:def 5
for n being Nat holds it . n = IFGT (n,(n1 + 1),(n + n2),n);

existence
ex b₁ being sequence of NAT st
for n being 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 Nat holds b₁ . n = IFGT (n,(n1 + 1),(n + n2),n) ) & ( for n being 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 Nat
for b₃ being sequence of NAT holds
( b₃ = Special_Function4 (n1,n2) iff for n being Nat holds b₃ . n = IFGT (n,(n1 + 1),(n + n2),n) );

registration

let n1, n2 be 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 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 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 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 Nat holds A . (e . n) = B . n ) ) holds
for n being 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 Nat holds A . (e . n) = B . n ) ) holds
for n being 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 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 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 Nat holds Prob . ((Partial_Intersection (Complement A)) . n) = 1 - (Prob . ((Partial_Union A) . n))

proof end;

Lemacik0: for X being set
for F being SetSequence of X
for n being Nat holds (superior_setsequence F) . n = union (rng (F ^\ n))

proof end;

definition

let X be set ;
let A be SetSequence of X;

:: original: superior_setsequence
redefine func superior_setsequence A -> SetSequence of X means :Def7: :: BOR_CANT:def 7
for n being Nat holds it . n = Union (A ^\ n);

compatibility
for b₁ being SetSequence of X holds
( b₁ = superior_setsequence A iff for n being Nat holds b₁ . n = Union (A ^\ n) )

proof end;

coherence
superior_setsequence A is SetSequence of X

proof end;

end;

:: deftheorem Def7 defines superior_setsequence BOR_CANT:def 7 :
for X being set
for A, b₃ being SetSequence of X holds
( b₃ = superior_setsequence A iff for n being Nat holds b₃ . n = Union (A ^\ n) );

registration

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let A be SetSequence of Sigma;

cluster superior_setsequence A -> Sigma -valued ;

coherence
superior_setsequence 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
lim_sup A;

coherence
lim_sup A is Event of Sigma

proof end;

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 = lim_sup A;

definition

let X be set ;
let A be SetSequence of X;

:: original: inferior_setsequence
redefine func inferior_setsequence A -> SetSequence of X means :Def9: :: BOR_CANT:def 9
for n being Nat holds it . n = Intersection (A ^\ n);

coherence
inferior_setsequence A is SetSequence of X

proof end;

compatibility
for b₁ being SetSequence of X holds
( b₁ = inferior_setsequence A iff for n being Nat holds b₁ . n = Intersection (A ^\ n) )

proof end;

end;

:: deftheorem Def9 defines inferior_setsequence BOR_CANT:def 9 :
for X being set
for A, b₃ being SetSequence of X holds
( b₃ = inferior_setsequence A iff for n being Nat holds b₃ . n = Intersection (A ^\ n) );

registration

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let A be SetSequence of Sigma;

cluster inferior_setsequence A -> Sigma -valued ;

coherence
inferior_setsequence 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
lim_inf A;

coherence
lim_inf 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 = lim_inf 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 Nat holds (inferior_setsequence (Complement A)) . n = ((superior_setsequence 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 Nat st A is_all_independent_wrt Prob holds
Prob . ((Partial_Intersection (Complement A)) . n) = (Partial_Product (Prob * (Complement A))) . n

proof end;

theorem :: BOR_CANT:11

canceled;

theorem :: BOR_CANT:12

canceled;

::$CT 2

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 Nat holds it . n = Sum (Prob * (A ^\ n));

existence
ex b₁ being Real_Sequence st
for n being Nat holds b₁ . n = Sum (Prob * (A ^\ n))

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat holds b₁ . n = Sum (Prob * (A ^\ n)) ) & ( for n being Nat holds b₂ . n = Sum (Prob * (A ^\ n)) ) holds
b₁ = b₂

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 b₅ being Real_Sequence holds
( b₅ = Sum_Shift_Seq (Prob,A) iff for n being Nat holds b₅ . 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 Nat
for x being object holds
( ex k being Nat st x in (A ^\ n) . k iff ex k being Nat st
( k >= n & x in A . k ) ) ) & ( for X being set
for A being SetSequence of X
for x being object holds
( x in Intersection (superior_setsequence A) iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) ) ) & ( for A being SetSequence of Sigma
for x being object holds
( x in @Intersection (superior_setsequence A) iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) ) ) & ( for X being set
for A being SetSequence of X
for x being object holds
( x in Union (inferior_setsequence A) iff ex n being Nat st
for k being Nat st k >= n holds
x in A . k ) ) & ( for A being SetSequence of Sigma
for x being object holds
( x in Union (inferior_setsequence A) iff ex n being Nat st
for k being 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 (inferior_setsequence (Complement A)) iff ex n being Nat st
for k being Nat st k >= n holds
not x in A . k ) ) )

proof end;

Lemma: for Omega being non empty set
for Sigma being SigmaField of Omega
for A being SetSequence of Sigma holds lim_inf A = @lim_inf A
;

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_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 n, n1 being 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 Nat holds Prob . ((inferior_setsequence (Complement A)) . n) = 1 - (Prob . ((superior_setsequence 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 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;