:: Borel-Cantelli Lemma
::  by Peter Jaeger
::
:: Received January 31, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies BOR_CANT, REALSET1, ABIAN, SIN_COS, ARYTM_3, CARD_3, EQREL_1,
      COMPLEX1, NUMBERS, ZFMISC_1, CARD_1, XXREAL_0, NEWTON, REAL_1, RELAT_1,
      PROB_1, SEQ_1, SEQ_2, ARYTM_1, ORDINAL2, RPR_1, XBOOLE_0, SUBSET_1,
      PROB_2, SERIES_1, NAT_1, FUNCT_1, PROB_3, SERIES_3, LIMFUNC1, SETLIM_1,
      XXREAL_2, FUNCOP_1, FUNCT_7, ASYMPT_1, TARSKI, SETFAM_1;
 notations TARSKI, XXREAL_0, XCMPLX_0, XREAL_0, ORDINAL1, REAL_1, XBOOLE_0,
      SUBSET_1, SETFAM_1, NUMBERS, NAT_1, COMPLEX1, SEQ_1, COMSEQ_2, SEQ_2,
      RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, PROB_1, PROB_2,
      SERIES_1, PROB_3, VALUED_0, VALUED_1, ZFMISC_1, LIMFUNC1, SERIES_3,
      NEWTON, ABIAN, SIN_COS, SETLIM_1, FUNCT_6;
 constructors RELSET_1, BINARITH, SQUARE_1, COMSEQ_3, RVSUM_1, SIN_COS, REAL_1,
      LIMFUNC1, SETLIM_1, SEQ_2, SERIES_1, KURATO_0, RINFSUP1, PROB_3,
      SERIES_3, ABIAN, NEWTON, NUMBERS, NAT_D, SEQ_4, RFUNCT_1, RCOMP_1,
      SEQM_3, FUNCT_4, COMSEQ_2, SEQ_1, SETFAM_1;
 registrations FUNCT_2, XCMPLX_0, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS,
      XREAL_0, NAT_1, MEMBERED, VALUED_0, VALUED_1, ABIAN, XXREAL_0, RELAT_1,
      SEQ_4, NEWTON, FUNCOP_1, PROB_2, PROB_3, SETLIM_1, RELSET_1, SIN_COS,
      INT_1, SEQ_1, SEQ_2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve Omega for non empty set,
        Sigma for SigmaField of Omega,
        Prob for Probability of Sigma,
        A for SetSequence of Sigma,
        n,n1,n2 for Nat;

definition
  let D be set;
  let x,y be ExtReal, a,b be Element of D;
  redefine func IFGT(x,y,a,b) -> Element of D;
end;

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

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

definition let s be Real_Sequence;
  func JSum(s) -> Real_Sequence means
:: BOR_CANT:def 1
  for d being Nat holds it.d = Sum ((-s.d) rExpSeq);
end;

theorem :: BOR_CANT:3
  Partial_Product(JSum(Prob*A)).n = exp_R.(-Partial_Sums(Prob*A).n);

theorem :: BOR_CANT:4
  Partial_Product(Prob*(Complement A)).n <= Partial_Product(JSum(Prob*A)).n;

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

definition let k be Nat;
  func Special_Function2(k) -> sequence of NAT means
:: BOR_CANT:def 3
  for n being Nat holds it.n = n+k;
end;

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

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

registration
  let n1,n2 be Nat;
  cluster Special_Function(n1,n2) -> one-to-one;
  cluster Special_Function4(n1,n2) -> one-to-one;
end;

registration
  let n be Nat;
  cluster Special_Function2(n) -> one-to-one;
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;
end;

theorem :: BOR_CANT:5
( 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,
    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) );

definition
  let Omega be non empty set, Sigma be SigmaField of Omega,
      Prob be Probability of Sigma, A be SetSequence of Sigma;
  pred A is_all_independent_wrt Prob means
:: 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;

theorem :: BOR_CANT:6
  n>n1 & A is_all_independent_wrt Prob implies
    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);

theorem :: BOR_CANT:7
  (Partial_Intersection Complement A).n = ((Partial_Union A).n)`;

theorem :: BOR_CANT:8
  Prob.( (Partial_Intersection Complement A).n ) =
  1-Prob.( (Partial_Union A).n );

definition
  let X be set, A be SetSequence of X;
  redefine func superior_setsequence A -> SetSequence of X means
:: BOR_CANT:def 7
  for n being Nat holds it.n = Union (A^\n);
end;

registration
  let Omega be non empty set,
      Sigma be SigmaField of Omega,
      A be SetSequence of Sigma;
  cluster superior_setsequence A -> Sigma-valued;
end;

definition
  let Omega be non empty set, Sigma be SigmaField of Omega,
      A be SetSequence of Sigma;
  func @lim_sup A -> Event of Sigma equals
:: BOR_CANT:def 8
  lim_sup A;
end;

definition
  let X be set, A be SetSequence of X;
  redefine func inferior_setsequence A -> SetSequence of X means
:: BOR_CANT:def 9
  for n being Nat holds it.n = Intersection (A^\n);
end;

registration
  let Omega be non empty set,
      Sigma be SigmaField of Omega,
      A be SetSequence of Sigma;
  cluster inferior_setsequence A -> Sigma-valued;
end;

definition
  let Omega be non empty set, Sigma be SigmaField of Omega,
      A be SetSequence of Sigma;
  func @lim_inf A -> Event of Sigma equals
:: BOR_CANT:def 10
  lim_inf A;
end;

theorem :: BOR_CANT:9
  (inferior_setsequence Complement A).n = ((superior_setsequence A).n)`;

theorem :: BOR_CANT:10
  A is_all_independent_wrt Prob implies
     Prob.((Partial_Intersection Complement A).n) =
      Partial_Product(Prob*Complement A).n;

::$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
:: BOR_CANT:def 11
  for n being Nat holds it.n = Sum (Prob*(A^\n));
end;

theorem :: BOR_CANT:13
  Partial_Sums(Prob*A) is convergent implies
    (Prob.@lim_sup A = 0 & lim(Sum_Shift_Seq(Prob,A))=0 &
       Sum_Shift_Seq(Prob,A) is convergent);

theorem :: BOR_CANT:14
( for X being set, A being SetSequence of X holds
       for n being Nat, 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, A being SetSequence of X holds
      for x being object holds x in Intersection superior_setsequence A iff
      for m being Nat holds
       ex n being Nat st n>=m & x in A.n ) &
( for A being SetSequence of Sigma holds
              for x being object holds
           x in @Intersection superior_setsequence A iff
           for m being Nat holds
            ex n being Nat st n>=m & x in A.n ) &
( for X being set, A being SetSequence of X holds
        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 holds
             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 holds
              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 ) ) );

theorem :: BOR_CANT:15
  @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;

theorem :: BOR_CANT:16
(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);

theorem :: BOR_CANT:17
 (not Partial_Sums(Prob*A) is convergent &
   A is_all_independent_wrt Prob) implies
  (Prob.lim_inf Complement A = 0 & Prob.lim_sup A = 1);

theorem :: BOR_CANT:18
A is_all_independent_wrt Prob implies
  (Prob.lim_inf Complement A = 0 or
   Prob.lim_inf Complement A = 1) &
   (Prob.lim_sup A = 0 or Prob.lim_sup A = 1);

theorem :: BOR_CANT:19
(Partial_Sums(Prob*(A^\(n1+1)))).n <=
Partial_Sums(Prob*A).(n1+1+n) - Partial_Sums(Prob*A).n1;

theorem :: BOR_CANT:20
Prob.( (inferior_setsequence Complement A).n ) =
  1-Prob.( (superior_setsequence A).n );

theorem :: BOR_CANT:21
( 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);