:: 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;
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;

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

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;

definition

let s be Real_Sequence;

ex b_{1} being Real_Sequence st

for d being Nat holds b_{1} . d = Sum ((- (s . d)) rExpSeq)

for b_{1}, b_{2} being Real_Sequence st ( for d being Nat holds b_{1} . d = Sum ((- (s . d)) rExpSeq) ) & ( for d being Nat holds b_{2} . d = Sum ((- (s . d)) rExpSeq) ) holds

b_{1} = b_{2}

end;
func JSum s -> Real_Sequence means :Def1: :: BOR_CANT:def 1

for d being Nat holds it . d = Sum ((- (s . d)) rExpSeq);

existence for d being Nat holds it . d = Sum ((- (s . d)) rExpSeq);

ex b

for d being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines JSum BOR_CANT:def 1 :

for s, b_{2} being Real_Sequence holds

( b_{2} = JSum s iff for d being Nat holds b_{2} . d = Sum ((- (s . d)) rExpSeq) );

for s, b

( b

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))

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

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;

ex b_{1} being sequence of NAT st

for n being Nat holds b_{1} . n = IFGT (n,n1,(n + n2),n)

for b_{1}, b_{2} being sequence of NAT st ( for n being Nat holds b_{1} . n = IFGT (n,n1,(n + n2),n) ) & ( for n being Nat holds b_{2} . n = IFGT (n,n1,(n + n2),n) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = IFGT (n,n1,(n + n2),n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines Special_Function BOR_CANT:def 2 :

for n1, n2 being Nat

for b_{3} being sequence of NAT holds

( b_{3} = Special_Function (n1,n2) iff for n being Nat holds b_{3} . n = IFGT (n,n1,(n + n2),n) );

for n1, n2 being Nat

for b

( b

definition

let k be Nat;

ex b_{1} being sequence of NAT st

for n being Nat holds b_{1} . n = n + k

for b_{1}, b_{2} being sequence of NAT st ( for n being Nat holds b_{1} . n = n + k ) & ( for n being Nat holds b_{2} . n = n + k ) holds

b_{1} = b_{2}

end;
func Special_Function2 k -> sequence of NAT means :Def3: :: BOR_CANT:def 3

for n being Nat holds it . n = n + k;

existence for n being Nat holds it . n = n + k;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines Special_Function2 BOR_CANT:def 3 :

for k being Nat

for b_{2} being sequence of NAT holds

( b_{2} = Special_Function2 k iff for n being Nat holds b_{2} . n = n + k );

for k being Nat

for b

( b

definition

let k be Nat;

ex b_{1} being sequence of NAT st

for n being Nat holds b_{1} . n = IFGT (n,k,0,1)

for b_{1}, b_{2} being sequence of NAT st ( for n being Nat holds b_{1} . n = IFGT (n,k,0,1) ) & ( for n being Nat holds b_{2} . n = IFGT (n,k,0,1) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = IFGT (n,k,0,1);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines Special_Function3 BOR_CANT:def 4 :

for k being Nat

for b_{2} being sequence of NAT holds

( b_{2} = Special_Function3 k iff for n being Nat holds b_{2} . n = IFGT (n,k,0,1) );

for k being Nat

for b

( b

definition

let n1, n2 be Nat;

ex b_{1} being sequence of NAT st

for n being Nat holds b_{1} . n = IFGT (n,(n1 + 1),(n + n2),n)

for b_{1}, b_{2} being sequence of NAT st ( for n being Nat holds b_{1} . n = IFGT (n,(n1 + 1),(n + n2),n) ) & ( for n being Nat holds b_{2} . n = IFGT (n,(n1 + 1),(n + n2),n) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = IFGT (n,(n1 + 1),(n + n2),n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines Special_Function4 BOR_CANT:def 5 :

for n1, n2 being Nat

for b_{3} being sequence of NAT holds

( b_{3} = Special_Function4 (n1,n2) iff for n being Nat holds b_{3} . n = IFGT (n,(n1 + 1),(n + n2),n) );

for n1, n2 being Nat

for b

( b

registration

let n1, n2 be Nat;

coherence

Special_Function (n1,n2) is one-to-one

Special_Function4 (n1,n2) is one-to-one

end;
coherence

Special_Function (n1,n2) is one-to-one

proof end;

coherence Special_Function4 (n1,n2) is one-to-one

proof end;

registration

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let s be Nat;

let A be SetSequence of Sigma;

coherence

A ^\ s is Sigma -valued ;

end;
let Sigma be SigmaField of Omega;

let s be Nat;

let A be SetSequence of Sigma;

coherence

A ^\ s is Sigma -valued ;

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)) ) )

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;

end;
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);

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);

:: 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) );

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))

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) `

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))

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;

for b_{1} being SetSequence of X holds

( b_{1} = superior_setsequence A iff for n being Nat holds b_{1} . n = Union (A ^\ n) )

superior_setsequence A is SetSequence of X

end;
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 redefine func superior_setsequence A -> SetSequence of X means :Def7: :: BOR_CANT:def 7

for n being Nat holds it . n = Union (A ^\ n);

for b

( b

proof end;

coherence superior_setsequence A is SetSequence of X

proof end;

:: deftheorem Def7 defines superior_setsequence BOR_CANT:def 7 :

for X being set

for A, b_{3} being SetSequence of X holds

( b_{3} = superior_setsequence A iff for n being Nat holds b_{3} . n = Union (A ^\ n) );

for X being set

for A, b

( b

registration

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let A be SetSequence of Sigma;

coherence

superior_setsequence A is Sigma -valued

end;
let Sigma be SigmaField of Omega;

let A be SetSequence of Sigma;

coherence

superior_setsequence A is Sigma -valued

proof end;

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let A be SetSequence of Sigma;

coherence

lim_sup A is Event of Sigma

end;
let Sigma be SigmaField of Omega;

let A be SetSequence of Sigma;

coherence

lim_sup A is Event of Sigma

proof 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;

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;

inferior_setsequence A is SetSequence of X

for b_{1} being SetSequence of X holds

( b_{1} = inferior_setsequence A iff for n being Nat holds b_{1} . n = Intersection (A ^\ n) )

end;
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 redefine func inferior_setsequence A -> SetSequence of X means :Def9: :: BOR_CANT:def 9

for n being Nat holds it . n = Intersection (A ^\ n);

inferior_setsequence A is SetSequence of X

proof end;

compatibility for b

( b

proof end;

:: deftheorem Def9 defines inferior_setsequence BOR_CANT:def 9 :

for X being set

for A, b_{3} being SetSequence of X holds

( b_{3} = inferior_setsequence A iff for n being Nat holds b_{3} . n = Intersection (A ^\ n) );

for X being set

for A, b

( b

registration

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let A be SetSequence of Sigma;

coherence

inferior_setsequence A is Sigma -valued

end;
let Sigma be SigmaField of Omega;

let A be SetSequence of Sigma;

coherence

inferior_setsequence A is Sigma -valued

proof end;

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let A be SetSequence of Sigma;

coherence

lim_inf A is Event of Sigma by PROB_1:26;

end;
let Sigma be SigmaField of Omega;

let A be SetSequence of Sigma;

coherence

lim_inf A is Event of Sigma by PROB_1:26;

:: 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;

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) `

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

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;

::$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;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = Sum (Prob * (A ^\ n))

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = Sum (Prob * (A ^\ n)) ) & ( for n being Nat holds b_{2} . n = Sum (Prob * (A ^\ n)) ) holds

b_{1} = b_{2}

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

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof 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_{5} being Real_Sequence holds

( b_{5} = Sum_Shift_Seq (Prob,A) iff for n being Nat holds b_{5} . n = Sum (Prob * (A ^\ n)) );

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

( b

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 )

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 ) ) )

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 )

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 ) ) )

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 )

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 ) )

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)

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))

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 ) )

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;