bor_cant.miz
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;
:: original:
IFGT
redefine
func
IFGT (x,y,a,b) ->
Element of D ;
coherence by
XXREAL_0:def 11;
end
theorem ::
BOR_CANT:1
Th1: for k be
Element of
NAT , x be
Element of
REAL st k is
odd & x
>
0 & x
<= 1 holds ((((
- x)
rExpSeq )
. (k
+ 1))
+ (((
- x)
rExpSeq )
. (k
+ 2)))
>=
0
proof
let k be
Element of
NAT , x be
Element of
REAL ;
assume that
A1: k is
odd and
A2: x
>
0 and
A3: x
<= 1;
consider m be
Nat such that
A4: k
= ((2
* m)
+ 1) by
A1,
ABIAN: 9;
set q = (m
+ 1);
A5: (k
+ 2)
= ((2
* q)
+ 1) by
A4;
consider m be
Nat such that
A6: k
= ((2
* m)
+ 1) by
A1,
ABIAN: 9;
A7: for k be
Element of
NAT st k is
even holds ((
- x)
|^ k)
>
0
proof
let k be
Element of
NAT ;
assume k is
even;
then
consider m be
Nat such that
A8: k
= (2
* m) by
ABIAN:def 2;
defpred
J2[
Nat] means ((
- x)
|^ (2
* $1))
>
0 ;
A9:
J2[
0 ] by
NEWTON: 4;
A10: for k be
Nat st
J2[k] holds
J2[(k
+ 1)]
proof
let k be
Nat;
assume
A11:
J2[k];
((
- x)
|^ (2
* (k
+ 1)))
= ((
- x)
|^ ((2
* k)
+ 2));
then
A12: ((
- x)
|^ (2
* (k
+ 1)))
= (((
- x)
|^ (2
* k))
* ((
- x)
|^ 2)) by
NEWTON: 8;
((
- x)
* (
- x))
>
0 by
A2;
then ((
- x)
|^ 2)
>
0 by
NEWTON: 81;
hence thesis by
A11,
A12;
end;
for k be
Nat holds
J2[k] from
NAT_1:sch 2(
A9,
A10);
hence thesis by
A8;
end;
A13: ((x
|^ (k
+ 2))
/ ((
- x)
|^ (k
+ 1)))
= x
proof
(x
|^ (k
+ 2))
= (x
|^ ((k
+ 1)
+ 1));
then (x
|^ (k
+ 2))
= ((x
|^ (k
+ 1))
* x) by
NEWTON: 6;
then (x
|^ (k
+ 2))
= (x
* ((
- x)
|^ (k
+ 1))) by
A6,
POWER: 1;
then ((x
|^ (k
+ 2))
/ ((
- x)
|^ (k
+ 1)))
= ((x
* ((
- x)
|^ (k
+ 1)))
* (((
- x)
|^ (k
+ 1))
" )) by
XCMPLX_0:def 9;
then
A15: ((x
|^ (k
+ 2))
/ ((
- x)
|^ (k
+ 1)))
= (x
* (((
- x)
|^ (k
+ 1))
* (((
- x)
|^ (k
+ 1))
" )));
(((
- x)
|^ (k
+ 1))
* (((
- x)
|^ (k
+ 1))
" ))
= 1
proof
A17: 1
<= (((
- x)
|^ (k
+ 1))
/ ((
- x)
|^ (k
+ 1))) by
A6,
A7,
XREAL_1: 181;
0
< ((
- x)
|^ (k
+ 1)) by
A6,
A7;
then
A18: (((
- x)
|^ (k
+ 1))
/ ((
- x)
|^ (k
+ 1)))
<= 1 by
XREAL_1: 185;
(((
- x)
|^ (k
+ 1))
/ ((
- x)
|^ (k
+ 1)))
= 1 by
A17,
A18,
XXREAL_0: 1;
hence thesis by
XCMPLX_0:def 9;
end;
hence thesis by
A15;
end;
A19: 1
<= (((k
+ 2)
! )
/ ((k
+ 1)
! ))
proof
((k
+ 2)
! )
= (((k
+ 1)
+ 1)
* ((k
+ 1)
! )) by
NEWTON: 15;
then
A20: (((k
+ 2)
! )
* (((k
+ 1)
! )
" ))
= (((k
+ 1)
+ 1)
* (((k
+ 1)
! )
* (((k
+ 1)
! )
" )));
A21: 1
<= (((k
+ 1)
! )
/ ((k
+ 1)
! )) by
XREAL_1: 181;
(((k
+ 1)
! )
/ ((k
+ 1)
! ))
<= 1 by
XREAL_1: 183;
then (((k
+ 1)
! )
/ ((k
+ 1)
! ))
= 1 by
A21,
XXREAL_0: 1;
then (((k
+ 2)
! )
* (((k
+ 1)
! )
" ))
= (((k
+ 1)
+ 1)
* 1) by
A20,
XCMPLX_0:def 9;
then (((k
+ 2)
! )
* (((k
+ 1)
! )
" ))
>= 1 by
NAT_1: 11;
hence thesis by
XCMPLX_0:def 9;
end;
((x
|^ (k
+ 2))
/ ((
- x)
|^ (k
+ 1)))
<= (((k
+ 2)
! )
/ ((k
+ 1)
! )) implies ((((
- x)
rExpSeq )
. (k
+ 1))
+ (((
- x)
rExpSeq )
. (k
+ 2)))
>=
0
proof
assume ((x
|^ (k
+ 2))
/ ((
- x)
|^ (k
+ 1)))
<= (((k
+ 2)
! )
/ ((k
+ 1)
! ));
then ((x
|^ (k
+ 2))
* (((
- x)
|^ (k
+ 1))
" ))
<= (((k
+ 2)
! )
/ ((k
+ 1)
! )) by
XCMPLX_0:def 9;
then
A24: ((x
|^ (k
+ 2))
* (((
- x)
|^ (k
+ 1))
" ))
<= ((((k
+ 1)
! )
" )
* ((k
+ 2)
! )) by
XCMPLX_0:def 9;
((
- x)
|^ (k
+ 1))
>
0 by
A6,
A7;
then
A25: ((x
|^ (k
+ 2))
/ ((k
+ 2)
! ))
<= ((((k
+ 1)
! )
" )
/ (((
- x)
|^ (k
+ 1))
" )) by
A24,
XREAL_1: 102;
A26: ((((k
+ 1)
! )
" )
* 1)
= (1
/ ((k
+ 1)
! )) by
XCMPLX_0:def 9;
((((k
+ 1)
! )
" )
/ (((
- x)
|^ (k
+ 1))
" ))
= ((1
/ ((k
+ 1)
! ))
* ((((
- x)
|^ (k
+ 1))
" )
" )) & (1
* (((k
+ 1)
! )
" ))
= (1
/ ((k
+ 1)
! )) by
A26,
XCMPLX_0:def 9;
then
A27: ((((k
+ 1)
! )
" )
/ (((
- x)
|^ (k
+ 1))
" ))
= (((
- x)
|^ (k
+ 1))
/ ((k
+ 1)
! )) by
XCMPLX_0:def 9;
((x
rExpSeq )
. (k
+ 2))
<= (((
- x)
|^ (k
+ 1))
/ ((k
+ 1)
! )) by
A25,
A27,
SIN_COS:def 5;
then ((x
rExpSeq )
. (k
+ 2))
<= (((
- x)
rExpSeq )
. (k
+ 1)) by
SIN_COS:def 5;
then (((x
rExpSeq )
. (k
+ 2))
- (((
- x)
rExpSeq )
. (k
+ 1)))
<= ((((
- x)
rExpSeq )
. (k
+ 1))
- (((
- x)
rExpSeq )
. (k
+ 1))) by
XREAL_1: 9;
then
A28: (((x
rExpSeq )
. (k
+ 2))
- (((
- x)
rExpSeq )
. (k
+ 1)))
<=
0 & (
- (((x
rExpSeq )
. (k
+ 2))
- (((
- x)
rExpSeq )
. (k
+ 1))))
>=
0 ;
(
- ((x
rExpSeq )
. (k
+ 2)))
= (((
- x)
rExpSeq )
. (k
+ 2))
proof
defpred
J3[
Nat] means (
- (x
|^ ((2
* $1)
+ 1)))
= ((
- x)
|^ ((2
* $1)
+ 1));
A30:
J3[
0 ];
A31: for k be
Nat st
J3[k] holds
J3[(k
+ 1)]
proof
let k be
Nat;
assume
A32:
J3[k];
(
- (x
|^ ((2
* (k
+ 1))
+ 1)))
= (
- ((x
|^ (((2
* k)
+ 1)
+ 1))
* x)) by
NEWTON: 6;
then (
- (x
|^ ((2
* (k
+ 1))
+ 1)))
= (
- (((x
|^ ((2
* k)
+ 1))
* x)
* x)) by
NEWTON: 6;
then (
- (x
|^ ((2
* (k
+ 1))
+ 1)))
= ((((
- x)
|^ ((2
* k)
+ 1))
* (
- x))
* (
- x)) by
A32;
then (
- (x
|^ ((2
* (k
+ 1))
+ 1)))
= (((
- x)
|^ (((2
* k)
+ 1)
+ 1))
* (
- x)) by
NEWTON: 6;
hence thesis by
NEWTON: 6;
end;
A33: for k be
Nat holds
J3[k] from
NAT_1:sch 2(
A30,
A31);
consider m be
Element of
NAT such that
A34: (k
+ 2)
= ((2
* m)
+ 1) by
A5;
A35: (
- (x
|^ (k
+ 2)))
= ((
- x)
|^ (k
+ 2)) by
A33,
A34;
(
- ((x
rExpSeq )
. (k
+ 2)))
= (
- ((x
|^ (k
+ 2))
/ ((k
+ 2)
! ))) by
SIN_COS:def 5;
then (
- ((x
rExpSeq )
. (k
+ 2)))
= (
- ((x
|^ (k
+ 2))
* (((k
+ 2)
! )
" ))) by
XCMPLX_0:def 9;
then (
- ((x
rExpSeq )
. (k
+ 2)))
= ((
- (x
|^ (k
+ 2)))
* (((k
+ 2)
! )
" ));
then (
- ((x
rExpSeq )
. (k
+ 2)))
= ((
- (x
|^ (k
+ 2)))
/ ((k
+ 2)
! )) by
XCMPLX_0:def 9;
hence thesis by
A35,
SIN_COS:def 5;
end;
hence thesis by
A28;
end;
hence thesis by
A3,
A19,
A13,
XXREAL_0: 2;
end;
theorem ::
BOR_CANT:2
Th2: for x be
Element of
REAL holds (1
+ x)
<= (
exp_R
. x)
proof
let x be
Element of
REAL ;
per cases ;
suppose
A1: x
>
0 ;
reconsider 1x = (1
+ x) as
Element of
REAL by
XREAL_0:def 1;
set B2 = (
NAT
--> 1x);
A2: for n be
Nat st x
>
0 holds (B2
. n)
<= ((
Partial_Sums (x
rExpSeq ))
. (n
+ 1))
proof
let n be
Nat;
defpred
J[
Nat] means (B2
. $1)
<= ((
Partial_Sums (x
rExpSeq ))
. (1
+ $1));
((
Partial_Sums (x
rExpSeq ))
. 1)
= (((
Partial_Sums (x
rExpSeq ))
.
0 )
+ ((x
rExpSeq )
. (
0
+ 1))) by
SERIES_1:def 1;
then
A3: ((
Partial_Sums (x
rExpSeq ))
. 1)
= (((x
rExpSeq )
.
0 )
+ ((x
rExpSeq )
. 1)) by
SERIES_1:def 1;
A4: ((x
rExpSeq )
.
0 )
= ((x
|^
0 )
/ (
0
! )) by
SIN_COS:def 5
.= 1 by
NEWTON: 4,
NEWTON: 12;
((x
rExpSeq )
. 1)
= ((x
|^ 1)
/ (1
! )) by
SIN_COS:def 5;
then
A5:
J[
0 ] by
A4,
A3,
NEWTON: 13;
A6: for k be
Nat st
J[k] holds
J[(k
+ 1)]
proof
let k be
Nat;
assume
A7:
J[k];
A8: ((
Partial_Sums (x
rExpSeq ))
. (1
+ (k
+ 1)))
= (((
Partial_Sums (x
rExpSeq ))
. (k
+ 1))
+ ((x
rExpSeq )
. ((k
+ 1)
+ 1))) by
SERIES_1:def 1;
A9: ((x
rExpSeq )
. ((k
+ 1)
+ 1))
>
0
proof
(x
|^ ((k
+ 1)
+ 1))
>
0 & (((k
+ 1)
+ 1)
! )
>
0 by
A1,
NEWTON: 83;
then ((x
|^ ((k
+ 1)
+ 1))
/ (((k
+ 1)
+ 1)
! ))
>
0 ;
hence thesis by
SIN_COS:def 5;
end;
A10: (1
+ x)
<= ((
Partial_Sums (x
rExpSeq ))
. (k
+ 1)) by
A7,
FUNCOP_1: 7,
ORDINAL1:def 12;
((
Partial_Sums (x
rExpSeq ))
. (k
+ 1))
<= (((x
rExpSeq )
. ((k
+ 1)
+ 1))
+ ((
Partial_Sums (x
rExpSeq ))
. (k
+ 1))) by
A9,
XREAL_1: 31;
hence thesis by
A8,
A10,
XXREAL_0: 2;
end;
for k be
Nat holds
J[k] from
NAT_1:sch 2(
A5,
A6);
hence thesis;
end;
A11: (B2
. n)
<= (((
Partial_Sums (x
rExpSeq ))
^\ 1)
. n)
proof
(B2
. n)
<= ((
Partial_Sums (x
rExpSeq ))
. (n
+ 1)) by
A1,
A2;
hence thesis by
NAT_1:def 3;
end;
A12: (
lim B2)
= (B2
. 1) by
SEQ_4: 26
.= (1
+ x);
A13: (
Partial_Sums (x
rExpSeq )) is
convergent by
SERIES_1:def 2,
SIN_COS: 45;
then
A14: (
lim ((
Partial_Sums (x
rExpSeq ))
^\ 1))
= (
lim (
Partial_Sums (x
rExpSeq ))) & ((
Partial_Sums (x
rExpSeq ))
^\ 1) is
convergent by
SEQ_4: 20;
(
lim B2)
<= (
lim ((
Partial_Sums (x
rExpSeq ))
^\ 1)) by
A13,
A11,
SEQ_2: 18;
then (
lim B2)
<= (
Sum (x
rExpSeq )) by
A14,
SERIES_1:def 3;
hence thesis by
A12,
SIN_COS:def 22;
end;
suppose x
=
0 ;
hence thesis by
SIN_COS: 51;
end;
suppose
A15: x
<
0 ;
set y = (
- x);
(1
- y)
<= (
exp_R
. (
- y))
proof
per cases ;
suppose
A16: y
<= 1;
for x be
Element of
REAL st x
>
0 & x
<= 1 holds (1
- x)
<= (
exp_R
. (
- x))
proof
let x be
Element of
REAL ;
assume that
A17: x
>
0 and
A18: x
<= 1;
reconsider 1x = (1
- x) as
Element of
REAL by
XREAL_0:def 1;
set B2 = (
NAT
--> 1x);
A19: for n be
Nat holds (B2
. n)
<= ((
Partial_Sums ((
- x)
rExpSeq ))
. (n
+ 1))
proof
let n be
Nat;
defpred
J[
Nat] means (B2
. $1)
<= ((
Partial_Sums ((
- x)
rExpSeq ))
. ($1
+ 1));
((
Partial_Sums ((
- x)
rExpSeq ))
. (
0
+ 1))
= (((
Partial_Sums ((
- x)
rExpSeq ))
.
0 )
+ (((
- x)
rExpSeq )
. 1)) by
SERIES_1:def 1;
then
A20: ((
Partial_Sums ((
- x)
rExpSeq ))
. (
0
+ 1))
= ((((
- x)
rExpSeq )
.
0 )
+ (((
- x)
rExpSeq )
. 1)) by
SERIES_1:def 1;
(((
- x)
rExpSeq )
. 1)
= (((
- x)
|^ 1)
/ (1
! )) by
SIN_COS:def 5;
then
A21: (((
- x)
rExpSeq )
. 1)
= (
- x) by
NEWTON: 13;
(((
- x)
rExpSeq )
.
0 )
= (((
- x)
|^
0 )
/ (
0
! )) by
SIN_COS:def 5
.= 1 by
NEWTON: 4,
NEWTON: 12;
then
A22:
J[
0 ] by
A21,
A20;
A23: for k be
Nat st
J[k] holds
J[(k
+ 1)]
proof
let k be
Nat;
assume
A24:
J[k];
per cases ;
suppose k is
even;
then
consider m be
Nat such that
A25: k
= (2
* m) by
ABIAN:def 2;
A26: (1
- x)
<= ((
Partial_Sums ((
- x)
rExpSeq ))
. (k
+ 1)) by
A24,
FUNCOP_1: 7,
ORDINAL1:def 12;
A27: for k be
Element of
NAT st k is
even & k
>
0 holds for y be
Real holds ((y
rExpSeq )
. k)
>=
0
proof
let k be
Element of
NAT ;
assume that
A28: k is
even and
A29: k
>
0 ;
let y be
Real;
per cases ;
suppose y
>
0 ;
then (y
|^ k)
>
0 by
NEWTON: 83;
then ((y
|^ k)
/ (k
! ))
>
0 ;
hence thesis by
SIN_COS:def 5;
end;
suppose y
=
0 ;
then (y
|^ k)
=
0 by
A29,
NEWTON: 84;
then ((y
|^ k)
/ (k
! ))
=
0 ;
hence thesis by
SIN_COS:def 5;
end;
suppose
A31: y
<
0 ;
consider m be
Nat such that
A32: k
= (2
* m) by
A28,
ABIAN:def 2;
(y
|^ k)
= (y
|^ (m
+ m)) by
A32;
then (y
|^ k)
= ((y
|^ m)
* (y
|^ m)) by
NEWTON: 8;
then (y
|^ k)
= ((y
* y)
|^ m) by
NEWTON: 7;
then (y
|^ k)
>=
0 by
A31,
NEWTON: 83;
then ((y
|^ k)
/ (k
! ))
>=
0 ;
hence thesis by
SIN_COS:def 5;
end;
end;
(((
- x)
rExpSeq )
. (k
+ 2))
>=
0 by
A25,
A27;
then
A35: ((
Partial_Sums ((
- x)
rExpSeq ))
. (k
+ 1))
<= (((
Partial_Sums ((
- x)
rExpSeq ))
. (k
+ 1))
+ (((
- x)
rExpSeq )
. (k
+ 2))) by
XREAL_1: 31;
(1
- x)
<= (((
Partial_Sums ((
- x)
rExpSeq ))
. (k
+ 1))
+ (((
- x)
rExpSeq )
. ((k
+ 1)
+ 1))) by
A26,
A35,
XXREAL_0: 2;
hence thesis by
SERIES_1:def 1;
end;
suppose k is
odd;
then
consider m be
Nat such that
A36: k
= ((2
* m)
+ 1) by
ABIAN: 9;
for k be
Element of
NAT , x be
Element of
REAL st k is
odd & x
>
0 & x
<= 1 holds (1
- x)
<= ((
Partial_Sums ((
- x)
rExpSeq ))
. k)
proof
let k be
Element of
NAT , x be
Element of
REAL ;
assume
A38: k is
odd;
assume
A39: x
>
0 ;
assume
A40: x
<= 1;
defpred
J[
Nat] means (1
- x)
<= ((
Partial_Sums ((
- x)
rExpSeq ))
. ((2
* $1)
+ 1));
((
Partial_Sums ((
- x)
rExpSeq ))
. ((2
*
0 )
+ 1))
= (((
Partial_Sums ((
- x)
rExpSeq ))
.
0 )
+ (((
- x)
rExpSeq )
. 1)) by
SERIES_1:def 1;
then
A41: ((
Partial_Sums ((
- x)
rExpSeq ))
. ((2
*
0 )
+ 1))
= ((((
- x)
rExpSeq )
.
0 )
+ (((
- x)
rExpSeq )
. 1)) by
SERIES_1:def 1;
A42: (((
- x)
rExpSeq )
.
0 )
= (((
- x)
|^
0 )
/ (
0
! )) by
SIN_COS:def 5
.= 1 by
NEWTON: 4,
NEWTON: 12;
(((
- x)
rExpSeq )
. 1)
= (((
- x)
|^ 1)
/ (1
! )) by
SIN_COS:def 5;
then
A44:
J[
0 ] by
A41,
A42,
NEWTON: 13;
A45: for k be
Nat st
J[k] holds
J[(k
+ 1)]
proof
let k be
Nat;
assume
A46:
J[k];
((
Partial_Sums ((
- x)
rExpSeq ))
. ((2
* k)
+ 1))
<= ((
Partial_Sums ((
- x)
rExpSeq ))
. ((2
* k)
+ 3))
proof
((
Partial_Sums ((
- x)
rExpSeq ))
. ((2
* k)
+ 3))
= (((
Partial_Sums ((
- x)
rExpSeq ))
. ((2
* k)
+ 2))
+ (((
- x)
rExpSeq )
. (((2
* k)
+ 2)
+ 1))) by
SERIES_1:def 1;
then ((
Partial_Sums ((
- x)
rExpSeq ))
. ((2
* k)
+ 3))
= (((
Partial_Sums ((
- x)
rExpSeq ))
. (((2
* k)
+ 1)
+ 1))
+ (((
- x)
rExpSeq )
. ((2
* k)
+ 3)));
then ((
Partial_Sums ((
- x)
rExpSeq ))
. ((2
* k)
+ 3))
= ((((
Partial_Sums ((
- x)
rExpSeq ))
. ((2
* k)
+ 1))
+ (((
- x)
rExpSeq )
. ((2
* k)
+ 2)))
+ (((
- x)
rExpSeq )
. ((2
* k)
+ 3))) by
SERIES_1:def 1;
then
A47: ((
Partial_Sums ((
- x)
rExpSeq ))
. ((2
* k)
+ 3))
= (((
Partial_Sums ((
- x)
rExpSeq ))
. ((2
* k)
+ 1))
+ ((((
- x)
rExpSeq )
. ((2
* k)
+ 2))
+ (((
- x)
rExpSeq )
. ((2
* k)
+ 3))));
((((
- x)
rExpSeq )
. (((2
* k)
+ 1)
+ 1))
+ (((
- x)
rExpSeq )
. (((2
* k)
+ 1)
+ 2)))
>=
0 by
A39,
A40,
Th1;
hence thesis by
A47,
XREAL_1: 31;
end;
hence thesis by
A46,
XXREAL_0: 2;
end;
A48: for k be
Nat holds
J[k] from
NAT_1:sch 2(
A44,
A45);
consider m be
Nat such that
A49: k
= ((2
* m)
+ 1) by
A38,
ABIAN: 9;
thus thesis by
A48,
A49;
end;
hence thesis by
A36,
A17,
A18;
end;
end;
for k be
Nat holds
J[k] from
NAT_1:sch 2(
A22,
A23);
hence thesis;
end;
A50: for n be
Nat holds (B2
. n)
<= (((
Partial_Sums ((
- x)
rExpSeq ))
^\ 1)
. n)
proof
let n be
Nat;
(B2
. n)
<= ((
Partial_Sums ((
- x)
rExpSeq ))
. (n
+ 1)) by
A19;
hence thesis by
NAT_1:def 3;
end;
A51: (
lim B2)
= (B2
. 1) by
SEQ_4: 26
.= (1
- x);
A52: (
Partial_Sums ((
- x)
rExpSeq )) is
convergent by
SERIES_1:def 2,
SIN_COS: 45;
then
A53: (
lim ((
Partial_Sums ((
- x)
rExpSeq ))
^\ 1))
= (
lim (
Partial_Sums ((
- x)
rExpSeq ))) & ((
Partial_Sums ((
- x)
rExpSeq ))
^\ 1) is
convergent by
SEQ_4: 20;
(
lim B2)
<= (
lim ((
Partial_Sums ((
- x)
rExpSeq ))
^\ 1)) by
A52,
A50,
SEQ_2: 18;
then (
lim B2)
<= (
Sum ((
- x)
rExpSeq )) by
A53,
SERIES_1:def 3;
hence thesis by
A51,
SIN_COS:def 22;
end;
hence thesis by
A15,
A16;
end;
suppose
A54: y
> 1;
then
0
< (
exp_R
. (
- y)) by
SIN_COS: 53;
hence thesis by
A54,
XREAL_1: 49;
end;
end;
hence thesis;
end;
end;
definition
let s be
Real_Sequence;
::
BOR_CANT:def1
func
JSum (s) ->
Real_Sequence means
:
Def1: for d be
Nat holds (it
. d)
= (
Sum ((
- (s
. d))
rExpSeq ));
existence
proof
deffunc
U(
Nat) = (
In ((
Sum ((
- (s
. $1))
rExpSeq )),
REAL ));
consider f be
Real_Sequence such that
A1: for d be
Element of
NAT holds (f
. d)
=
U(d) from
FUNCT_2:sch 4;
take f;
let d be
Nat;
d
in
NAT by
ORDINAL1:def 12;
then (f
. d)
=
U(d) by
A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
Real_Sequence;
assume that
A2: for d be
Nat holds (f1
. d)
= (
Sum ((
- (s
. d))
rExpSeq )) and
A3: for d be
Nat holds (f2
. d)
= (
Sum ((
- (s
. d))
rExpSeq ));
let d be
Element of
NAT ;
(f1
. d)
= (
Sum ((
- (s
. d))
rExpSeq )) by
A2;
hence thesis by
A3;
end;
end
theorem ::
BOR_CANT:3
Th3: ((
Partial_Product (
JSum (Prob
* A)))
. n)
= (
exp_R
. (
- ((
Partial_Sums (Prob
* A))
. n)))
proof
defpred
J[
Nat] means (
exp_R
. (
- ((
Partial_Sums (Prob
* A))
. $1)))
= ((
Partial_Product (
JSum (Prob
* A)))
. $1);
A1: (
exp_R
. (
- ((
Partial_Sums (Prob
* A))
.
0 )))
= (
exp_R
. (
- ((Prob
* A)
.
0 ))) by
SERIES_1:def 1;
((
Partial_Product (
JSum (Prob
* A)))
.
0 )
= ((
JSum (Prob
* A))
.
0 ) by
SERIES_3:def 1;
then ((
Partial_Product (
JSum (Prob
* A)))
.
0 )
= (
Sum ((
- ((Prob
* A)
.
0 ))
rExpSeq )) by
Def1;
then
A2:
J[
0 ] by
A1,
SIN_COS:def 22;
A3: for k be
Nat st
J[k] holds
J[(k
+ 1)]
proof
let k be
Nat;
assume
A4:
J[k];
((
Partial_Product (
JSum (Prob
* A)))
. (k
+ 1))
= (((
Partial_Product (
JSum (Prob
* A)))
. k)
* ((
JSum (Prob
* A))
. (k
+ 1))) by
SERIES_3:def 1;
then
A6: ((
Partial_Product (
JSum (Prob
* A)))
. (k
+ 1))
= ((
exp_R
. (
- ((
Partial_Sums (Prob
* A))
. k)))
* (
Sum ((
- ((Prob
* A)
. (k
+ 1)))
rExpSeq ))) by
A4,
Def1;
A7: ((
exp_R (
- ((
Partial_Sums (Prob
* A))
. k)))
* (
exp_R (
- ((Prob
* A)
. (k
+ 1)))))
= (
exp_R ((
- ((
Partial_Sums (Prob
* A))
. k))
+ (
- ((Prob
* A)
. (k
+ 1))))) by
SIN_COS: 50;
(
- (((
Partial_Sums (Prob
* A))
. k)
+ ((Prob
* A)
. (k
+ 1))))
= (
- ((
Partial_Sums (Prob
* A))
. (k
+ 1))) by
SERIES_1:def 1;
hence thesis by
A7,
A6,
SIN_COS:def 22;
end;
for k be
Nat holds
J[k] from
NAT_1:sch 2(
A2,
A3);
hence thesis;
end;
theorem ::
BOR_CANT:4
Th4: ((
Partial_Product (Prob
* (
Complement A)))
. n)
<= ((
Partial_Product (
JSum (Prob
* A)))
. n)
proof
defpred
J[
Nat] means ((
Partial_Product (Prob
* (
Complement A)))
. $1)
<= ((
Partial_Product (
JSum (Prob
* A)))
. $1);
A1: ((
Partial_Product (Prob
* (
Complement A)))
.
0 )
= ((Prob
* (
Complement A))
.
0 ) by
SERIES_3:def 1;
(
dom (Prob
* (
Complement A)))
=
NAT by
FUNCT_2:def 1;
then
A2: ((Prob
* (
Complement A))
.
0 )
= (Prob
. ((
Complement A)
.
0 )) by
FUNCT_1: 12;
A3: ((
Partial_Product (Prob
* (
Complement A)))
.
0 )
= (Prob
. ((A
.
0 )
` )) by
A2,
A1,
PROB_1:def 2;
(Prob
. ((A
.
0 )
` ))
= (Prob
. ((
[#] Sigma)
\ (A
.
0 ))) by
SUBSET_1:def 4;
then
A4: ((
Partial_Product (Prob
* (
Complement A)))
.
0 )
= (1
- (Prob
. (A
.
0 ))) by
A3,
PROB_1: 32;
((
Partial_Product (
JSum (Prob
* A)))
.
0 )
= ((
JSum (Prob
* A))
.
0 ) by
SERIES_3:def 1;
then ((
Partial_Product (
JSum (Prob
* A)))
.
0 )
= (
Sum ((
- ((Prob
* A)
.
0 ))
rExpSeq )) by
Def1;
then
A5: ((
Partial_Product (
JSum (Prob
* A)))
.
0 )
= (
exp_R
. (
- ((Prob
* A)
.
0 ))) by
SIN_COS:def 22;
A6: (
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
(1
+ (
- (Prob
. (A
.
0 ))))
<= (
exp_R
. (
- (Prob
. (A
.
0 )))) by
Th2;
then
A7:
J[
0 ] by
A4,
A6,
A5,
FUNCT_1: 12;
A8: for k be
Nat st
J[k] holds
J[(k
+ 1)]
proof
let k be
Nat;
assume
A9:
J[k];
(Prob
. ((
Complement A)
. (k
+ 1)))
= (Prob
. ((A
. (k
+ 1))
` )) & ((A
. (k
+ 1))
` )
= ((
[#] Sigma)
\ (A
. (k
+ 1))) by
PROB_1:def 2,
SUBSET_1:def 4;
then
A10: (Prob
. ((
Complement A)
. (k
+ 1)))
= (1
- (Prob
. (A
. (k
+ 1)))) by
PROB_1: 32;
A11: (1
+ (
- (Prob
. (A
. (k
+ 1)))))
<= (
exp_R
. (
- (Prob
. (A
. (k
+ 1))))) by
Th2;
(
dom (Prob
* (
Complement A)))
=
NAT by
FUNCT_2:def 1;
then
A12: ((Prob
* (
Complement A))
. (k
+ 1))
<= (
exp_R
. (
- (Prob
. (A
. (k
+ 1))))) by
A11,
A10,
FUNCT_1: 12;
A13: (((Prob
* (
Complement A))
. (k
+ 1))
* ((
Partial_Product (
JSum (Prob
* A)))
. k))
<= ((
exp_R
. (
- (Prob
. (A
. (k
+ 1)))))
* ((
Partial_Product (
JSum (Prob
* A)))
. k))
proof
for n be
Nat holds ((
JSum (Prob
* A))
. n)
>
0
proof
let n be
Nat;
A14: (
exp_R
. (
- ((Prob
* A)
. n)))
>
0 by
SIN_COS: 54;
((
JSum (Prob
* A))
. n)
= (
Sum ((
- ((Prob
* A)
. n))
rExpSeq )) by
Def1;
hence thesis by
A14,
SIN_COS:def 22;
end;
then ((
Partial_Product (
JSum (Prob
* A)))
. k)
>
0 by
SERIES_3: 43;
hence thesis by
A12,
XREAL_1: 64;
end;
A15: (((
Partial_Product (Prob
* (
Complement A)))
. k)
* ((Prob
* (
Complement A))
. (k
+ 1)))
<= (((
Partial_Product (
JSum (Prob
* A)))
. k)
* ((Prob
* (
Complement A))
. (k
+ 1)))
proof
for n be
Element of
NAT holds ((Prob
* (
Complement A))
. n)
>=
0
proof
let n be
Element of
NAT ;
A16: (Prob
. ((
Complement A)
. n))
>=
0 by
PROB_1:def 8;
(
dom (Prob
* (
Complement A)))
=
NAT by
FUNCT_2:def 1;
hence thesis by
A16,
FUNCT_1: 12;
end;
then ((Prob
* (
Complement A))
. (k
+ 1))
>=
0 ;
hence thesis by
A9,
XREAL_1: 64;
end;
(((
Partial_Product (Prob
* (
Complement A)))
. k)
* ((Prob
* (
Complement A))
. (k
+ 1)))
<= ((
exp_R
. (
- (Prob
. (A
. (k
+ 1)))))
* ((
Partial_Product (
JSum (Prob
* A)))
. k)) by
A15,
A13,
XXREAL_0: 2;
then ((
Partial_Product (Prob
* (
Complement A)))
. (k
+ 1))
<= ((
exp_R
. (
- (Prob
. (A
. (k
+ 1)))))
* ((
Partial_Product (
JSum (Prob
* A)))
. k)) by
SERIES_3:def 1;
then ((
Partial_Product (Prob
* (
Complement A)))
. (k
+ 1))
<= ((
Sum ((
- (Prob
. (A
. (k
+ 1))))
rExpSeq ))
* ((
Partial_Product (
JSum (Prob
* A)))
. k)) by
SIN_COS:def 22;
then ((
Partial_Product (Prob
* (
Complement A)))
. (k
+ 1))
<= ((
Sum ((
- (Prob
. (A
. (k
+ 1))))
rExpSeq ))
* (
exp_R
. (
- ((
Partial_Sums (Prob
* A))
. k)))) by
Th3;
then ((
Partial_Product (Prob
* (
Complement A)))
. (k
+ 1))
<= ((
exp_R (
- (Prob
. (A
. (k
+ 1)))))
* (
exp_R (
- ((
Partial_Sums (Prob
* A))
. k)))) by
SIN_COS:def 22;
then
A17: ((
Partial_Product (Prob
* (
Complement A)))
. (k
+ 1))
<= (
exp_R ((
- (Prob
. (A
. (k
+ 1))))
+ (
- ((
Partial_Sums (Prob
* A))
. k)))) by
SIN_COS: 50;
(
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* A)
. (k
+ 1))
= (Prob
. (A
. (k
+ 1))) by
FUNCT_1: 12;
then ((
- (Prob
. (A
. (k
+ 1))))
+ (
- ((
Partial_Sums (Prob
* A))
. k)))
= (
- (((Prob
* A)
. (k
+ 1))
+ ((
Partial_Sums (Prob
* A))
. k)));
then ((
Partial_Product (Prob
* (
Complement A)))
. (k
+ 1))
<= (
exp_R
. (
- ((
Partial_Sums (Prob
* A))
. (k
+ 1)))) by
A17,
SERIES_1:def 1;
hence thesis by
Th3;
end;
for k be
Nat holds
J[k] from
NAT_1:sch 2(
A7,
A8);
hence thesis;
end;
definition
let n1,n2 be
Nat;
::
BOR_CANT:def2
func
Special_Function (n1,n2) ->
sequence of
NAT means
:
Def2: for n be
Nat holds (it
. n)
= (
IFGT (n,n1,(n
+ n2),n));
existence
proof
deffunc
U(
Nat) = (
In ((
IFGT ($1,n1,($1
+ n2),$1)),
NAT ));
consider f be
sequence of
NAT such that
A1: for n be
Element of
NAT holds (f
. n)
=
U(n) from
FUNCT_2:sch 4;
take f;
let n;
n
in
NAT by
ORDINAL1:def 12;
hence (f
. n)
=
U(n) by
A1
.= (
IFGT (n,n1,(n
+ n2),n));
end;
uniqueness
proof
let s1,s2 be
sequence of
NAT ;
assume that
A2: for n be
Nat holds (s1
. n)
= (
IFGT (n,n1,(n
+ n2),n)) and
A3: for n be
Nat holds (s2
. n)
= (
IFGT (n,n1,(n
+ n2),n));
let n be
Element of
NAT ;
(s1
. n)
= (
IFGT (n,n1,(n
+ n2),n)) & (s2
. n)
= (
IFGT (n,n1,(n
+ n2),n)) by
A2,
A3;
hence thesis;
end;
end
definition
let k be
Nat;
::
BOR_CANT:def3
func
Special_Function2 (k) ->
sequence of
NAT means
:
Def3: for n be
Nat holds (it
. n)
= (n
+ k);
existence
proof
deffunc
U(
Nat) = (
In (($1
+ k),
NAT ));
consider f be
sequence of
NAT such that
A1: for n be
Element of
NAT holds (f
. n)
=
U(n) from
FUNCT_2:sch 4;
take f;
let n be
Nat;
n
in
NAT by
ORDINAL1:def 12;
then (f
. n)
=
U(n) by
A1;
hence thesis;
end;
uniqueness
proof
let s1,s2 be
sequence of
NAT ;
assume that
A2: for n be
Nat holds (s1
. n)
= (n
+ k) and
A3: for n be
Nat holds (s2
. n)
= (n
+ k);
let n be
Element of
NAT ;
(s1
. n)
= (n
+ k) & (s2
. n)
= (n
+ k) by
A2,
A3;
hence thesis;
end;
end
definition
let k be
Nat;
::
BOR_CANT:def4
func
Special_Function3 (k) ->
sequence of
NAT means
:
Def4: for n be
Nat holds (it
. n)
= (
IFGT (n,k,
0 ,1));
existence
proof
deffunc
U(
Nat) = (
IFGT ($1,k,
0 ,1));
consider f be
sequence of
NAT such that
A1: for n be
Element of
NAT holds (f
. n)
=
U(n) from
FUNCT_2:sch 4;
take f;
let n be
Nat;
n
in
NAT by
ORDINAL1:def 12;
hence thesis by
A1;
end;
uniqueness
proof
let s1,s2 be
sequence of
NAT ;
assume that
A2: for n be
Nat holds (s1
. n)
= (
IFGT (n,k,
0 ,1)) and
A3: for n be
Nat holds (s2
. n)
= (
IFGT (n,k,
0 ,1));
let n be
Element of
NAT ;
(s1
. n)
= (
IFGT (n,k,
0 ,1)) & (s2
. n)
= (
IFGT (n,k,
0 ,1)) by
A2,
A3;
hence thesis;
end;
end
definition
let n1,n2 be
Nat;
::
BOR_CANT:def5
func
Special_Function4 (n1,n2) ->
sequence of
NAT means
:
Def5: for n be
Nat holds (it
. n)
= (
IFGT (n,(n1
+ 1),(n
+ n2),n));
existence
proof
deffunc
U(
Nat) = (
In ((
IFGT ($1,(n1
+ 1),($1
+ n2),$1)),
NAT ));
consider f be
sequence of
NAT such that
A1: for n be
Element of
NAT holds (f
. n)
=
U(n) from
FUNCT_2:sch 4;
take f;
let n be
Nat;
n
in
NAT by
ORDINAL1:def 12;
then (f
. n)
=
U(n) by
A1;
hence thesis;
end;
uniqueness
proof
let s1,s2 be
sequence of
NAT ;
assume that
A2: for n be
Nat holds (s1
. n)
= (
IFGT (n,(n1
+ 1),(n
+ n2),n)) and
A3: for n be
Nat holds (s2
. n)
= (
IFGT (n,(n1
+ 1),(n
+ n2),n));
let n be
Element of
NAT ;
(s1
. n)
= (
IFGT (n,(n1
+ 1),(n
+ n2),n)) & (s2
. n)
= (
IFGT (n,(n1
+ 1),(n
+ n2),n)) by
A2,
A3;
hence thesis;
end;
end
registration
let n1,n2 be
Nat;
cluster (
Special_Function (n1,n2)) ->
one-to-one;
coherence
proof
let x1,x2 be
object;
assume that
A1: x1
in (
dom (
Special_Function (n1,n2))) and
A2: x2
in (
dom (
Special_Function (n1,n2)));
assume
A3: ((
Special_Function (n1,n2))
. x1)
= ((
Special_Function (n1,n2))
. x2);
reconsider x1 as
Element of
NAT by
A1;
reconsider x2 as
Element of
NAT by
A2;
A4: ((
Special_Function (n1,n2))
. x2)
= (
IFGT (x2,n1,(x2
+ n2),x2)) & ((
Special_Function (n1,n2))
. x1)
= (
IFGT (x1,n1,(x1
+ n2),x1)) by
Def2;
per cases ;
suppose x1
<= n1 & x2
<= n1;
then (
IFGT (x2,n1,(x2
+ n2),x2))
= x2 & (
IFGT (x1,n1,(x1
+ n2),x1))
= x1 by
XXREAL_0:def 11;
hence thesis by
A4,
A3;
end;
suppose
A6: x1
<= n1 & x2
> n1;
then (
IFGT (x2,n1,(x2
+ n2),x2))
= (x2
+ n2) by
XXREAL_0:def 11;
then
A7: ((
Special_Function (n1,n2))
. x2)
= (x2
+ n2) by
Def2;
(
IFGT (x1,n1,(x1
+ n2),x1))
= x1 by
A6,
XXREAL_0:def 11;
then
A9: ((
Special_Function (n1,n2))
. x1)
= x1 by
Def2;
x1
<> x2 implies ((
Special_Function (n1,n2))
. x1)
<> ((
Special_Function (n1,n2))
. x2)
proof
assume x1
<> x2;
x1
< x2 &
0
<= n2 by
A6,
XXREAL_0: 2;
hence thesis by
A9,
A7,
XREAL_1: 31;
end;
hence thesis by
A3;
end;
suppose
A10: x2
<= n1 & x1
> n1;
((
Special_Function (n1,n2))
. x1)
= (
IFGT (x1,n1,(x1
+ n2),x1)) by
Def2;
then
A12: ((
Special_Function (n1,n2))
. x1)
= (x1
+ n2) by
A10,
XXREAL_0:def 11;
((
Special_Function (n1,n2))
. x2)
= (
IFGT (x2,n1,(x2
+ n2),x2)) by
Def2;
then
A14: ((
Special_Function (n1,n2))
. x2)
= x2 by
A10,
XXREAL_0:def 11;
x2
<> x1 implies ((
Special_Function (n1,n2))
. x2)
<> ((
Special_Function (n1,n2))
. x1)
proof
assume x2
<> x1;
x2
< x1 &
0
<= n2 by
A10,
XXREAL_0: 2;
hence thesis by
A14,
A12,
XREAL_1: 31;
end;
hence thesis by
A3;
end;
suppose
A15: x1
> n1 & x2
> n1;
(
IFGT (x2,n1,(x2
+ n2),x2))
= (x2
+ n2) & (
IFGT (x1,n1,(x1
+ n2),x1))
= (x1
+ n2) by
A15,
XXREAL_0:def 11;
then (x2
+ n2)
= (x1
+ n2) by
A4,
A3;
hence thesis;
end;
end;
cluster (
Special_Function4 (n1,n2)) ->
one-to-one;
coherence
proof
let x1,x2 be
object;
assume that
A16: x1
in (
dom (
Special_Function4 (n1,n2))) and
A17: x2
in (
dom (
Special_Function4 (n1,n2)));
assume
A18: ((
Special_Function4 (n1,n2))
. x1)
= ((
Special_Function4 (n1,n2))
. x2);
reconsider x1 as
Element of
NAT by
A16;
reconsider x2 as
Element of
NAT by
A17;
per cases ;
suppose
A19: x1
<= (n1
+ 1) & x2
<= (n1
+ 1);
A20: ((
Special_Function4 (n1,n2))
. x2)
= (
IFGT (x2,(n1
+ 1),(x2
+ n2),x2)) & ((
Special_Function4 (n1,n2))
. x1)
= (
IFGT (x1,(n1
+ 1),(x1
+ n2),x1)) by
Def5;
(
IFGT (x2,(n1
+ 1),(x2
+ n2),x2))
= x2 & (
IFGT (x1,(n1
+ 1),(x1
+ n2),x1))
= x1 by
A19,
XXREAL_0:def 11;
hence thesis by
A20,
A18;
end;
suppose
A21: x1
> (n1
+ 1) & x2
<= (n1
+ 1);
((
Special_Function4 (n1,n2))
. x2)
= (
IFGT (x2,(n1
+ 1),(x2
+ n2),x2)) & ((
Special_Function4 (n1,n2))
. x1)
= (
IFGT (x1,(n1
+ 1),(x1
+ n2),x1)) by
Def5;
then
A23: ((
Special_Function4 (n1,n2))
. x2)
= x2 & ((
Special_Function4 (n1,n2))
. x1)
= (x1
+ n2) by
A21,
XXREAL_0:def 11;
x1
<> x2 implies ((
Special_Function4 (n1,n2))
. x2)
<> ((
Special_Function4 (n1,n2))
. x1)
proof
assume x1
<> x2;
((
Special_Function4 (n1,n2))
. x1)
> ((n1
+ 1)
+ n2) & ((n1
+ 1)
+ n2)
>= (n1
+ 1) by
A23,
A21,
XREAL_1: 6,
XREAL_1: 31;
hence thesis by
A21,
A23,
XXREAL_0: 2;
end;
hence thesis by
A18;
end;
suppose
A24: x1
<= (n1
+ 1) & x2
> (n1
+ 1);
then
A25: ((
Special_Function4 (n1,n2))
. x2)
= (
IFGT (x2,(n1
+ 1),(x2
+ n2),x2)) & ((
Special_Function4 (n1,n2))
. x1)
= (
IFGT (x1,(n1
+ 1),(x1
+ n2),x1)) & (
IFGT (x2,(n1
+ 1),(x2
+ n2),x2))
= (x2
+ n2) & (
IFGT (x1,(n1
+ 1),(x1
+ n2),x1))
= x1 by
Def5,
XXREAL_0:def 11;
x1
<> x2 implies (((
Special_Function4 (n1,n2))
. x2)
<> ((
Special_Function4 (n1,n2))
. x1))
proof
assume x1
<> x2;
((
Special_Function4 (n1,n2))
. x2)
> ((n1
+ 1)
+ n2) & ((n1
+ 1)
+ n2)
>= (n1
+ 1) by
A25,
A24,
XREAL_1: 6,
XREAL_1: 31;
hence thesis by
A24,
A25,
XXREAL_0: 2;
end;
hence thesis by
A18;
end;
suppose
A26: x1
> (n1
+ 1) & x2
> (n1
+ 1);
A27: ((
Special_Function4 (n1,n2))
. x2)
= (
IFGT (x2,(n1
+ 1),(x2
+ n2),x2)) & ((
Special_Function4 (n1,n2))
. x1)
= (
IFGT (x1,(n1
+ 1),(x1
+ n2),x1)) by
Def5;
(
IFGT (x2,(n1
+ 1),(x2
+ n2),x2))
= (x2
+ n2) & (
IFGT (x1,(n1
+ 1),(x1
+ n2),x1))
= (x1
+ n2) by
A26,
XXREAL_0:def 11;
then (x1
+ n2)
= (x2
+ n2) by
A27,
A18;
hence thesis;
end;
end;
end
registration
let n be
Nat;
cluster (
Special_Function2 n) ->
one-to-one;
coherence
proof
let x1,x2 be
object;
assume that
A1: x1
in (
dom (
Special_Function2 n)) and
A2: x2
in (
dom (
Special_Function2 n));
assume
A3: ((
Special_Function2 n)
. x1)
= ((
Special_Function2 n)
. x2);
reconsider x1 as
Element of
NAT by
A1;
reconsider x2 as
Element of
NAT by
A2;
((
Special_Function2 n)
. x2)
= (x2
+ n) by
Def3;
then (x1
+ n)
= (x2
+ n) by
A3,
Def3;
hence thesis;
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 ;
end
theorem ::
BOR_CANT:5
Th5: (for A,B be
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 be
SetSequence of Sigma, e be
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
A1: for A,B be
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)))
proof
let A,B be
SetSequence of Sigma;
assume that
A2: n
> n1 and
A3: B
= (A
* (
Special_Function (n1,n2)));
A4: for q be
Element of
NAT st q
<= n1 holds ((
Partial_Product (Prob
* B))
. q)
= ((
Partial_Product (Prob
* A))
. q)
proof
let q be
Element of
NAT ;
assume
A5: q
<= n1;
defpred
J[
Nat] means ((
Partial_Product (Prob
* B))
. ($1
* ((
Special_Function3 n1)
. $1)))
= ((
Partial_Product (Prob
* A))
. ($1
* ((
Special_Function3 n1)
. $1)));
A6:
J[
0 ]
proof
A7: ((
Partial_Product (Prob
* B))
.
0 )
= ((Prob
* B)
.
0 ) by
SERIES_3:def 1;
A8: ((
Partial_Product (Prob
* A))
.
0 )
= ((Prob
* A)
.
0 ) by
SERIES_3:def 1;
(
dom (Prob
* B))
=
NAT by
FUNCT_2:def 1;
then
A9: ((Prob
* B)
.
0 )
= (Prob
. (B
.
0 )) by
FUNCT_1: 12;
A10: (
dom (A
* (
Special_Function (n1,n2))))
=
NAT by
FUNCT_2:def 1;
((
Special_Function (n1,n2))
.
0 )
= (
IFGT (
0 ,n1,(
0
+ n2),
0 )) & (
IFGT (
0 ,n1,(
0
+ n2),
0 ))
=
0 by
Def2,
XXREAL_0:def 11;
then
A11: ((Prob
* B)
.
0 )
= (Prob
. (A
.
0 )) by
A10,
A3,
A9,
FUNCT_1: 12;
(
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
hence thesis by
A11,
A7,
A8,
FUNCT_1: 12;
end;
A12: for k be
Nat st
J[k] holds
J[(k
+ 1)]
proof
let k be
Nat;
assume
A13:
J[k];
per cases ;
suppose
A14: k
< n1;
then
A15: ((
Special_Function3 n1)
. k)
= (
IFGT (k,n1,
0 ,1)) & (
IFGT (k,n1,
0 ,1))
= 1 by
Def4,
XXREAL_0:def 11;
V: (k
+ 1)
<= n1 by
A14,
NAT_1: 13;
then
A16: ((
Special_Function3 n1)
. (k
+ 1))
= (
IFGT ((k
+ 1),n1,
0 ,1)) & (
IFGT ((k
+ 1),n1,
0 ,1))
= 1 by
Def4,
XXREAL_0:def 11;
A17: ((Prob
* B)
. (k
+ 1))
= ((Prob
* A)
. (k
+ 1))
proof
(
dom (Prob
* B))
=
NAT by
FUNCT_2:def 1;
then
A18: ((Prob
* B)
. (k
+ 1))
= (Prob
. (B
. (k
+ 1))) by
FUNCT_1: 12;
A19: (
dom (A
* (
Special_Function (n1,n2))))
=
NAT by
FUNCT_2:def 1;
((
Special_Function (n1,n2))
. (k
+ 1))
= (
IFGT ((k
+ 1),n1,((k
+ 1)
+ n2),(k
+ 1))) & (
IFGT ((k
+ 1),n1,((k
+ 1)
+ n2),(k
+ 1)))
= (k
+ 1) by
Def2,
XXREAL_0:def 11,
V;
then
A20: ((Prob
* B)
. (k
+ 1))
= (Prob
. (A
. (k
+ 1))) by
A19,
A3,
A18,
FUNCT_1: 12;
(
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
hence thesis by
A20,
FUNCT_1: 12;
end;
((
Partial_Product (Prob
* B))
. (k
+ 1))
= (((
Partial_Product (Prob
* A))
. k)
* ((Prob
* A)
. (k
+ 1))) by
A15,
A13,
A17,
SERIES_3:def 1;
hence thesis by
A16,
SERIES_3:def 1;
end;
suppose not k
< n1;
then n1
< (k
+ 1) by
XREAL_1: 145;
then
A22: ((
Special_Function3 n1)
. (k
+ 1))
= (
IFGT ((k
+ 1),n1,
0 ,1)) & (
IFGT ((k
+ 1),n1,
0 ,1))
=
0 by
Def4,
XXREAL_0:def 11;
A23: ((Prob
* B)
.
0 )
= ((Prob
* A)
.
0 )
proof
(
dom (Prob
* B))
=
NAT by
FUNCT_2:def 1;
then
A24: ((Prob
* B)
.
0 )
= (Prob
. (B
.
0 )) by
FUNCT_1: 12;
A25: (
dom (A
* (
Special_Function (n1,n2))))
=
NAT by
FUNCT_2:def 1;
((
Special_Function (n1,n2))
.
0 )
= (
IFGT (
0 ,n1,(
0
+ n2),
0 )) & (
IFGT (
0 ,n1,(
0
+ n2),
0 ))
=
0 by
Def2,
XXREAL_0:def 11;
then
A26: ((Prob
* B)
.
0 )
= (Prob
. (A
.
0 )) by
A25,
A3,
A24,
FUNCT_1: 12;
(
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
hence thesis by
A26,
FUNCT_1: 12;
end;
((
Partial_Product (Prob
* B))
. ((k
+ 1)
* ((
Special_Function3 n1)
. (k
+ 1))))
= ((Prob
* B)
.
0 ) & ((
Partial_Product (Prob
* A))
. ((k
+ 1)
* ((
Special_Function3 n1)
. (k
+ 1))))
= ((Prob
* A)
.
0 ) by
A22,
SERIES_3:def 1;
hence thesis by
A23;
end;
end;
A27: for k be
Nat holds
J[k] from
NAT_1:sch 2(
A6,
A12);
((
Partial_Product (Prob
* B))
. q)
= ((
Partial_Product (Prob
* A))
. q)
proof
((
Special_Function3 n1)
. q)
= (
IFGT (q,n1,
0 ,1)) & (
IFGT (q,n1,
0 ,1))
= 1 by
Def4,
A5,
XXREAL_0:def 11;
then (q
* ((
Special_Function3 n1)
. q))
= q;
hence thesis by
A27;
end;
hence thesis;
end;
defpred
J[
Nat] means ((
Partial_Product (Prob
* B))
. (($1
+ n1)
+ 1))
= (((
Partial_Product (Prob
* A))
. n1)
* ((
Partial_Product (Prob
* (A
^\ ((n1
+ n2)
+ 1))))
. (((($1
+ n1)
+ 1)
- n1)
- 1)));
A28: n1
in
NAT by
ORDINAL1:def 12;
((
Partial_Product (Prob
* B))
. ((
0
+ n1)
+ 1))
= (((
Partial_Product (Prob
* B))
. n1)
* ((Prob
* B)
. (n1
+ 1))) & n1
<= n1 by
SERIES_3:def 1;
then
A29: ((
Partial_Product (Prob
* B))
. ((
0
+ n1)
+ 1))
= (((
Partial_Product (Prob
* A))
. n1)
* ((Prob
* B)
. (n1
+ 1))) by
A4,
A28;
A30: (
dom (A
* (
Special_Function (n1,n2))))
=
NAT by
FUNCT_2:def 1;
n1
< (n1
+ 1) by
NAT_1: 13;
then ((
Special_Function (n1,n2))
. (n1
+ 1))
= (
IFGT ((n1
+ 1),n1,((n1
+ 1)
+ n2),(n1
+ 1))) & (
IFGT ((n1
+ 1),n1,((n1
+ 1)
+ n2),(n1
+ 1)))
= ((n1
+ 1)
+ n2) by
Def2,
XXREAL_0:def 11;
then
A32: (Prob
. (B
. (n1
+ 1)))
= (Prob
. (A
. ((n1
+ 1)
+ n2))) by
A30,
A3,
FUNCT_1: 12;
A33: (A
. (((n1
+ n2)
+ 1)
+
0 ))
= ((A
^\ ((n1
+ n2)
+ 1))
.
0 ) by
NAT_1:def 3;
(
dom (Prob
* (A
^\ ((n1
+ n2)
+ 1))))
=
NAT by
FUNCT_2:def 1;
then
A34: (Prob
. (B
. (n1
+ 1)))
= ((Prob
* (A
^\ ((n1
+ n2)
+ 1)))
.
0 ) by
A33,
A32,
FUNCT_1: 12;
(
dom (Prob
* B))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* B)
. (n1
+ 1))
= ((Prob
* (A
^\ ((n1
+ n2)
+ 1)))
.
0 ) by
A34,
FUNCT_1: 12;
then
A35:
J[
0 ] by
A29,
SERIES_3:def 1;
A36: for k be
Nat st
J[k] holds
J[(k
+ 1)]
proof
let k be
Nat;
assume
A37:
J[k];
A38: ((
Partial_Product (Prob
* B))
. (((k
+ 1)
+ n1)
+ 1))
= ((((
Partial_Product (Prob
* A))
. n1)
* ((
Partial_Product (Prob
* (A
^\ ((n1
+ n2)
+ 1))))
. k))
* ((Prob
* B)
. (((k
+ 1)
+ n1)
+ 1))) by
A37,
SERIES_3:def 1;
A39: ((Prob
* B)
. (((k
+ 1)
+ n1)
+ 1))
= ((Prob
* (A
^\ ((n1
+ n2)
+ 1)))
. (k
+ 1))
proof
set j = (((k
+ 1)
+ n1)
+ 1);
A40: (
dom (A
* (
Special_Function (n1,n2))))
=
NAT by
FUNCT_2:def 1;
n1
< (n1
+ ((k
+ 1)
+ 1)) by
NAT_1: 19,
XREAL_1: 31;
then ((
Special_Function (n1,n2))
. j)
= (
IFGT (j,n1,(j
+ n2),j)) & (
IFGT (j,n1,(j
+ n2),j))
= (j
+ n2) by
Def2,
XXREAL_0:def 11;
then (B
. (((k
+ 1)
+ n1)
+ 1))
= (A
. (((n1
+ n2)
+ 1)
+ (k
+ 1))) by
A40,
A3,
FUNCT_1: 12;
then
A41: (Prob
. (B
. (((k
+ 1)
+ n1)
+ 1)))
= (Prob
. ((A
^\ ((n1
+ n2)
+ 1))
. (k
+ 1))) by
NAT_1:def 3;
(
dom (Prob
* B))
=
NAT by
FUNCT_2:def 1;
then
A42: ((Prob
* B)
. (((k
+ 1)
+ n1)
+ 1))
= (Prob
. ((A
^\ ((n1
+ n2)
+ 1))
. (k
+ 1))) by
A41,
FUNCT_1: 12;
(
dom (Prob
* (A
^\ ((n1
+ n2)
+ 1))))
=
NAT by
FUNCT_2:def 1;
hence thesis by
A42,
FUNCT_1: 12;
end;
(((
Partial_Product (Prob
* (A
^\ ((n1
+ n2)
+ 1))))
. k)
* ((Prob
* (A
^\ ((n1
+ n2)
+ 1)))
. (k
+ 1)))
= ((
Partial_Product (Prob
* (A
^\ ((n1
+ n2)
+ 1))))
. (k
+ 1)) by
SERIES_3:def 1;
hence thesis by
A39,
A38;
end;
A43: for k be
Nat holds
J[k] from
NAT_1:sch 2(
A35,
A36);
((n
- n1)
- 1) is
Element of
NAT
proof
(n1
+ 1)
<= n by
A2,
NAT_1: 13;
then ((n1
+ 1)
- 1)
<= (n
- 1) by
XREAL_1: 9;
then n1
<= (n
- 1) & (n
- 1) is
Element of
NAT by
A2,
NAT_1: 20;
then ((n
- 1)
- n1) is
Element of
NAT by
NAT_1: 21;
hence thesis;
end;
then
consider k be
Element of
NAT such that
A44: k
= ((n
- n1)
- 1);
((
Partial_Product (Prob
* B))
. n)
= (((
Partial_Product (Prob
* A))
. n1)
* ((
Partial_Product (Prob
* (A
^\ ((n1
+ n2)
+ 1))))
. ((((((n
- n1)
- 1)
+ n1)
+ 1)
- n1)
- 1))) by
A43,
A44;
hence thesis;
end;
for A,B,C be
SetSequence of Sigma, n1,n2,n be
Nat, e be
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
let A,B,C be
SetSequence of Sigma;
let n1,n2,n be
Nat;
let e be
sequence of
NAT ;
assume
A45: n
> n1;
assume C
= (A
* e);
assume
A46: B
= (C
* (
Special_Function (n1,n2)));
reconsider B as
SetSequence of Sigma;
A47: ((
Partial_Intersection B)
. n1)
= ((
Partial_Intersection C)
. n1)
proof
for x be
object holds x
in ((
Partial_Intersection B)
. n1) iff x
in ((
Partial_Intersection C)
. n1)
proof
let x be
object;
hereby
assume
A48: x
in ((
Partial_Intersection B)
. n1);
x
in ((
Partial_Intersection C)
. n1)
proof
for knat be
Nat st knat
<= n1 holds x
in (C
. knat)
proof
let knat be
Nat;
assume
A50: knat
<= n1;
reconsider knat as
Element of
NAT by
ORDINAL1:def 12;
A51: x
in (B
. knat) by
A50,
A48,
PROB_3: 25;
A52: (
dom (C
* (
Special_Function (n1,n2))))
=
NAT by
FUNCT_2:def 1;
((
Special_Function (n1,n2))
. knat)
= (
IFGT (knat,n1,(knat
+ n2),knat)) & (
IFGT (knat,n1,(knat
+ n2),knat))
= knat by
Def2,
A50,
XXREAL_0:def 11;
hence thesis by
A52,
A46,
A51,
FUNCT_1: 12;
end;
hence thesis by
PROB_3: 25;
end;
hence x
in ((
Partial_Intersection C)
. n1);
end;
assume
A53: x
in ((
Partial_Intersection C)
. n1);
x
in ((
Partial_Intersection B)
. n1)
proof
for knat be
Nat st knat
<= n1 holds x
in (B
. knat)
proof
let knat be
Nat;
assume
A54: knat
<= n1;
reconsider knat as
Element of
NAT by
ORDINAL1:def 12;
A55: x
in (C
. knat) by
A53,
A54,
PROB_3: 25;
A56: (
dom (C
* (
Special_Function (n1,n2))))
=
NAT by
FUNCT_2:def 1;
((
Special_Function (n1,n2))
. knat)
= (
IFGT (knat,n1,(knat
+ n2),knat)) & (
IFGT (knat,n1,(knat
+ n2),knat))
= knat by
Def2,
A54,
XXREAL_0:def 11;
hence thesis by
A56,
A46,
A55,
FUNCT_1: 12;
end;
hence thesis by
PROB_3: 25;
end;
hence x
in ((
Partial_Intersection B)
. n1);
end;
hence thesis by
TARSKI: 2;
end;
A57: for x be
set holds ((for knat be
Nat st knat
<= n holds x
in (B
. knat)) implies (for knat be
Nat st knat
<= n1 holds x
in (B
. knat)) & (for knat be
Nat st n1
< knat & knat
<= n holds x
in (B
. knat))) by
A45,
XXREAL_0: 2;
A58: for x be
object holds x
in ((
Partial_Intersection (C
^\ ((n1
+ n2)
+ 1)))
. ((n
- n1)
- 1)) implies (for qnat be
Nat st n1
< qnat & qnat
<= n holds x
in (B
. qnat))
proof
let x be
object;
assume
A59: x
in ((
Partial_Intersection (C
^\ ((n1
+ n2)
+ 1)))
. ((n
- n1)
- 1));
A60: ((n
- n1)
- 1)
>=
0 & ((n
- n1)
- 1) is
Element of
NAT
proof
(n
- n1) is
Element of
NAT by
A45,
NAT_1: 21;
hence thesis by
A45,
NAT_1: 20,
XREAL_1: 50;
end;
A61: for knat be
Nat st knat
<= ((n
- n1)
- 1) holds x
in (C
. (knat
+ ((n1
+ n2)
+ 1)))
proof
let knat be
Nat;
assume knat
<= ((n
- n1)
- 1);
then x
in ((C
^\ ((n1
+ n2)
+ 1))
. knat) by
A60,
A59,
PROB_3: 25;
hence thesis by
NAT_1:def 3;
end;
for qnat be
Nat st n1
< qnat & qnat
<= n holds x
in (B
. qnat)
proof
let qnat be
Nat;
assume that
A62: n1
< qnat and
A63: qnat
<= n;
(n1
+ 1)
<= qnat & qnat
<= n by
A62,
A63,
NAT_1: 13;
then (qnat
- (n1
+ 1)) is
Element of
NAT by
NAT_1: 21;
then
consider knat be
Nat such that
A66: knat
= ((qnat
- n1)
- 1);
A67: ((qnat
- n1)
- 1)
<= ((n
- n1)
- 1)
proof
(qnat
- (n1
+ 1))
<= (n
- (n1
+ 1)) by
A63,
XREAL_1: 9;
hence thesis;
end;
A68: x
in (C
. (knat
+ ((n1
+ n2)
+ 1))) by
A66,
A67,
A61;
x
in (B
. qnat)
proof
reconsider qnat as
Element of
NAT by
ORDINAL1:def 12;
A69: (
dom (C
* (
Special_Function (n1,n2))))
=
NAT by
FUNCT_2:def 1;
((
Special_Function (n1,n2))
. qnat)
= (
IFGT (qnat,n1,(qnat
+ n2),qnat)) & (
IFGT (qnat,n1,(qnat
+ n2),qnat))
= (qnat
+ n2) by
Def2,
A62,
XXREAL_0:def 11;
hence thesis by
A69,
A46,
A66,
A68,
FUNCT_1: 12;
end;
hence thesis;
end;
hence thesis;
end;
A70: for x be
object holds (for qnat be
Nat st n1
< qnat & qnat
<= n holds x
in (B
. qnat)) implies x
in ((
Partial_Intersection (C
^\ ((n1
+ n2)
+ 1)))
. ((n
- n1)
- 1))
proof
let x be
object;
assume
A71: for qnat be
Nat st n1
< qnat & qnat
<= n holds x
in (B
. qnat);
A72: ((n
- n1)
- 1)
>=
0 & ((n
- n1)
- 1) is
Element of
NAT
proof
(n
- n1) is
Element of
NAT by
A45,
NAT_1: 21;
hence thesis by
A45,
NAT_1: 20,
XREAL_1: 50;
end;
x
in ((
Partial_Intersection (C
^\ ((n1
+ n2)
+ 1)))
. ((n
- n1)
- 1))
proof
A73: for qnat be
Nat st
0
<= ((qnat
- n1)
- 1) & ((qnat
- n1)
- 1)
<= ((n
- n1)
- 1) holds x
in (B
. qnat)
proof
let qnat be
Nat;
assume that
A74:
0
<= ((qnat
- n1)
- 1) and
A75: ((qnat
- n1)
- 1)
<= ((n
- n1)
- 1);
(
0
+ (n1
+ 1))
<= ((qnat
- (n1
+ 1))
+ (n1
+ 1)) by
A74,
XREAL_1: 6;
then ((n1
+ 1)
- 1)
<= (qnat
- 1) by
XREAL_1: 9;
then n1
<= (qnat
- 1) & qnat
< (qnat
+ 1) by
NAT_1: 13;
then n1
<= (qnat
- 1) & (qnat
- 1)
< ((qnat
+ 1)
- 1) by
XREAL_1: 9;
then
A76: n1
< qnat by
XXREAL_0: 2;
((qnat
- (n1
+ 1))
+ (n1
+ 1))
<= ((n
- (n1
+ 1))
+ (n1
+ 1)) by
A75,
XREAL_1: 6;
hence thesis by
A76,
A71;
end;
for knat be
Nat st
0
<= knat & knat
<= ((n
- n1)
- 1) holds x
in ((C
^\ ((n1
+ n2)
+ 1))
. knat)
proof
let knat be
Nat;
assume that
0
<= knat and
A77: knat
<= ((n
- n1)
- 1);
set qnat = ((knat
+ n1)
+ 1);
((qnat
- n1)
- 1)
<= ((n
- n1)
- 1) by
A77;
then
A79: x
in (B
. qnat) by
A73;
A80: (
dom (C
* (
Special_Function (n1,n2))))
=
NAT by
FUNCT_2:def 1;
n1
< qnat by
NAT_1: 13,
XREAL_1: 31;
then ((
Special_Function (n1,n2))
. qnat)
= (
IFGT (qnat,n1,(qnat
+ n2),qnat)) & (
IFGT (qnat,n1,(qnat
+ n2),qnat))
= (qnat
+ n2) by
Def2,
XXREAL_0:def 11;
then (B
. qnat)
= (C
. (((n1
+ n2)
+ 1)
+ knat)) by
A46,
A80,
FUNCT_1: 12;
hence thesis by
A79,
NAT_1:def 3;
end;
then for knat be
Nat st knat
<= ((n
- n1)
- 1) holds x
in ((C
^\ ((n1
+ n2)
+ 1))
. knat);
hence thesis by
A72,
PROB_3: 25;
end;
hence thesis;
end;
A82: for x be
set holds (x
in ((
Partial_Intersection B)
. n) iff (for knat be
Nat st knat
<= n1 holds x
in (B
. knat)) & (for knat be
Nat st n1
< knat & knat
<= n holds x
in (B
. knat)))
proof
let x be
set;
x
in ((
Partial_Intersection B)
. n) iff for knat be
Nat st knat
<= n holds x
in (B
. knat) by
PROB_3: 25;
hence thesis by
A57;
end;
A83: for x be
set holds ((x
in ((
Partial_Intersection B)
. n)) iff (x
in ((
Partial_Intersection B)
. n1) & (for knat be
Nat st n1
< knat & knat
<= n holds x
in (B
. knat))))
proof
let x be
set;
x
in ((
Partial_Intersection B)
. n1) iff for knat be
Nat st knat
<= n1 holds x
in (B
. knat) by
PROB_3: 25;
hence thesis by
A82;
end;
for x be
object holds ((x
in ((
Partial_Intersection B)
. n)) iff (x
in ((
Partial_Intersection B)
. n1) & x
in ((
Partial_Intersection (C
^\ ((n1
+ n2)
+ 1)))
. ((n
- n1)
- 1))))
proof
let x be
object;
x
in ((
Partial_Intersection (C
^\ ((n1
+ n2)
+ 1)))
. ((n
- n1)
- 1)) iff for knat be
Nat st n1
< knat & knat
<= n holds x
in (B
. knat) by
A58,
A70;
hence thesis by
A83;
end;
hence thesis by
A47,
XBOOLE_0:def 4;
end;
hence thesis by
A1;
end;
definition
let Omega be non
empty
set, Sigma be
SigmaField of Omega, Prob be
Probability of Sigma, A be
SetSequence of Sigma;
::
BOR_CANT:def6
pred A
is_all_independent_wrt Prob means
:
Def6: for B be
SetSequence of Sigma st (ex e be
sequence of
NAT st (e is
one-to-one & (for n be
Nat holds (A
. (e
. n))
= (B
. n)))) holds (for n be
Nat holds ((
Partial_Product (Prob
* B))
. n)
= (Prob
. ((
Partial_Intersection B)
. n)));
end
theorem ::
BOR_CANT:6
Th6: 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)))
proof
assume that
A1: n
> n1 and
A2: A
is_all_independent_wrt Prob;
A3: for A,B be
SetSequence of Sigma, k,n be
Element of
NAT st B
= (A
* (
Special_Function2 k)) holds ((
Partial_Product (Prob
* (A
^\ k)))
. n)
= ((
Partial_Product (Prob
* B))
. n)
proof
let A,B be
SetSequence of Sigma;
let k,n be
Element of
NAT ;
assume
A4: B
= (A
* (
Special_Function2 k));
defpred
J[
Nat] means ((
Partial_Product (Prob
* (A
^\ k)))
. $1)
= ((
Partial_Product (Prob
* B))
. $1);
(
dom (Prob
* (A
^\ k)))
=
NAT by
FUNCT_2:def 1;
then
A5: ((Prob
* (A
^\ k))
.
0 )
= (Prob
. ((A
^\ k)
.
0 )) by
FUNCT_1: 12;
((Prob
* (A
^\ k))
.
0 )
= (Prob
. (A
. (
0
+ k))) by
A5,
NAT_1:def 3;
then
A6: ((
Partial_Product (Prob
* (A
^\ k)))
.
0 )
= (Prob
. (A
. k)) by
SERIES_3:def 1;
A7: ((
Partial_Product (Prob
* B))
.
0 )
= ((Prob
* B)
.
0 ) by
SERIES_3:def 1;
A8: ((
Special_Function2 k)
.
0 )
= (
0
+ k) by
Def3;
(
dom (A
* (
Special_Function2 k)))
=
NAT by
FUNCT_2:def 1;
then
A9: (Prob
. (B
.
0 ))
= (Prob
. (A
. k)) by
A8,
A4,
FUNCT_1: 12;
(
dom (Prob
* B))
=
NAT by
FUNCT_2:def 1;
then
A10:
J[
0 ] by
A9,
A7,
A6,
FUNCT_1: 12;
A11: for q be
Nat st
J[q] holds
J[(q
+ 1)]
proof
let q be
Nat;
assume
J[q];
then
A13: ((
Partial_Product (Prob
* (A
^\ k)))
. (q
+ 1))
= (((
Partial_Product (Prob
* B))
. q)
* ((Prob
* (A
^\ k))
. (q
+ 1))) by
SERIES_3:def 1;
((Prob
* (A
^\ k))
. (q
+ 1))
= ((Prob
* B)
. (q
+ 1))
proof
(
dom (Prob
* (A
^\ k)))
=
NAT by
FUNCT_2:def 1;
then
A14: ((Prob
* (A
^\ k))
. (q
+ 1))
= (Prob
. ((A
^\ k)
. (q
+ 1))) by
FUNCT_1: 12;
(
dom (Prob
* B))
=
NAT by
FUNCT_2:def 1;
then
A15: ((Prob
* B)
. (q
+ 1))
= (Prob
. (B
. (q
+ 1))) by
FUNCT_1: 12;
(
dom (A
* (
Special_Function2 k)))
=
NAT by
FUNCT_2:def 1;
then
A16: (B
. (q
+ 1))
= (A
. ((
Special_Function2 k)
. (q
+ 1))) by
A4,
FUNCT_1: 12;
((
Special_Function2 k)
. (q
+ 1))
= ((q
+ 1)
+ k) & ((q
+ 1)
+ k)
= ((q
+ 1)
+ k) by
Def3;
hence thesis by
A16,
A15,
A14,
NAT_1:def 3;
end;
hence thesis by
A13,
SERIES_3:def 1;
end;
for k be
Nat holds
J[k] from
NAT_1:sch 2(
A10,
A11);
hence thesis;
end;
A17: for m,m1,m2 be
Element of
NAT , e be
sequence of
NAT , C,B be
SetSequence of Sigma st m1
< m & e is
one-to-one & C
= (A
* e) & B
= (C
* (
Special_Function (m1,m2))) holds (Prob
. ((
Partial_Intersection B)
. m))
= (((
Partial_Product (Prob
* C))
. m1)
* ((
Partial_Product (Prob
* (C
^\ ((m1
+ m2)
+ 1))))
. ((m
- m1)
- 1)))
proof
let m,m1,m2 be
Element of
NAT ;
let e be
sequence of
NAT ;
let C,B be
SetSequence of Sigma;
assume that
A18: m1
< m and
A19: e is
one-to-one and
A20: C
= (A
* e) and
A21: B
= (C
* (
Special_Function (m1,m2)));
B is
SetSequence of Sigma & (e
* (
Special_Function (m1,m2))) is
sequence of
NAT & (e
* (
Special_Function (m1,m2))) is
one-to-one & (for n be
Nat holds (A
. ((e
* (
Special_Function (m1,m2)))
. n))
= (B
. n))
proof
for n be
Nat holds (A
. ((e
* (
Special_Function (m1,m2)))
. n))
= (B
. n)
proof
let n be
Nat;
A22: (
dom ((A
* e)
* (
Special_Function (m1,m2))))
=
NAT by
FUNCT_2:def 1;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
A23: (B
. n)
= ((A
* e)
. ((
Special_Function (m1,m2))
. n)) by
A21,
A20,
A22,
FUNCT_1: 12;
(
dom (A
* e))
=
NAT by
FUNCT_2:def 1;
then
A24: (B
. n)
= (A
. (e
. ((
Special_Function (m1,m2))
. n))) by
A23,
FUNCT_1: 12;
(
dom (e
* (
Special_Function (m1,m2))))
=
NAT by
FUNCT_2:def 1;
hence thesis by
A24,
FUNCT_1: 12;
end;
hence thesis by
A19,
FUNCT_1: 24;
end;
then (Prob
. ((
Partial_Intersection B)
. m))
= ((
Partial_Product (Prob
* B))
. m) by
A2;
hence thesis by
A18,
A21,
Th5;
end;
A25: for m,m1 be
Element of
NAT , e be
sequence of
NAT , C,B be
SetSequence of Sigma st C
= (A
* e) & e is
one-to-one & B
= (C
* (
Special_Function2 m1)) holds (Prob
. ((
Partial_Intersection B)
. m))
= ((
Partial_Product (Prob
* (C
^\ m1)))
. m)
proof
let m,m1 be
Element of
NAT ;
let e be
sequence of
NAT ;
let C,B be
SetSequence of Sigma;
assume that
A26: C
= (A
* e) and
A27: e is
one-to-one and
A28: B
= (C
* (
Special_Function2 m1));
A29: B is
SetSequence of Sigma & (
Special_Function2 m1) is
sequence of
NAT & (
dom (e
* (
Special_Function2 m1)))
<>
{} & (e
* (
Special_Function2 m1)) is
one-to-one & (for n be
Nat holds (A
. ((e
* (
Special_Function2 m1))
. n))
= (B
. n))
proof
for n be
Nat holds (A
. ((e
* (
Special_Function2 m1))
. n))
= (B
. n)
proof
let n be
Nat;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
(
dom (A
* (e
* (
Special_Function2 m1))))
=
NAT by
FUNCT_2:def 1;
then
A31: ((A
* (e
* (
Special_Function2 m1)))
. n)
= (A
. ((e
* (
Special_Function2 m1))
. n)) by
FUNCT_1: 12;
(
dom (A
* e))
=
NAT by
FUNCT_2:def 1;
then
A32: ((A
* e)
. ((
Special_Function2 m1)
. n))
= (A
. (e
. ((
Special_Function2 m1)
. n))) by
FUNCT_1: 12;
(
dom (e
* (
Special_Function2 m1)))
=
NAT by
FUNCT_2:def 1;
then
A33: ((A
* e)
. ((
Special_Function2 m1)
. n))
= ((A
* (e
* (
Special_Function2 m1)))
. n) by
A32,
A31,
FUNCT_1: 12;
(
dom ((A
* e)
* (
Special_Function2 m1)))
=
NAT by
FUNCT_2:def 1;
then
A34: (B
. n)
= ((A
* (e
* (
Special_Function2 m1)))
. n) by
A33,
A28,
A26,
FUNCT_1: 12;
(
dom (A
* (e
* (
Special_Function2 m1))))
=
NAT by
FUNCT_2:def 1;
hence thesis by
A34,
FUNCT_1: 12;
end;
hence thesis by
A27,
FUNCT_1: 24;
end;
(Prob
. ((
Partial_Intersection B)
. m))
= ((
Partial_Product (Prob
* B))
. m) by
A2,
A29;
hence thesis by
A28,
A3;
end;
A35: for q be
Nat holds (Prob
. (((
Partial_Intersection (
Complement A))
. n1)
/\ ((
Partial_Intersection (A
^\ ((n1
+ n2)
+ 1)))
. q)))
= (((
Partial_Product (Prob
* (
Complement A)))
. n1)
* ((
Partial_Product (Prob
* (A
^\ ((n1
+ n2)
+ 1))))
. q))
proof
let q be
Nat;
defpred
J[
Nat] means for e be
sequence of
NAT , q,n2 be
Nat, C be
SetSequence of Sigma st e is
one-to-one & C
= (A
* e) holds (Prob
. (((
Partial_Intersection (
Complement C))
. $1)
/\ ((
Partial_Intersection (C
^\ (($1
+ n2)
+ 1)))
. q)))
= (((
Partial_Product (Prob
* (
Complement C)))
. $1)
* ((
Partial_Product (Prob
* (C
^\ (($1
+ n2)
+ 1))))
. q));
A36:
J[
0 ]
proof
let e be
sequence of
NAT ;
let q,n2 be
Nat;
let C be
SetSequence of Sigma;
assume
A37: e is
one-to-one;
assume
A38: C
= (A
* e);
(Prob
. (((
Partial_Intersection (
Complement C))
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q)))
= (Prob
. (((
Complement C)
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q))) by
PROB_3: 21;
then (Prob
. (((
Partial_Intersection (
Complement C))
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q)))
= (Prob
. (((C
.
0 )
` )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q))) by
PROB_1:def 2;
then (Prob
. (((
Partial_Intersection (
Complement C))
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q)))
= (Prob
. ((Omega
\ (C
.
0 ))
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q))) by
SUBSET_1:def 4;
then
A39: (Prob
. (((
Partial_Intersection (
Complement C))
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q)))
= (Prob
. ((Omega
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q))
\ ((C
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q)))) by
XBOOLE_1: 111;
A40: (Prob
. (((
Partial_Intersection (
Complement C))
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q)))
= (Prob
. (((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q)
\ ((C
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q)))) by
A39,
XBOOLE_1: 28;
A41: (Prob
. (((
Partial_Intersection (
Complement C))
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q)))
= ((Prob
. ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q))
- (Prob
. ((C
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q)))) by
A40,
PROB_1: 33,
XBOOLE_1: 17;
consider m1 be
Element of
NAT such that
A42: m1
=
0 ;
reconsider m = ((m1
+ 1)
+ q) as
Element of
NAT by
ORDINAL1:def 12;
reconsider m2 = n2 as
Element of
NAT by
ORDINAL1:def 12;
consider B be
SetSequence of Omega such that
A43: B
= (C
* (
Special_Function (m1,m2)));
reconsider B as
SetSequence of Sigma by
A43;
A44: m1
< m & C
= (A
* e) & B
= (C
* (
Special_Function (m1,m2)))
proof
m1
< (m1
+ 1) & (m1
+ 1)
<= ((m1
+ 1)
+ q) by
NAT_1: 13,
XREAL_1: 31;
hence thesis by
A38,
A43,
XXREAL_0: 2;
end;
then (Prob
. ((
Partial_Intersection B)
. m))
= (Prob
. (((
Partial_Intersection C)
. m1)
/\ ((
Partial_Intersection (C
^\ ((m1
+ m2)
+ 1)))
. ((m
- m1)
- 1)))) by
Th5;
then (((
Partial_Product (Prob
* C))
.
0 )
* ((
Partial_Product (Prob
* (C
^\ ((
0
+ n2)
+ 1))))
. q))
= (Prob
. (((
Partial_Intersection C)
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q))) by
A44,
A37,
A17,
A42;
then ((Prob
. ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q))
- (((
Partial_Product (Prob
* C))
.
0 )
* ((
Partial_Product (Prob
* (C
^\ ((
0
+ n2)
+ 1))))
. q)))
= ((Prob
. ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q))
- (Prob
. ((C
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q)))) by
PROB_3: 21;
then
A45: (Prob
. (((
Partial_Intersection (
Complement C))
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q)))
= ((Prob
. ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q))
- (((Prob
* C)
.
0 )
* ((
Partial_Product (Prob
* (C
^\ ((
0
+ n2)
+ 1))))
. q))) by
A41,
SERIES_3:def 1;
((Prob
* C)
.
0 )
= (1
- ((Prob
* (
Complement C))
.
0 ))
proof
(C
.
0 )
= (((C
.
0 )
` )
` ) & (((C
.
0 )
` )
` )
= (Omega
\ ((C
.
0 )
` )) by
SUBSET_1:def 4;
then (Prob
. (C
.
0 ))
= (Prob
. ((
[#] Sigma)
\ ((C
.
0 )
` ))) & ((C
.
0 )
` ) is
Event of Sigma by
PROB_1: 20;
then
A46: (Prob
. (C
.
0 ))
= (1
- (Prob
. ((C
.
0 )
` ))) by
PROB_1: 32;
(
dom (Prob
* C))
=
NAT by
FUNCT_2:def 1;
then
A47: ((Prob
* C)
.
0 )
= (1
- (Prob
. ((C
.
0 )
` ))) by
A46,
FUNCT_1: 12;
(
dom (Prob
* (
Complement C)))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* (
Complement C))
.
0 )
= (Prob
. ((
Complement C)
.
0 )) by
FUNCT_1: 12;
hence thesis by
A47,
PROB_1:def 2;
end;
then
A48: (Prob
. (((
Partial_Intersection (
Complement C))
.
0 )
/\ ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q)))
= ((Prob
. ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q))
- (((
Partial_Product (Prob
* (C
^\ ((
0
+ n2)
+ 1))))
. q)
- (((Prob
* (
Complement C))
.
0 )
* ((
Partial_Product (Prob
* (C
^\ ((
0
+ n2)
+ 1))))
. q)))) by
A45;
set m1 = ((
0
+ n2)
+ 1);
set m = q;
set B = (C
* (
Special_Function2 m1));
reconsider B as
SetSequence of Sigma;
A49: for A,B,C be
SetSequence of Sigma, k,n be
Element of
NAT , e be
sequence of
NAT st B
= (C
* (
Special_Function2 k)) holds ((
Partial_Intersection (C
^\ k))
. n)
= ((
Partial_Intersection B)
. n)
proof
let A,B,C be
SetSequence of Sigma;
let k,n be
Element of
NAT ;
let e be
sequence of
NAT ;
assume
A50: B
= (C
* (
Special_Function2 k));
A51: for x be
set holds (for knat be
Nat st knat
<= n holds x
in ((C
^\ k)
. knat)) iff (for knat be
Nat st knat
<= n holds x
in (B
. knat))
proof
let x be
set;
hereby
assume
A52: for knat be
Nat st knat
<= n holds x
in ((C
^\ k)
. knat);
thus for knat be
Nat st knat
<= n holds x
in (B
. knat)
proof
let knat be
Nat;
assume
A53: knat
<= n;
reconsider knat as
Element of
NAT by
ORDINAL1:def 12;
(
dom (C
* (
Special_Function2 k)))
=
NAT by
FUNCT_2:def 1;
then
A54: ((C
* (
Special_Function2 k))
. knat)
= (C
. ((
Special_Function2 k)
. knat)) by
FUNCT_1: 12;
((
Special_Function2 k)
. knat)
= (knat
+ k) & (knat
+ k)
= (knat
+ k) by
Def3;
then x
in (B
. knat) iff x
in ((C
^\ k)
. knat) by
A50,
A54,
NAT_1:def 3;
hence thesis by
A53,
A52;
end;
end;
assume
A55: for knat be
Nat st knat
<= n holds x
in (B
. knat);
thus for knat be
Nat st knat
<= n holds x
in ((C
^\ k)
. knat)
proof
let knat be
Nat;
assume
A56: knat
<= n;
reconsider knat as
Element of
NAT by
ORDINAL1:def 12;
(
dom (C
* (
Special_Function2 k)))
=
NAT by
FUNCT_2:def 1;
then
A57: ((C
* (
Special_Function2 k))
. knat)
= (C
. ((
Special_Function2 k)
. knat)) by
FUNCT_1: 12;
((
Special_Function2 k)
. knat)
= (knat
+ k) & (knat
+ k)
= (knat
+ k) by
Def3;
then x
in (B
. knat) iff x
in ((C
^\ k)
. knat) by
A50,
A57,
NAT_1:def 3;
hence thesis by
A55,
A56;
end;
end;
for x be
object holds (x
in ((
Partial_Intersection (C
^\ k))
. n) iff (x
in ((
Partial_Intersection B)
. n)))
proof
let x be
object;
(x
in ((
Partial_Intersection (C
^\ k))
. n) iff for knat be
Nat st knat
<= n holds x
in ((C
^\ k)
. knat)) & (x
in ((
Partial_Intersection B)
. n) iff for knat be
Nat st knat
<= n holds x
in (B
. knat)) by
PROB_3: 25;
hence thesis by
A51;
end;
hence thesis by
TARSKI: 2;
end;
m
in
NAT by
ORDINAL1:def 12;
then
A58: (Prob
. ((
Partial_Intersection B)
. m))
= ((
Partial_Product (Prob
* (C
^\ m1)))
. m) by
A38,
A37,
A25;
q
in
NAT by
ORDINAL1:def 12;
then (Prob
. ((
Partial_Intersection (C
^\ ((
0
+ n2)
+ 1)))
. q))
= ((
Partial_Product (Prob
* (C
^\ ((
0
+ n2)
+ 1))))
. q) by
A49,
A58;
hence thesis by
A48,
SERIES_3:def 1;
end;
A59: for k be
Nat st
J[k] holds
J[(k
+ 1)]
proof
let k be
Nat;
assume
A60:
J[k];
let e be
sequence of
NAT ;
let q,n2 be
Nat;
let C be
SetSequence of Sigma;
assume
A61: e is
one-to-one;
assume
A62: C
= (A
* e);
(Prob
. (((
Partial_Intersection (
Complement C))
. (k
+ 1))
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q)))
= (Prob
. ((((
Partial_Intersection (
Complement C))
. k)
/\ ((
Complement C)
. (k
+ 1)))
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q))) by
PROB_3: 21;
then (Prob
. (((
Partial_Intersection (
Complement C))
. (k
+ 1))
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q)))
= (Prob
. ((((C
. (k
+ 1))
` )
/\ ((
Partial_Intersection (
Complement C))
. k))
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q))) by
PROB_1:def 2;
then (Prob
. (((
Partial_Intersection (
Complement C))
. (k
+ 1))
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q)))
= (Prob
. (((C
. (k
+ 1))
` )
/\ (((
Partial_Intersection (
Complement C))
. k)
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q)))) by
XBOOLE_1: 16;
then (Prob
. (((
Partial_Intersection (
Complement C))
. (k
+ 1))
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q)))
= (Prob
. ((Omega
\ (C
. (k
+ 1)))
/\ (((
Partial_Intersection (
Complement C))
. k)
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q)))) by
SUBSET_1:def 4;
then
A63: (Prob
. (((
Partial_Intersection (
Complement C))
. (k
+ 1))
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q)))
= (Prob
. ((Omega
/\ (((
Partial_Intersection (
Complement C))
. k)
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q)))
\ ((C
. (k
+ 1))
/\ (((
Partial_Intersection (
Complement C))
. k)
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q))))) by
XBOOLE_1: 50;
A64: (Prob
. (((
Partial_Intersection (
Complement C))
. (k
+ 1))
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q)))
= (Prob
. ((((
Partial_Intersection (
Complement C))
. k)
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q))
\ ((C
. (k
+ 1))
/\ (((
Partial_Intersection (
Complement C))
. k)
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q))))) by
A63,
XBOOLE_1: 28;
A65: (Prob
. (((
Partial_Intersection (
Complement C))
. k)
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q)))
= (((
Partial_Product (Prob
* (
Complement C)))
. k)
* ((
Partial_Product (Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1))))
. q))
proof
(Prob
. (((
Partial_Intersection (
Complement C))
. k)
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q)))
= (((
Partial_Product (Prob
* (
Complement C)))
. k)
* ((
Partial_Product (Prob
* (C
^\ ((k
+ (1
+ n2))
+ 1))))
. q)) by
A61,
A62,
A60;
hence thesis;
end;
A66: (Prob
. (((
Partial_Intersection (
Complement C))
. (k
+ 1))
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q)))
= ((((
Partial_Product (Prob
* (
Complement C)))
. k)
* ((
Partial_Product (Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1))))
. q))
- ((((Prob
* C)
. (k
+ 1))
* ((
Partial_Product (Prob
* (
Complement C)))
. k))
* ((
Partial_Product (Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1))))
. q)))
proof
((((Prob
* C)
. (k
+ 1))
* ((
Partial_Product (Prob
* (
Complement C)))
. k))
* ((
Partial_Product (Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1))))
. q))
= (Prob
. ((C
. (k
+ 1))
/\ (((
Partial_Intersection (
Complement C))
. k)
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q))))
proof
consider F be
SetSequence of Omega such that
A67: F
= (C
* (
Special_Function4 (k,n2)));
F is
SetSequence of Sigma
proof
for n be
Nat holds (F
. n) is
Event of Sigma
proof
let n be
Nat;
(
dom (C
* (
Special_Function4 (k,n2))))
=
NAT by
FUNCT_2:def 1;
then (F
. n)
= (C
. ((
Special_Function4 (k,n2))
. n)) by
A67,
FUNCT_1: 12,
ORDINAL1:def 12;
hence thesis;
end;
hence thesis by
PROB_1: 25;
end;
then
reconsider F as
SetSequence of Sigma;
(e
* (
Special_Function4 (k,n2))) is
one-to-one & (
dom (e
* (
Special_Function4 (k,n2))))
<>
{} by
A61,
FUNCT_1: 24;
then
consider f be
sequence of
NAT such that
A70: f
= (e
* (
Special_Function4 (k,n2))) & f is
one-to-one & (
dom f)
<>
{} ;
A71: for q be
object st q
in
NAT holds (F
. q)
= ((A
* f)
. q)
proof
let q be
object;
assume q
in
NAT ;
then
reconsider q as
Element of
NAT ;
(
dom (A
* e))
=
NAT by
FUNCT_2:def 1;
then
A72: ((A
* e)
. ((
Special_Function4 (k,n2))
. q))
= (A
. (e
. ((
Special_Function4 (k,n2))
. q))) by
FUNCT_1: 12;
(
dom ((A
* e)
* (
Special_Function4 (k,n2))))
=
NAT by
FUNCT_2:def 1;
then
A73: (((A
* e)
* (
Special_Function4 (k,n2)))
. q)
= (A
. (e
. ((
Special_Function4 (k,n2))
. q))) by
A72,
FUNCT_1: 12;
(
dom (e
* (
Special_Function4 (k,n2))))
=
NAT by
FUNCT_2:def 1;
then
A74: (((A
* e)
* (
Special_Function4 (k,n2)))
. q)
= (A
. ((e
* (
Special_Function4 (k,n2)))
. q)) by
A73,
FUNCT_1: 12;
(
dom (A
* f))
=
NAT by
FUNCT_2:def 1;
hence thesis by
A70,
A74,
A62,
A67,
FUNCT_1: 12;
end;
A75: (Prob
. (((
Partial_Intersection (
Complement F))
. k)
/\ ((
Partial_Intersection (F
^\ ((k
+
0 )
+ 1)))
. (q
+ 1))))
= (((
Partial_Product (Prob
* (
Complement F)))
. k)
* ((
Partial_Product (Prob
* (F
^\ ((k
+
0 )
+ 1))))
. (q
+ 1))) by
A70,
A71,
A60,
FUNCT_2: 12;
A76: ((
Partial_Intersection (
Complement C))
. k)
= ((
Partial_Intersection (
Complement F))
. k)
proof
A77: for x be
set holds (for knat be
Nat st knat
<= k holds (x
in ((
Complement C)
. knat) iff x
in ((
Complement F)
. knat)))
proof
let x be
set;
let knat be
Nat;
assume knat
<= k;
then
A78: knat
<= (k
+ 1) by
NAT_1: 13;
reconsider knat as
Element of
NAT by
ORDINAL1:def 12;
(
dom (C
* (
Special_Function4 (k,n2))))
=
NAT by
FUNCT_2:def 1;
then
A79: ((C
* (
Special_Function4 (k,n2)))
. knat)
= (C
. ((
Special_Function4 (k,n2))
. knat)) by
FUNCT_1: 12;
((
Special_Function4 (k,n2))
. knat)
= (
IFGT (knat,(k
+ 1),(knat
+ n2),knat)) & (
IFGT (knat,(k
+ 1),(knat
+ n2),knat))
= knat by
Def5,
A78,
XXREAL_0:def 11;
then ((
Complement F)
. knat)
= ((C
. knat)
` ) by
A67,
A79,
PROB_1:def 2;
hence thesis by
PROB_1:def 2;
end;
A80: for x be
object holds ((for knat be
Nat st knat
<= k holds x
in ((
Complement C)
. knat)) iff (for knat be
Nat st knat
<= k holds x
in ((
Complement F)
. knat)))
proof
let x be
object;
hereby
assume
A81: (for knat be
Nat st knat
<= k holds x
in ((
Complement C)
. knat));
thus (for knat be
Nat st knat
<= k holds x
in ((
Complement F)
. knat))
proof
let knat be
Nat;
assume
A82: knat
<= k;
then x
in ((
Complement C)
. knat) iff x
in ((
Complement F)
. knat) by
A77;
hence thesis by
A82,
A81;
end;
end;
assume
A83: (for knat be
Nat st knat
<= k holds x
in ((
Complement F)
. knat));
thus (for knat be
Nat st knat
<= k holds x
in ((
Complement C)
. knat))
proof
let knat be
Nat;
assume
A84: knat
<= k;
then x
in ((
Complement C)
. knat) iff x
in ((
Complement F)
. knat) by
A77;
hence thesis by
A84,
A83;
end;
end;
for x be
object holds (x
in ((
Partial_Intersection (
Complement C))
. k) iff x
in ((
Partial_Intersection (
Complement F))
. k))
proof
let x be
object;
x
in ((
Partial_Intersection (
Complement C))
. k) iff for knat be
Nat st knat
<= k holds x
in ((
Complement C)
. knat) by
PROB_3: 25;
then x
in ((
Partial_Intersection (
Complement C))
. k) iff for knat be
Nat st knat
<= k holds x
in ((
Complement F)
. knat) by
A80;
hence thesis by
PROB_3: 25;
end;
hence thesis by
TARSKI: 2;
end;
A85: ((
Partial_Intersection (F
^\ (k
+ 1)))
. (q
+ 1))
= ((C
. (k
+ 1))
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q))
proof
A86: for x be
set holds (for knat be
Nat st knat
<= q holds (x
in ((F
^\ ((k
+ 1)
+ 1))
. knat) iff x
in ((C
^\ (((k
+ 1)
+ n2)
+ 1))
. knat)))
proof
let x be
set;
let knat be
Nat;
assume knat
<= q;
reconsider knat as
Element of
NAT by
ORDINAL1:def 12;
A87: (
dom (C
* (
Special_Function4 (k,n2))))
=
NAT by
FUNCT_2:def 1;
set j = (((knat
+ k)
+ 1)
+ 1);
j
> (k
+ 1)
proof
(k
+ 1)
< ((k
+ 1)
+ 1) & (k
+ 2)
<= ((k
+ 2)
+ knat) by
NAT_1: 12,
NAT_1: 13;
hence thesis by
XXREAL_0: 2;
end;
then ((
Special_Function4 (k,n2))
. j)
= (
IFGT (j,(k
+ 1),(j
+ n2),j)) & (
IFGT (j,(k
+ 1),(j
+ n2),j))
= (j
+ n2) by
Def5,
XXREAL_0:def 11;
then (F
. (knat
+ ((k
+ 1)
+ 1)))
= (C
. (knat
+ (((k
+ 1)
+ n2)
+ 1))) by
A67,
A87,
FUNCT_1: 12;
then ((F
^\ ((k
+ 1)
+ 1))
. knat)
= (C
. (knat
+ (((k
+ 1)
+ n2)
+ 1))) by
NAT_1:def 3;
hence thesis by
NAT_1:def 3;
end;
A88: for x be
object holds ((for knat be
Nat st knat
<= q holds x
in ((C
^\ (((k
+ 1)
+ n2)
+ 1))
. knat)) iff (for knat be
Nat st knat
<= q holds x
in ((F
^\ ((k
+ 1)
+ 1))
. knat)))
proof
let x be
object;
hereby
assume
A89: for knat be
Nat st knat
<= q holds x
in ((C
^\ (((k
+ 1)
+ n2)
+ 1))
. knat);
thus (for knat be
Nat st knat
<= q holds x
in ((F
^\ ((k
+ 1)
+ 1))
. knat))
proof
let knat be
Nat;
assume
A90: knat
<= q;
then x
in ((C
^\ (((k
+ 1)
+ n2)
+ 1))
. knat) iff x
in ((F
^\ ((k
+ 1)
+ 1))
. knat) by
A86;
hence thesis by
A90,
A89;
end;
end;
assume
A91: (for knat be
Nat st knat
<= q holds x
in ((F
^\ ((k
+ 1)
+ 1))
. knat));
thus for knat be
Nat st knat
<= q holds x
in ((C
^\ (((k
+ 1)
+ n2)
+ 1))
. knat)
proof
let knat be
Nat;
assume
A92: knat
<= q;
then x
in ((C
^\ (((k
+ 1)
+ n2)
+ 1))
. knat) iff x
in ((F
^\ ((k
+ 1)
+ 1))
. knat) by
A86;
hence thesis by
A92,
A91;
end;
end;
A93: for x be
object holds (x
in ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q) iff x
in ((
Partial_Intersection (F
^\ ((k
+ 1)
+ 1)))
. q))
proof
let x be
object;
x
in ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q) iff for knat be
Nat st knat
<= q holds x
in ((C
^\ (((k
+ 1)
+ n2)
+ 1))
. knat) by
PROB_3: 25;
then x
in ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q) iff for knat be
Nat st knat
<= q holds x
in ((F
^\ ((k
+ 1)
+ 1))
. knat) by
A88;
hence thesis by
PROB_3: 25;
end;
(((
Partial_Intersection (F
^\ ((k
+ 1)
+ 1)))
. q)
/\ (C
. (k
+ 1)))
= ((
Partial_Intersection (F
^\ (k
+ 1)))
. (q
+ 1))
proof
defpred
J[
Nat] means (((
Partial_Intersection (F
^\ ((k
+ 1)
+ 1)))
. $1)
/\ (C
. (k
+ 1)))
= ((
Partial_Intersection (F
^\ (k
+ 1)))
. ($1
+ 1));
A94:
J[
0 ]
proof
(((
Partial_Intersection (F
^\ ((k
+ 1)
+ 1)))
.
0 )
/\ (C
. (k
+ 1)))
= (((F
^\ ((k
+ 1)
+ 1))
.
0 )
/\ (C
. (k
+ 1))) by
PROB_3: 21;
then (((
Partial_Intersection (F
^\ ((k
+ 1)
+ 1)))
.
0 )
/\ (C
. (k
+ 1)))
= ((F
. (
0
+ ((k
+ 1)
+ 1)))
/\ (C
. (k
+ 1))) by
NAT_1:def 3;
then
A95: (((
Partial_Intersection (F
^\ ((k
+ 1)
+ 1)))
.
0 )
/\ (C
. (k
+ 1)))
= (((F
^\ (k
+ 1))
. (
0
+ 1))
/\ (C
. (k
+ 1))) by
NAT_1:def 3;
A96: (
dom (C
* (
Special_Function4 (k,n2))))
=
NAT by
FUNCT_2:def 1;
((
Special_Function4 (k,n2))
. (k
+ 1))
= (
IFGT ((k
+ 1),(k
+ 1),((k
+ 1)
+ n2),(k
+ 1))) & (
IFGT ((k
+ 1),(k
+ 1),((k
+ 1)
+ n2),(k
+ 1)))
= (k
+ 1) by
Def5,
XXREAL_0:def 11;
then (((
Partial_Intersection (F
^\ ((k
+ 1)
+ 1)))
.
0 )
/\ (C
. (k
+ 1)))
= (((F
^\ (k
+ 1))
. (
0
+ 1))
/\ (F
. (
0
+ (k
+ 1)))) by
A67,
A96,
A95,
FUNCT_1: 12;
then (((
Partial_Intersection (F
^\ ((k
+ 1)
+ 1)))
.
0 )
/\ (C
. (k
+ 1)))
= (((F
^\ (k
+ 1))
. (
0
+ 1))
/\ ((F
^\ (k
+ 1))
.
0 )) by
NAT_1:def 3;
then (((
Partial_Intersection (F
^\ ((k
+ 1)
+ 1)))
.
0 )
/\ (C
. (k
+ 1)))
= (((
Partial_Intersection (F
^\ (k
+ 1)))
.
0 )
/\ ((F
^\ (k
+ 1))
. (
0
+ 1))) by
PROB_3: 21;
hence thesis by
PROB_3: 21;
end;
A97: for q be
Nat st
J[q] holds
J[(q
+ 1)]
proof
let q be
Nat;
assume
A98:
J[q];
(((
Partial_Intersection (F
^\ ((k
+ 1)
+ 1)))
. (q
+ 1))
/\ (C
. (k
+ 1)))
= ((((
Partial_Intersection (F
^\ ((k
+ 1)
+ 1)))
. q)
/\ ((F
^\ ((k
+ 1)
+ 1))
. (q
+ 1)))
/\ (C
. (k
+ 1))) by
PROB_3: 21;
then
A99: (((
Partial_Intersection (F
^\ ((k
+ 1)
+ 1)))
. (q
+ 1))
/\ (C
. (k
+ 1)))
= (((
Partial_Intersection (F
^\ (k
+ 1)))
. (q
+ 1))
/\ ((F
^\ ((k
+ 1)
+ 1))
. (q
+ 1))) by
A98,
XBOOLE_1: 16;
((F
^\ ((k
+ 1)
+ 1))
. (q
+ 1))
= ((F
^\ (k
+ 1))
. ((q
+ 1)
+ 1))
proof
((F
^\ ((k
+ 1)
+ 1))
. (q
+ 1))
= (F
. ((q
+ 1)
+ ((k
+ 1)
+ 1))) by
NAT_1:def 3;
then ((F
^\ ((k
+ 1)
+ 1))
. (q
+ 1))
= (F
. (((q
+ 1)
+ 1)
+ (k
+ 1)));
hence thesis by
NAT_1:def 3;
end;
hence thesis by
A99,
PROB_3: 21;
end;
for k be
Nat holds
J[k] from
NAT_1:sch 2(
A94,
A97);
hence thesis;
end;
hence thesis by
A93,
TARSKI: 2;
end;
A100: ((
Partial_Product (Prob
* (F
^\ (k
+ 1))))
. (q
+ 1))
= (((Prob
* C)
. (k
+ 1))
* ((
Partial_Product (Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1))))
. q))
proof
defpred
J[
Nat] means ((
Partial_Product (Prob
* (F
^\ (k
+ 1))))
. ($1
+ 1))
= (((Prob
* C)
. (k
+ 1))
* ((
Partial_Product (Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1))))
. $1));
A101:
J[
0 ]
proof
A102: ((F
^\ (k
+ 1))
. (
0
+ 1))
= ((C
* (
Special_Function4 (k,n2)))
. ((k
+ 1)
+ 1)) by
A67,
NAT_1:def 3;
A103: (
dom (C
* (
Special_Function4 (k,n2))))
=
NAT by
FUNCT_2:def 1;
set j = ((k
+ 1)
+ 1);
j
> (k
+ 1) by
NAT_1: 13;
then ((
Special_Function4 (k,n2))
. j)
= (
IFGT (j,(k
+ 1),(j
+ n2),j)) & (
IFGT (j,(k
+ 1),(j
+ n2),j))
= (j
+ n2) by
Def5,
XXREAL_0:def 11;
then ((F
^\ (k
+ 1))
. (
0
+ 1))
= (C
. (
0
+ (((k
+ 1)
+ n2)
+ 1))) by
A103,
A102,
FUNCT_1: 12;
then
A104: (Prob
. ((F
^\ (k
+ 1))
. (
0
+ 1)))
= (Prob
. ((C
^\ (((k
+ 1)
+ n2)
+ 1))
.
0 )) by
NAT_1:def 3;
(
dom (Prob
* (F
^\ (k
+ 1))))
=
NAT & (
dom (Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1))))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* (F
^\ (k
+ 1)))
. (
0
+ 1))
= (Prob
. ((C
^\ (((k
+ 1)
+ n2)
+ 1))
.
0 )) & (Prob
. ((F
^\ (k
+ 1))
. (
0
+ 1)))
= ((Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1)))
.
0 ) & (Prob
. ((F
^\ (k
+ 1))
. (
0
+ 1)))
= (Prob
. ((C
^\ (((k
+ 1)
+ n2)
+ 1))
.
0 )) by
A104,
FUNCT_1: 12;
then
A105: (((
Partial_Product (Prob
* (F
^\ (k
+ 1))))
.
0 )
* ((Prob
* (F
^\ (k
+ 1)))
. (
0
+ 1)))
= (((Prob
* (F
^\ (k
+ 1)))
.
0 )
* ((Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1)))
.
0 )) by
SERIES_3:def 1;
((Prob
* (F
^\ (k
+ 1)))
.
0 )
= ((Prob
* C)
. (k
+ 1))
proof
A106: ((F
^\ (k
+ 1))
.
0 )
= (F
. (
0
+ (k
+ 1))) by
NAT_1:def 3;
A107: (
dom (C
* (
Special_Function4 (k,n2))))
=
NAT by
FUNCT_2:def 1;
A108: (F
. (k
+ 1))
= (C
. ((
Special_Function4 (k,n2))
. (k
+ 1))) by
A67,
A107,
FUNCT_1: 12;
A109: ((
Special_Function4 (k,n2))
. (k
+ 1))
= (
IFGT ((k
+ 1),(k
+ 1),((k
+ 1)
+ n2),(k
+ 1))) & (
IFGT ((k
+ 1),(k
+ 1),((k
+ 1)
+ n2),(k
+ 1)))
= (k
+ 1) by
Def5,
XXREAL_0:def 11;
(
dom (Prob
* C))
=
NAT by
FUNCT_2:def 1;
then
A110: (Prob
. ((F
^\ (k
+ 1))
.
0 ))
= ((Prob
* C)
. (k
+ 1)) by
A109,
A108,
A106,
FUNCT_1: 12;
(
dom (Prob
* (F
^\ (k
+ 1))))
=
NAT by
FUNCT_2:def 1;
hence thesis by
A110,
FUNCT_1: 12;
end;
then ((
Partial_Product (Prob
* (F
^\ (k
+ 1))))
. (
0
+ 1))
= (((Prob
* C)
. (k
+ 1))
* ((Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1)))
.
0 )) by
A105,
SERIES_3:def 1;
hence thesis by
SERIES_3:def 1;
end;
A111: for q be
Nat st
J[q] holds
J[(q
+ 1)]
proof
let q be
Nat;
assume
A112:
J[q];
A113: ((Prob
* (F
^\ (k
+ 1)))
. ((q
+ 1)
+ 1))
= ((Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. (q
+ 1))
proof
A114: ((F
^\ (k
+ 1))
. ((q
+ 1)
+ 1))
= ((C
* (
Special_Function4 (k,n2)))
. (((q
+ 1)
+ 1)
+ (k
+ 1))) by
A67,
NAT_1:def 3;
A115: (
dom (C
* (
Special_Function4 (k,n2))))
=
NAT by
FUNCT_2:def 1;
set j = (((q
+ 1)
+ 1)
+ (k
+ 1));
j
> (k
+ 1)
proof
(k
+ 1)
< ((k
+ 1)
+ 1) & ((k
+ 1)
+ 1)
<= (((k
+ 1)
+ 1)
+ (q
+ 1)) by
NAT_1: 13,
XREAL_1: 31;
hence thesis by
XXREAL_0: 2;
end;
then ((
Special_Function4 (k,n2))
. j)
= (
IFGT (j,(k
+ 1),(j
+ n2),j)) & (
IFGT (j,(k
+ 1),(j
+ n2),j))
= (j
+ n2) by
Def5,
XXREAL_0:def 11;
then ((F
^\ (k
+ 1))
. ((q
+ 1)
+ 1))
= (C
. ((q
+ 1)
+ (((k
+ 1)
+ n2)
+ 1))) by
A115,
A114,
FUNCT_1: 12;
then
A116: (Prob
. ((F
^\ (k
+ 1))
. ((q
+ 1)
+ 1)))
= (Prob
. ((C
^\ (((k
+ 1)
+ n2)
+ 1))
. (q
+ 1))) by
NAT_1:def 3;
(
dom (Prob
* (F
^\ (k
+ 1))))
=
NAT & (
dom (Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1))))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* (F
^\ (k
+ 1)))
. ((q
+ 1)
+ 1))
= (Prob
. ((C
^\ (((k
+ 1)
+ n2)
+ 1))
. (q
+ 1))) & (Prob
. ((F
^\ (k
+ 1))
. ((q
+ 1)
+ 1)))
= ((Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. (q
+ 1)) & (Prob
. ((F
^\ (k
+ 1))
. ((q
+ 1)
+ 1)))
= (Prob
. ((C
^\ (((k
+ 1)
+ n2)
+ 1))
. (q
+ 1))) by
A116,
FUNCT_1: 12;
hence thesis;
end;
((
Partial_Product (Prob
* (F
^\ (k
+ 1))))
. ((q
+ 1)
+ 1))
= ((((Prob
* C)
. (k
+ 1))
* ((
Partial_Product (Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1))))
. q))
* ((Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. (q
+ 1))) by
A112,
A113,
SERIES_3:def 1;
then ((
Partial_Product (Prob
* (F
^\ (k
+ 1))))
. ((q
+ 1)
+ 1))
= (((Prob
* C)
. (k
+ 1))
* (((
Partial_Product (Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1))))
. q)
* ((Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. (q
+ 1))));
hence thesis by
SERIES_3:def 1;
end;
for k be
Nat holds
J[k] from
NAT_1:sch 2(
A101,
A111);
hence thesis;
end;
defpred
J[
Nat] means (for k be
Element of
NAT st k
<= $1 holds (C
. k)
= (F
. k)) implies ((
Partial_Product (Prob
* (
Complement F)))
. $1)
= ((
Partial_Product (Prob
* (
Complement C)))
. $1);
(
dom (C
* (
Special_Function4 (k,n2))))
=
NAT by
FUNCT_2:def 1;
then
A117: ((C
* (
Special_Function4 (k,n2)))
.
0 )
= (C
. ((
Special_Function4 (k,n2))
.
0 )) by
FUNCT_1: 12;
A118: (
IFGT (
0 ,(k
+ 1),(
0
+ n2),
0 ))
=
0 by
XXREAL_0:def 11;
then ((F
.
0 )
` )
= ((C
.
0 )
` ) by
Def5,
A117,
A67;
then ((
Complement F)
.
0 )
= ((C
.
0 )
` ) by
PROB_1:def 2;
then (Prob
. ((
Complement F)
.
0 ))
= (Prob
. ((
Complement C)
.
0 )) & (
dom (Prob
* (
Complement F)))
=
NAT & (
dom (Prob
* (
Complement C)))
=
NAT by
FUNCT_2:def 1,
PROB_1:def 2;
then (Prob
. ((
Complement F)
.
0 ))
= (Prob
. ((
Complement C)
.
0 )) & ((Prob
* (
Complement F))
.
0 )
= (Prob
. ((
Complement F)
.
0 )) & ((Prob
* (
Complement C))
.
0 )
= (Prob
. ((
Complement C)
.
0 )) by
FUNCT_1: 12;
then
A119: ((
Partial_Product (Prob
* (
Complement F)))
.
0 )
= ((Prob
* (
Complement C))
.
0 ) & (F
.
0 )
= (C
.
0 ) by
A118,
Def5,
A117,
A67,
SERIES_3:def 1;
A120:
J[
0 ] by
A119,
SERIES_3:def 1;
A121: for q be
Nat st
J[q] holds
J[(q
+ 1)]
proof
let q be
Nat;
assume
A122:
J[q];
A123: (for k be
Element of
NAT st k
<= (q
+ 1) holds (C
. k)
= (F
. k)) implies (for k be
Element of
NAT st k
<= q holds (C
. k)
= (F
. k))
proof
assume
A124: (for k be
Element of
NAT st k
<= (q
+ 1) holds (C
. k)
= (F
. k));
let k be
Element of
NAT ;
assume k
<= q;
then k
<= (q
+ 1) by
NAT_1: 13;
hence thesis by
A124;
end;
(for k be
Element of
NAT st k
<= (q
+ 1) holds (C
. k)
= (F
. k)) implies ((
Partial_Product (Prob
* (
Complement F)))
. (q
+ 1))
= ((
Partial_Product (Prob
* (
Complement C)))
. (q
+ 1))
proof
assume
A125: (for k be
Element of
NAT st k
<= (q
+ 1) holds (C
. k)
= (F
. k));
then (q
+ 1)
<= (q
+ 1) implies ((C
. (q
+ 1))
` )
= ((F
. (q
+ 1))
` );
then (q
+ 1)
<= (q
+ 1) implies ((
Complement C)
. (q
+ 1))
= ((F
. (q
+ 1))
` ) by
PROB_1:def 2;
then
A126: (((
Partial_Product (Prob
* (
Complement F)))
. q)
* (Prob
. ((
Complement F)
. (q
+ 1))))
= (((
Partial_Product (Prob
* (
Complement C)))
. q)
* (Prob
. ((
Complement C)
. (q
+ 1)))) by
A125,
A123,
A122,
PROB_1:def 2;
(
dom (Prob
* (
Complement C)))
=
NAT & (
dom (Prob
* (
Complement F)))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* (
Complement C))
. (q
+ 1))
= (Prob
. ((
Complement C)
. (q
+ 1))) & ((Prob
* (
Complement F))
. (q
+ 1))
= (Prob
. ((
Complement F)
. (q
+ 1))) by
FUNCT_1: 12;
then ((
Partial_Product (Prob
* (
Complement F)))
. (q
+ 1))
= (((
Partial_Product (Prob
* (
Complement C)))
. q)
* ((Prob
* (
Complement C))
. (q
+ 1))) by
A126,
SERIES_3:def 1;
hence thesis by
SERIES_3:def 1;
end;
hence thesis;
end;
A127: for k be
Nat holds
J[k] from
NAT_1:sch 2(
A120,
A121);
for q be
Element of
NAT st q
<= k holds (C
. q)
= (F
. q)
proof
let q be
Element of
NAT ;
assume q
<= k;
then
A128: q
<= (k
+ 1) by
NAT_1: 13;
A129: (
dom (C
* (
Special_Function4 (k,n2))))
=
NAT by
FUNCT_2:def 1;
((
Special_Function4 (k,n2))
. q)
= (
IFGT (q,(k
+ 1),(q
+ n2),q)) & (
IFGT (q,(k
+ 1),(q
+ n2),q))
= q by
Def5,
A128,
XXREAL_0:def 11;
hence thesis by
A129,
A67,
FUNCT_1: 12;
end;
then (Prob
. (((
Partial_Intersection (
Complement C))
. k)
/\ ((C
. (k
+ 1))
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q))))
= (((
Partial_Product (Prob
* (
Complement C)))
. k)
* (((Prob
* C)
. (k
+ 1))
* ((
Partial_Product (Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1))))
. q))) by
A127,
A100,
A85,
A76,
A75;
hence thesis by
XBOOLE_1: 16;
end;
hence thesis by
A65,
A64,
PROB_1: 33,
XBOOLE_1: 17;
end;
((Prob
* C)
. (k
+ 1))
= (1
- ((Prob
* (
Complement C))
. (k
+ 1)))
proof
(C
. (k
+ 1))
= (((C
. (k
+ 1))
` )
` ) & (((C
. (k
+ 1))
` )
` )
= (Omega
\ ((C
. (k
+ 1))
` )) by
SUBSET_1:def 4;
then (Prob
. (C
. (k
+ 1)))
= (Prob
. ((
[#] Sigma)
\ ((C
. (k
+ 1))
` ))) & ((C
. (k
+ 1))
` ) is
Event of Sigma by
PROB_1: 20;
then
A130: (Prob
. (C
. (k
+ 1)))
= (1
- (Prob
. ((C
. (k
+ 1))
` ))) by
PROB_1: 32;
(
dom (Prob
* C))
=
NAT by
FUNCT_2:def 1;
then
A131: ((Prob
* C)
. (k
+ 1))
= (1
- (Prob
. ((C
. (k
+ 1))
` ))) by
A130,
FUNCT_1: 12;
(
dom (Prob
* (
Complement C)))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* (
Complement C))
. (k
+ 1))
= (Prob
. ((
Complement C)
. (k
+ 1))) by
FUNCT_1: 12;
hence thesis by
A131,
PROB_1:def 2;
end;
then (Prob
. (((
Partial_Intersection (
Complement C))
. (k
+ 1))
/\ ((
Partial_Intersection (C
^\ (((k
+ 1)
+ n2)
+ 1)))
. q)))
= ((((Prob
* (
Complement C))
. (k
+ 1))
* ((
Partial_Product (Prob
* (
Complement C)))
. k))
* ((
Partial_Product (Prob
* (C
^\ (((k
+ 1)
+ n2)
+ 1))))
. q)) by
A66;
hence thesis by
SERIES_3:def 1;
end;
A132: for k be
Nat holds
J[k] from
NAT_1:sch 2(
A36,
A59);
ex e be
sequence of
NAT st (A
* e)
= A & e is
one-to-one & (
dom e)
<>
{}
proof
set e = (
Special_Function2
0 );
A133: (
dom e)
<>
{} ;
A is
sequence of (
bool Omega) & (A
* e) is
sequence of (
bool Omega) & for n be
object st n
in
NAT holds ((A
* e)
. n)
= (A
. n)
proof
for n be
object st n
in
NAT holds ((A
* e)
. n)
= (A
. n) & (A
. (e
. n))
= (A
. n)
proof
let n be
object;
assume n
in
NAT ;
then
reconsider n as
Element of
NAT ;
A135: (e
. n)
= (n
+
0 ) by
Def3;
(
dom (A
* e))
=
NAT by
FUNCT_2:def 1;
hence thesis by
A135,
FUNCT_1: 12;
end;
hence thesis;
end;
hence thesis by
A133,
FUNCT_2: 12;
end;
hence (Prob
. (((
Partial_Intersection (
Complement A))
. n1)
/\ ((
Partial_Intersection (A
^\ ((n1
+ n2)
+ 1)))
. q)))
= (((
Partial_Product (Prob
* (
Complement A)))
. n1)
* ((
Partial_Product (Prob
* (A
^\ ((n1
+ n2)
+ 1))))
. q)) by
A132;
end;
((n
- n1)
- 1) is
Element of
NAT
proof
(n1
+ 1)
<= n by
A1,
NAT_1: 13;
then ((n1
+ 1)
- 1)
<= (n
- 1) by
XREAL_1: 9;
then n1
<= (n
- 1) & (n
- 1) is
Element of
NAT by
A1,
NAT_1: 20;
then ((n
- 1)
- n1) is
Element of
NAT by
NAT_1: 21;
hence thesis;
end;
hence thesis by
A35;
end;
theorem ::
BOR_CANT:7
Th7: ((
Partial_Intersection (
Complement A))
. n)
= (((
Partial_Union A)
. n)
` )
proof
for x be
object holds (x
in ((
Partial_Intersection (
Complement A))
. n) iff x
in (((
Partial_Union A)
. n)
` ))
proof
let x be
object;
hereby
assume
A1: x
in ((
Partial_Intersection (
Complement A))
. n);
for knat be
Nat st knat
<= n holds not x
in (A
. knat)
proof
let knat be
Nat;
assume knat
<= n;
then
A2: x
in ((
Complement A)
. knat) by
A1,
PROB_3: 25;
reconsider knat as
Element of
NAT by
ORDINAL1:def 12;
((
Complement A)
. knat)
= ((A
. knat)
` ) by
PROB_1:def 2;
then ((
Complement A)
. knat)
= (Omega
\ (A
. knat)) by
SUBSET_1:def 4;
hence thesis by
A2,
XBOOLE_0:def 5;
end;
then
A3: not x
in ((
Partial_Union A)
. n) by
PROB_3: 26;
x
in (Omega
\ ((
Partial_Union A)
. n)) by
A1,
A3,
XBOOLE_0:def 5;
hence x
in (((
Partial_Union A)
. n)
` ) by
SUBSET_1:def 4;
end;
assume
A4: x
in (((
Partial_Union A)
. n)
` );
x
in (Omega
\ ((
Partial_Union A)
. n)) by
A4,
SUBSET_1:def 4;
then
A5: x
in Omega & not x
in ((
Partial_Union A)
. n) by
XBOOLE_0:def 5;
for knat be
Nat st knat
<= n holds x
in ((
Complement A)
. knat)
proof
let knat be
Nat;
assume knat
<= n;
then x
in Omega & not x
in (A
. knat) by
A5,
PROB_3: 26;
then
A6: x
in (Omega
\ (A
. knat)) by
XBOOLE_0:def 5;
reconsider knat as
Element of
NAT by
ORDINAL1:def 12;
x
in ((A
. knat)
` ) by
A6,
SUBSET_1:def 4;
hence thesis by
PROB_1:def 2;
end;
hence x
in ((
Partial_Intersection (
Complement A))
. n) by
PROB_3: 25;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
BOR_CANT:8
Th8: (Prob
. ((
Partial_Intersection (
Complement A))
. n))
= (1
- (Prob
. ((
Partial_Union A)
. n)))
proof
A1: (Prob
. ((
Partial_Intersection (
Complement A))
. n))
= (Prob
. (((
Partial_Union A)
. n)
` )) by
Th7;
(Prob
. (((
Partial_Union A)
. n)
` ))
= (Prob
. ((
[#] Sigma)
\ ((
Partial_Union A)
. n))) by
SUBSET_1:def 4;
hence thesis by
A1,
PROB_1: 32;
end;
Lemacik0: for X be
set holds for F be
SetSequence of X, n be
Nat holds ((
superior_setsequence F)
. n)
= (
union (
rng (F
^\ n)))
proof
let X be
set;
let F be
SetSequence of X, n be
Nat;
{ (F
. k) where k be
Nat : n
<= k }
= (
rng (F
^\ n)) by
SETLIM_1: 6;
hence ((
superior_setsequence F)
. n)
= (
union (
rng (F
^\ n))) by
SETLIM_1:def 3;
end;
definition
let X be
set, A be
SetSequence of X;
:: original:
superior_setsequence
redefine
::
BOR_CANT:def7
func
superior_setsequence A ->
SetSequence of X means
:
Def7: for n be
Nat holds (it
. n)
= (
Union (A
^\ n));
compatibility
proof
let f be
SetSequence of X;
thus f
= (
superior_setsequence A) implies for n be
Nat holds (f
. n)
= (
Union (A
^\ n)) by
Lemacik0;
assume
A1: for n be
Nat holds (f
. n)
= (
Union (A
^\ n));
for n be
Element of
NAT holds (f
. n)
= ((
superior_setsequence A)
. n)
proof
let n be
Element of
NAT ;
(f
. n)
= (
Union (A
^\ n)) by
A1
.= ((
superior_setsequence A)
. n) by
Lemacik0;
hence thesis;
end;
hence thesis by
FUNCT_2:def 8;
end;
coherence
proof
for n holds ((
superior_setsequence A)
. n)
= (
union { (A
. k) where k be
Nat : n
<= k }) by
SETLIM_1:def 3;
hence thesis;
end;
end
registration
let Omega be non
empty
set, Sigma be
SigmaField of Omega, A be
SetSequence of Sigma;
cluster (
superior_setsequence A) -> Sigma
-valued;
coherence
proof
defpred
P[
set] means ((
superior_setsequence A)
. $1) is
Event of Sigma;
((
superior_setsequence A)
.
0 )
= (
Union (A
^\
0 )) by
Def7;
then
A1:
P[
0 ] by
PROB_1: 17;
A2: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume ((
superior_setsequence A)
. k) is
Event of Sigma;
(
Union (A
^\ (k
+ 1)))
in Sigma by
PROB_1: 17;
hence thesis by
Def7;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A1,
A2);
hence thesis by
PROB_1: 25;
end;
end
definition
let Omega be non
empty
set, Sigma be
SigmaField of Omega, A be
SetSequence of Sigma;
::
BOR_CANT:def8
func
@lim_sup A ->
Event of Sigma equals (
lim_sup A);
coherence
proof
(
lim_sup A)
= (
@Intersection (
superior_setsequence A));
hence thesis;
end;
end
definition
let X be
set, A be
SetSequence of X;
:: original:
inferior_setsequence
redefine
::
BOR_CANT:def9
func
inferior_setsequence A ->
SetSequence of X means
:
Def9: for n be
Nat holds (it
. n)
= (
Intersection (A
^\ n));
coherence
proof
for n holds ((
inferior_setsequence A)
. n)
= (
meet { (A
. k) where k be
Nat : n
<= k }) by
SETLIM_1:def 2;
hence thesis;
end;
compatibility
proof
let f be
SetSequence of X;
thus f
= (
inferior_setsequence A) implies for n be
Nat holds (f
. n)
= (
Intersection (A
^\ n))
proof
assume
AA: f
= (
inferior_setsequence A);
let n be
Nat;
for x be
object holds x
in ((
inferior_setsequence A)
. n) iff x
in (
Intersection (A
^\ n))
proof
let x be
object;
hereby
assume
A3: x
in ((
inferior_setsequence A)
. n);
for k be
Nat holds x
in ((A
^\ n)
. k)
proof
let k be
Nat;
x
in (A
. (k
+ n)) by
A3,
SETLIM_1: 19;
hence thesis by
NAT_1:def 3;
end;
hence x
in (
Intersection (A
^\ n)) by
PROB_1: 13;
end;
assume
A5: x
in (
Intersection (A
^\ n));
for k be
Nat holds x
in (A
. (n
+ k))
proof
let k be
Nat;
x
in ((A
^\ n)
. k) by
A5,
PROB_1: 13;
hence thesis by
NAT_1:def 3;
end;
hence thesis by
SETLIM_1: 19;
end;
hence thesis by
AA,
TARSKI: 2;
end;
assume
B1: for n be
Nat holds (f
. n)
= (
Intersection (A
^\ n));
for n be
Element of
NAT holds (f
. n)
= ((
inferior_setsequence A)
. n)
proof
let n be
Element of
NAT ;
for x be
object holds x
in (f
. n) iff x
in ((
inferior_setsequence A)
. n)
proof
let x be
object;
hereby
assume x
in (f
. n);
then
A5: x
in (
Intersection (A
^\ n)) by
B1;
for k be
Nat holds x
in (A
. (n
+ k))
proof
let k be
Nat;
x
in ((A
^\ n)
. k) by
A5,
PROB_1: 13;
hence thesis by
NAT_1:def 3;
end;
hence x
in ((
inferior_setsequence A)
. n) by
SETLIM_1: 19;
end;
assume
A3: x
in ((
inferior_setsequence A)
. n);
for k be
Nat holds x
in ((A
^\ n)
. k)
proof
let k be
Nat;
x
in (A
. (k
+ n)) by
A3,
SETLIM_1: 19;
hence thesis by
NAT_1:def 3;
end;
then x
in (
Intersection (A
^\ n)) by
PROB_1: 13;
hence thesis by
B1;
end;
hence thesis by
TARSKI: 2;
end;
then f
= (
inferior_setsequence A);
hence thesis;
end;
end
registration
let Omega be non
empty
set, Sigma be
SigmaField of Omega, A be
SetSequence of Sigma;
cluster (
inferior_setsequence A) -> Sigma
-valued;
coherence
proof
defpred
P[
set] means ((
inferior_setsequence A)
. $1) is
Event of Sigma;
A1: (
Union (
Complement (A
^\
0 ))) is
Event of Sigma by
PROB_1: 26;
((
inferior_setsequence A)
.
0 )
= (
Intersection (A
^\
0 )) by
Def9;
then
A2:
P[
0 ] by
A1,
PROB_1: 20;
A3: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume ((
inferior_setsequence A)
. k) is
Event of Sigma;
A4: (
Union (
Complement (A
^\ (k
+ 1)))) is
Event of Sigma by
PROB_1: 26;
((
inferior_setsequence A)
. (k
+ 1))
= (
Intersection (A
^\ (k
+ 1))) by
Def9;
hence thesis by
A4,
PROB_1: 20;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A2,
A3);
hence thesis by
PROB_1: 25;
end;
end
definition
let Omega be non
empty
set, Sigma be
SigmaField of Omega, A be
SetSequence of Sigma;
::
BOR_CANT:def10
func
@lim_inf A ->
Event of Sigma equals (
lim_inf A);
coherence by
PROB_1: 26;
end
theorem ::
BOR_CANT:9
Th9: ((
inferior_setsequence (
Complement A))
. n)
= (((
superior_setsequence A)
. n)
` )
proof
set B = (
Complement A);
n
in
NAT by
ORDINAL1:def 12;
then ((
inferior_setsequence B)
. n)
= (((
superior_setsequence (
Complement B))
. n)
` ) by
SETLIM_1: 30;
hence thesis;
end;
theorem ::
BOR_CANT:10
Th10: A
is_all_independent_wrt Prob implies (Prob
. ((
Partial_Intersection (
Complement A))
. n))
= ((
Partial_Product (Prob
* (
Complement A)))
. n)
proof
assume
A1: A
is_all_independent_wrt Prob;
defpred
J[
Nat] means (Prob
. ((
Partial_Intersection (
Complement A))
. $1))
= ((
Partial_Product (Prob
* (
Complement A)))
. $1);
(
dom (Prob
* (
Complement A)))
=
NAT by
FUNCT_2:def 1;
then
A2: ((Prob
* (
Complement A))
.
0 )
= (Prob
. ((
Complement A)
.
0 )) by
FUNCT_1: 12;
((
Partial_Product (Prob
* (
Complement A)))
.
0 )
= ((Prob
* (
Complement A))
.
0 ) by
SERIES_3:def 1;
then
A4:
J[
0 ] by
A2,
PROB_3: 21;
A5: for k be
Nat st
J[k] holds
J[(k
+ 1)]
proof
let k be
Nat;
assume
A6:
J[k];
((((
Partial_Intersection (
Complement A))
. k)
/\ ((
Partial_Intersection (
Complement A))
. k))
/\ ((
Complement A)
. (k
+ 1)))
= (((
Partial_Intersection (
Complement A))
. k)
/\ ((A
. (k
+ 1))
` )) by
PROB_1:def 2;
then ((((
Partial_Intersection (
Complement A))
. k)
/\ ((
Partial_Intersection (
Complement A))
. k))
/\ ((
Complement A)
. (k
+ 1)))
= (((
Partial_Intersection (
Complement A))
. k)
/\ (Omega
\ (A
. (k
+ 1)))) by
SUBSET_1:def 4;
then
A7: ((((
Partial_Intersection (
Complement A))
. k)
/\ ((
Partial_Intersection (
Complement A))
. k))
/\ ((
Complement A)
. (k
+ 1)))
= ((((
Partial_Intersection (
Complement A))
. k)
/\ Omega)
\ (((
Partial_Intersection (
Complement A))
. k)
/\ (A
. (k
+ 1)))) by
XBOOLE_1: 50;
A8: (((
Partial_Intersection (
Complement A))
. k)
/\ Omega)
= ((
Partial_Intersection (
Complement A))
. k) by
XBOOLE_1: 28;
(Prob
. (((
Partial_Intersection (
Complement A))
. k)
\ (((
Partial_Intersection (
Complement A))
. k)
/\ (A
. (k
+ 1)))))
= ((Prob
. ((
Partial_Intersection (
Complement A))
. k))
- (Prob
. (((
Partial_Intersection (
Complement A))
. k)
/\ (A
. (k
+ 1))))) by
PROB_1: 33,
XBOOLE_1: 17;
then
A10: (Prob
. ((
Partial_Intersection (
Complement A))
. (k
+ 1)))
= ((Prob
. ((
Partial_Intersection (
Complement A))
. k))
- (Prob
. (((
Partial_Intersection (
Complement A))
. k)
/\ (A
. (k
+ 1))))) by
A7,
A8,
PROB_3: 21;
for A be
SetSequence of Sigma holds for k be
Nat st A
is_all_independent_wrt Prob holds (Prob
. (((
Partial_Intersection (
Complement A))
. k)
/\ (A
. (k
+ 1))))
= (((
Partial_Product (Prob
* (
Complement A)))
. k)
* ((Prob
* A)
. (k
+ 1)))
proof
let A be
SetSequence of Sigma;
let k be
Nat;
assume
A11: A
is_all_independent_wrt Prob;
set n = (k
+ 1);
reconsider n1 = k as
Element of
NAT by
ORDINAL1:def 12;
n1
< (k
+ 1) by
NAT_1: 13;
then (Prob
. (((
Partial_Intersection (
Complement A))
. k)
/\ ((
Partial_Intersection (A
^\ ((k
+
0 )
+ 1)))
. ((n
- k)
- 1))))
= (((
Partial_Product (Prob
* (
Complement A)))
. k)
* ((
Partial_Product (Prob
* (A
^\ ((k
+
0 )
+ 1))))
. ((n
- k)
- 1))) by
A11,
Th6;
then
A12: (Prob
. (((
Partial_Intersection (
Complement A))
. k)
/\ ((A
^\ (k
+ 1))
.
0 )))
= (((
Partial_Product (Prob
* (
Complement A)))
. k)
* ((
Partial_Product (Prob
* (A
^\ (k
+ 1))))
.
0 )) by
PROB_3: 21;
A13: ((A
^\ (k
+ 1))
.
0 )
= (A
. (
0
+ (k
+ 1))) by
NAT_1:def 3;
then
A14: (Prob
. (((
Partial_Intersection (
Complement A))
. k)
/\ (A
. (k
+ 1))))
= (((
Partial_Product (Prob
* (
Complement A)))
. k)
* ((Prob
* (A
^\ (k
+ 1)))
.
0 )) by
A12,
SERIES_3:def 1;
(
dom (Prob
* (A
^\ (k
+ 1))))
=
NAT by
FUNCT_2:def 1;
then
A15: (Prob
. (((
Partial_Intersection (
Complement A))
. k)
/\ (A
. (k
+ 1))))
= (((
Partial_Product (Prob
* (
Complement A)))
. k)
* (Prob
. (A
. (k
+ 1)))) by
A13,
A14,
FUNCT_1: 12;
(
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
hence thesis by
A15,
FUNCT_1: 12;
end;
then
A16: (Prob
. ((
Partial_Intersection (
Complement A))
. (k
+ 1)))
= (((
Partial_Product (Prob
* (
Complement A)))
. k)
- (((
Partial_Product (Prob
* (
Complement A)))
. k)
* ((Prob
* A)
. (k
+ 1)))) by
A6,
A10,
A1;
(A
. (k
+ 1))
= (((A
. (k
+ 1))
` )
` ) & (((A
. (k
+ 1))
` )
` )
= (Omega
\ ((A
. (k
+ 1))
` )) by
SUBSET_1:def 4;
then (Prob
. (A
. (k
+ 1)))
= (Prob
. ((
[#] Sigma)
\ ((A
. (k
+ 1))
` ))) & ((A
. (k
+ 1))
` ) is
Event of Sigma by
PROB_1: 20;
then
A17: (Prob
. (A
. (k
+ 1)))
= (1
- (Prob
. ((A
. (k
+ 1))
` ))) by
PROB_1: 32;
(
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
then
A18: ((Prob
* A)
. (k
+ 1))
= (1
- (Prob
. ((A
. (k
+ 1))
` ))) by
A17,
FUNCT_1: 12;
(
dom (Prob
* (
Complement A)))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* (
Complement A))
. (k
+ 1))
= (Prob
. ((
Complement A)
. (k
+ 1))) by
FUNCT_1: 12;
then ((Prob
* A)
. (k
+ 1))
= (1
- ((Prob
* (
Complement A))
. (k
+ 1))) by
A18,
PROB_1:def 2;
then (Prob
. ((
Partial_Intersection (
Complement A))
. (k
+ 1)))
= ((((
Partial_Product (Prob
* (
Complement A)))
. k)
- ((
Partial_Product (Prob
* (
Complement A)))
. k))
+ (((
Partial_Product (Prob
* (
Complement A)))
. k)
* ((Prob
* (
Complement A))
. (k
+ 1)))) by
A16;
hence thesis by
SERIES_3:def 1;
end;
for k be
Nat holds
J[k] from
NAT_1:sch 2(
A4,
A5);
hence thesis;
end;
::$Canceled
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;
::
BOR_CANT:def11
func
Sum_Shift_Seq (Prob,A) ->
Real_Sequence means
:
Def11: for n be
Nat holds (it
. n)
= (
Sum (Prob
* (A
^\ n)));
existence
proof
deffunc
J(
Nat) = (
In ((
Sum (Prob
* (A
^\ $1))),
REAL ));
consider f be
Real_Sequence such that
A1: for k be
Element of
NAT holds (f
. k)
=
J(k) from
FUNCT_2:sch 4;
take f;
let k be
Nat;
k
in
NAT by
ORDINAL1:def 12;
then (f
. k)
=
J(k) by
A1;
hence thesis;
end;
uniqueness
proof
let J1,J2 be
Real_Sequence;
assume that
A2: for n be
Nat holds (J1
. n)
= (
Sum (Prob
* (A
^\ n))) and
A3: for n be
Nat holds (J2
. n)
= (
Sum (Prob
* (A
^\ n)));
let n be
Element of
NAT ;
(J1
. n)
= (
Sum (Prob
* (A
^\ n))) by
A2;
hence thesis by
A3;
end;
end
theorem ::
BOR_CANT:13
Th13: (
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)
proof
assume
A1: (
Partial_Sums (Prob
* A)) is
convergent;
then
A2: (Prob
* A) is
summable by
SERIES_1:def 2;
A3: for n be
Nat holds
0
<= ((Prob
* (
Partial_Intersection (
superior_setsequence A)))
. n)
proof
let n be
Nat;
(
dom (Prob
* (
Partial_Intersection (
superior_setsequence A))))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* (
Partial_Intersection (
superior_setsequence A)))
. n)
= (Prob
. ((
Partial_Intersection (
superior_setsequence A))
. n)) by
FUNCT_1: 12,
ORDINAL1:def 12;
hence thesis by
PROB_1:def 8;
end;
A5: (
Intersection (
Partial_Intersection (
superior_setsequence A)))
= (
Intersection (
superior_setsequence A)) by
PROB_3: 29;
(
Partial_Intersection (
superior_setsequence A)) is
non-ascending by
PROB_3: 27;
then
A7: (
lim (Prob
* (
Partial_Intersection (
superior_setsequence A))))
= (Prob
. (
Intersection (
Partial_Intersection (
superior_setsequence A)))) & (Prob
* (
Partial_Intersection (
superior_setsequence A))) is
convergent by
PROB_1:def 8;
A8: for A be
SetSequence of Sigma holds for n,s be
Nat holds ((Prob
* (
Partial_Union (A
^\ s)))
. n)
<= ((
Partial_Sums (Prob
* (A
^\ s)))
. n)
proof
let A be
SetSequence of Sigma;
let n,s be
Nat;
defpred
P[
set] means ((Prob
* (
Partial_Union (A
^\ s)))
. $1)
<= ((
Partial_Sums (Prob
* (A
^\ s)))
. $1);
A9: ((
Partial_Sums (Prob
* (A
^\ s)))
.
0 )
= ((Prob
* (A
^\ s))
.
0 ) by
SERIES_1:def 1;
(
dom (Prob
* (A
^\ s)))
=
NAT by
FUNCT_2:def 1;
then
A11: ((Prob
* (A
^\ s))
.
0 )
= (Prob
. ((A
^\ s)
.
0 )) by
FUNCT_1: 12;
A12: (Prob
. ((
Partial_Union (A
^\ s))
.
0 ))
= (Prob
. ((A
^\ s)
.
0 )) by
PROB_3:def 2;
(
dom (Prob
* (
Partial_Union (A
^\ s))))
=
NAT by
FUNCT_2:def 1;
then
A14:
P[
0 ] by
A12,
A11,
A9,
FUNCT_1: 12;
A15: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A16: ((Prob
* (
Partial_Union (A
^\ s)))
. k)
<= ((
Partial_Sums (Prob
* (A
^\ s)))
. k);
A17: (
dom (Prob
* (
Partial_Union (A
^\ s))))
=
NAT by
FUNCT_2:def 1;
A18: (Prob
. (((
Partial_Union (A
^\ s))
. k)
\/ ((A
^\ s)
. (k
+ 1))))
<= ((Prob
. ((
Partial_Union (A
^\ s))
. k))
+ (Prob
. ((A
^\ s)
. (k
+ 1)))) by
PROB_1: 39;
(
dom (Prob
* (A
^\ s)))
=
NAT by
FUNCT_2:def 1;
then
A19: ((Prob
* (A
^\ s))
. (k
+ 1))
= (Prob
. ((A
^\ s)
. (k
+ 1))) by
FUNCT_1: 12;
A20: (Prob
. ((
Partial_Union (A
^\ s))
. (k
+ 1)))
<= ((Prob
. ((
Partial_Union (A
^\ s))
. k))
+ ((Prob
* (A
^\ s))
. (k
+ 1))) implies ((Prob
. ((
Partial_Union (A
^\ s))
. (k
+ 1)))
- (Prob
. ((
Partial_Union (A
^\ s))
. k)))
<= ((Prob
* (A
^\ s))
. (k
+ 1)) by
XREAL_1: 20;
A21: ((Prob
. ((
Partial_Union (A
^\ s))
. (k
+ 1)))
- ((Prob
* (A
^\ s))
. (k
+ 1)))
<= (Prob
. ((
Partial_Union (A
^\ s))
. k)) & (Prob
. ((
Partial_Union (A
^\ s))
. k))
<= ((
Partial_Sums (Prob
* (A
^\ s)))
. k) implies ((Prob
. ((
Partial_Union (A
^\ s))
. (k
+ 1)))
- ((Prob
* (A
^\ s))
. (k
+ 1)))
<= ((
Partial_Sums (Prob
* (A
^\ s)))
. k) by
XXREAL_0: 2;
A22: ((Prob
. ((
Partial_Union (A
^\ s))
. (k
+ 1)))
- ((Prob
* (A
^\ s))
. (k
+ 1)))
<= ((
Partial_Sums (Prob
* (A
^\ s)))
. k) implies (Prob
. ((
Partial_Union (A
^\ s))
. (k
+ 1)))
<= (((
Partial_Sums (Prob
* (A
^\ s)))
. k)
+ ((Prob
* (A
^\ s))
. (k
+ 1))) by
XREAL_1: 20;
A23: (Prob
. ((
Partial_Union (A
^\ s))
. (k
+ 1)))
<= ((
Partial_Sums (Prob
* (A
^\ s)))
. (k
+ 1)) by
A18,
A19,
A20,
A17,
A16,
A21,
A22,
FUNCT_1: 12,
PROB_3:def 2,
SERIES_1:def 1,
XREAL_1: 12,
ORDINAL1:def 12;
(
dom (Prob
* (
Partial_Union (A
^\ s))))
=
NAT by
FUNCT_2:def 1;
hence thesis by
A23,
FUNCT_1: 12;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A14,
A15);
hence thesis;
end;
A24: for k be
Nat holds (
Partial_Sums ((Prob
* A)
^\ k)) is
convergent
proof
let k be
Nat;
((Prob
* A)
^\ k) is
summable by
A2,
SERIES_1: 12;
hence thesis by
SERIES_1:def 2;
end;
A25: for A be
SetSequence of Sigma holds for n be
Nat holds (Prob
* (A
^\ n))
= ((Prob
* A)
^\ n)
proof
let A be
SetSequence of Sigma;
let n be
Nat;
for k be
Element of
NAT holds ((Prob
* (A
^\ n))
. k)
= (((Prob
* A)
^\ n)
. k)
proof
let k be
Element of
NAT ;
(
dom (Prob
* (A
^\ n)))
=
NAT by
FUNCT_2:def 1;
then
A26: ((Prob
* (A
^\ n))
. k)
= (Prob
. ((A
^\ n)
. k)) by
FUNCT_1: 12;
(
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
then
A27: (Prob
. (A
. (n
+ k)))
= ((Prob
* A)
. (n
+ k)) by
FUNCT_1: 12;
((Prob
* A)
. (k
+ n))
= (((Prob
* A)
^\ n)
. k) by
NAT_1:def 3;
hence thesis by
A26,
A27,
NAT_1:def 3;
end;
hence thesis;
end;
A28: for n be
Nat holds (
Partial_Sums (Prob
* (A
^\ n))) is
convergent
proof
let n be
Nat;
(
Partial_Sums (Prob
* (A
^\ n)))
= (
Partial_Sums ((Prob
* A)
^\ n)) by
A25;
hence thesis by
A24;
end;
A29: for n be
Nat holds (
lim (Prob
* (
Partial_Union (A
^\ n))))
<= (
lim (
Partial_Sums (Prob
* (A
^\ n))))
proof
let n be
Nat;
A30: for k be
Nat holds ((Prob
* (
Partial_Union (A
^\ n)))
. k)
<= ((
Partial_Sums (Prob
* (A
^\ n)))
. k) by
A8;
A31: (Prob
* (
Partial_Union (A
^\ n))) is
convergent by
PROB_3: 41;
(
Partial_Sums (Prob
* (A
^\ n))) is
convergent by
A28;
hence thesis by
A31,
A30,
SEQ_2: 18;
end;
A32: for n be
Nat holds (Prob
. (
Union (A
^\ n)))
<= (
lim (
Partial_Sums (Prob
* (A
^\ n))))
proof
let n be
Nat;
(
lim (Prob
* (
Partial_Union (A
^\ n))))
<= (
lim (
Partial_Sums (Prob
* (A
^\ n)))) by
A29;
hence thesis by
PROB_3: 41;
end;
A33: for n be
Nat holds (Prob
. (
Union (A
^\ n)))
<= (
Sum (Prob
* (A
^\ n)))
proof
let n be
Nat;
(
lim (
Partial_Sums (Prob
* (A
^\ n))))
= (
Sum (Prob
* (A
^\ n))) by
SERIES_1:def 3;
hence thesis by
A32;
end;
A34: for n be
Nat holds ((Prob
* (
superior_setsequence A))
. n)
<= ((
Sum_Shift_Seq (Prob,A))
. n)
proof
let n be
Nat;
(
dom (Prob
* (
superior_setsequence A)))
=
NAT by
FUNCT_2:def 1;
then
A36: ((Prob
* (
superior_setsequence A))
. n)
= (Prob
. ((
superior_setsequence A)
. n)) by
FUNCT_1: 12,
ORDINAL1:def 12;
A37: (Prob
. (
Union (A
^\ n)))
<= (
Sum (Prob
* (A
^\ n))) by
A33;
(
Sum (Prob
* (A
^\ n)))
= ((
Sum_Shift_Seq (Prob,A))
. n) by
Def11;
hence thesis by
Def7,
A36,
A37;
end;
A38:
0
<= (
lim (Prob
* (
Partial_Intersection (
superior_setsequence A)))) by
A7,
A3,
SEQ_2: 17;
A39: (
Sum_Shift_Seq (Prob,A)) is
convergent implies (
lim (Prob
* (
Partial_Intersection (
superior_setsequence A))))
<= (
lim (
Sum_Shift_Seq (Prob,A)))
proof
assume
A40: (
Sum_Shift_Seq (Prob,A)) is
convergent;
A41: for n be
Nat holds ((Prob
* (
Partial_Intersection (
superior_setsequence A)))
. n)
<= ((Prob
* (
superior_setsequence A))
. n)
proof
let n be
Nat;
A42: (Prob
. ((
Partial_Intersection (
superior_setsequence A))
. n))
<= (Prob
. ((
superior_setsequence A)
. n)) by
PROB_1: 34,
PROB_3: 23;
A43: (
dom (Prob
* (
Partial_Intersection (
superior_setsequence A))))
=
NAT by
FUNCT_2:def 1;
(
dom (Prob
* (
superior_setsequence A)))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* (
superior_setsequence A))
. n)
= (Prob
. ((
superior_setsequence A)
. n)) by
FUNCT_1: 12,
ORDINAL1:def 12;
hence thesis by
A43,
A42,
FUNCT_1: 12,
ORDINAL1:def 12;
end;
(
lim (Prob
* (
Partial_Intersection (
superior_setsequence A))))
<= (
lim (
Sum_Shift_Seq (Prob,A)))
proof
for n be
Nat holds ((Prob
* (
Partial_Intersection (
superior_setsequence A)))
. n)
<= ((
Sum_Shift_Seq (Prob,A))
. n)
proof
let n be
Nat;
A47: ((Prob
* (
Partial_Intersection (
superior_setsequence A)))
. n)
<= ((Prob
* (
superior_setsequence A))
. n) by
A41;
((Prob
* (
superior_setsequence A))
. n)
<= ((
Sum_Shift_Seq (Prob,A))
. n) by
A34;
hence thesis by
A47,
XXREAL_0: 2;
end;
hence thesis by
A7,
A40,
SEQ_2: 18;
end;
hence thesis;
end;
for A be
SetSequence of Sigma holds (
Partial_Sums (Prob
* A)) is
convergent implies (
0
= (
lim (
Sum_Shift_Seq (Prob,A))) & (
Sum_Shift_Seq (Prob,A)) is
convergent)
proof
let A be
SetSequence of Sigma;
assume
A50: (
Partial_Sums (Prob
* A)) is
convergent;
A52: for n be
Nat holds ((
Sum (Prob
* A))
- (
Sum ((Prob
* A)
^\ (n
+ 1))))
= ((
Partial_Sums (Prob
* A))
. n)
proof
let n be
Nat;
((
Sum (Prob
* A))
- (
Sum ((Prob
* A)
^\ (n
+ 1))))
= ((((
Partial_Sums (Prob
* A))
. n)
+ (
Sum ((Prob
* A)
^\ (n
+ 1))))
- (
Sum ((Prob
* A)
^\ (n
+ 1)))) by
A50,
SERIES_1: 15,
SERIES_1:def 2;
hence thesis;
end;
A53: for n,m be
Nat holds
|.(((
Partial_Sums (Prob
* A))
. m)
- ((
Partial_Sums (Prob
* A))
. n)).|
=
|.((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)).|
proof
let n,m be
Nat;
A54: (((
Partial_Sums (Prob
* A))
. m)
- ((
Partial_Sums (Prob
* A))
. n))
= (((
Partial_Sums (Prob
* A))
. m)
- ((
Sum (Prob
* A))
- (
Sum ((Prob
* A)
^\ (n
+ 1))))) by
A52;
(((
Partial_Sums (Prob
* A))
. m)
- ((
Partial_Sums (Prob
* A))
. n))
= (((
Sum (Prob
* A))
- (
Sum ((Prob
* A)
^\ (m
+ 1))))
- ((
Sum (Prob
* A))
- (
Sum ((Prob
* A)
^\ (n
+ 1))))) by
A52,
A54;
then
A56: (((
Partial_Sums (Prob
* A))
. m)
- ((
Partial_Sums (Prob
* A))
. n))
= ((
Sum ((Prob
* A)
^\ (n
+ 1)))
- (
Sum ((Prob
* A)
^\ (m
+ 1))));
A57: for A be
SetSequence of Sigma holds for n be
Element of
NAT holds (Prob
* (A
^\ n))
= ((Prob
* A)
^\ n)
proof
let A be
SetSequence of Sigma;
let n be
Element of
NAT ;
for k be
Element of
NAT holds ((Prob
* (A
^\ n))
. k)
= (((Prob
* A)
^\ n)
. k)
proof
let k be
Element of
NAT ;
(
dom (Prob
* (A
^\ n)))
=
NAT by
FUNCT_2:def 1;
then
A58: ((Prob
* (A
^\ n))
. k)
= (Prob
. ((A
^\ n)
. k)) by
FUNCT_1: 12;
(
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
then
A59: (Prob
. (A
. (n
+ k)))
= ((Prob
* A)
. (n
+ k)) by
FUNCT_1: 12;
((Prob
* A)
. (k
+ n))
= (((Prob
* A)
^\ n)
. k) by
NAT_1:def 3;
hence thesis by
A58,
A59,
NAT_1:def 3;
end;
hence thesis;
end;
A60: for n be
Nat holds (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
= (
Sum ((Prob
* A)
^\ (n
+ 1)))
proof
let n be
Nat;
A61: (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
= ((
Sum_Shift_Seq (Prob,A))
. (n
+ 1)) by
NAT_1:def 3;
((
Sum_Shift_Seq (Prob,A))
. (n
+ 1))
= (
Sum (Prob
* (A
^\ (n
+ 1)))) by
Def11;
hence thesis by
A57,
A61;
end;
A62:
|.(((
Partial_Sums (Prob
* A))
. m)
- ((
Partial_Sums (Prob
* A))
. n)).|
=
|.((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m)).|
proof
(((
Partial_Sums (Prob
* A))
. m)
- ((
Partial_Sums (Prob
* A))
. n))
= ((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
- (
Sum ((Prob
* A)
^\ (m
+ 1)))) by
A56,
A60;
hence thesis by
A60;
end;
|.((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m)).|
=
|.((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)).|
proof
per cases ;
suppose ((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m))
=
0 ;
hence thesis;
end;
suppose
0
< ((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m));
then
A63: (
-
0 )
> (
- ((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m)));
|.((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)).|
= (
- ((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n))) by
A63,
ABSVALUE:def 1;
hence thesis;
end;
suppose ((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m))
<
0 ;
then
|.((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m)).|
= (
- ((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m))) by
ABSVALUE:def 1;
hence thesis;
end;
end;
hence thesis by
A62;
end;
A65: (for sr be
Real st
0
< sr holds ex n be
Nat st for m be
Nat st n
<= m holds
|.(((
Partial_Sums (Prob
* A))
. m)
- ((
Partial_Sums (Prob
* A))
. n)).|
< sr) implies (for sr be
Real st
0
< sr holds ex n be
Nat st for m be
Nat st n
<= m holds
|.((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)).|
< sr)
proof
assume
A66: for sr be
Real st
0
< sr holds ex n be
Nat st for m be
Nat st n
<= m holds
|.(((
Partial_Sums (Prob
* A))
. m)
- ((
Partial_Sums (Prob
* A))
. n)).|
< sr;
let sr be
Real such that
A67:
0
< sr;
consider n be
Nat such that
A68: for m be
Nat st n
<= m holds
|.(((
Partial_Sums (Prob
* A))
. m)
- ((
Partial_Sums (Prob
* A))
. n)).|
< sr by
A66,
A67;
take n;
let m be
Nat such that
A69: n
<= m;
|.(((
Partial_Sums (Prob
* A))
. m)
- ((
Partial_Sums (Prob
* A))
. n)).|
=
|.((((
Sum_Shift_Seq (Prob,A))
^\ 1)
. m)
- (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)).| by
A53;
hence thesis by
A68,
A69;
end;
A70: (
Partial_Sums (Prob
* A)) is
convergent & ((
Sum_Shift_Seq (Prob,A))
^\ 1) is
convergent by
A50,
A65,
SEQ_4: 41;
A71: (
dom (((
Sum_Shift_Seq (Prob,A))
^\ 1)
+ (
Partial_Sums (Prob
* A))))
=
NAT by
FUNCT_2:def 1;
consider B be
Real_Sequence such that
A72: B
= (((
Sum_Shift_Seq (Prob,A))
^\ 1)
+ (
Partial_Sums (Prob
* A)));
reconsider SP = (
Sum (Prob
* A)) as
Element of
REAL by
XREAL_0:def 1;
set B1 = (
NAT
--> SP);
A74: for n be
Nat holds (B1
. n)
= (B
. n)
proof
let n be
Nat;
A75: for n be
Nat holds (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
= (
Sum ((Prob
* A)
^\ (n
+ 1)))
proof
let n be
Nat;
A76: (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
= ((
Sum_Shift_Seq (Prob,A))
. (n
+ 1)) by
NAT_1:def 3;
A77: for A be
SetSequence of Sigma holds for n be
Element of
NAT holds (Prob
* (A
^\ n))
= ((Prob
* A)
^\ n)
proof
let A be
SetSequence of Sigma;
let n be
Element of
NAT ;
for k be
Element of
NAT holds ((Prob
* (A
^\ n))
. k)
= (((Prob
* A)
^\ n)
. k)
proof
let k be
Element of
NAT ;
(
dom (Prob
* (A
^\ n)))
=
NAT by
FUNCT_2:def 1;
then
A78: ((Prob
* (A
^\ n))
. k)
= (Prob
. ((A
^\ n)
. k)) by
FUNCT_1: 12;
(
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
then
A79: (Prob
. (A
. (n
+ k)))
= ((Prob
* A)
. (n
+ k)) by
FUNCT_1: 12;
((Prob
* A)
. (k
+ n))
= (((Prob
* A)
^\ n)
. k) by
NAT_1:def 3;
hence thesis by
A78,
A79,
NAT_1:def 3;
end;
hence thesis;
end;
((
Sum_Shift_Seq (Prob,A))
. (n
+ 1))
= (
Sum (Prob
* (A
^\ (n
+ 1)))) by
Def11;
hence thesis by
A76,
A77;
end;
A81: (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)
= (
Sum ((Prob
* A)
^\ (n
+ 1))) by
A75;
(
Sum (Prob
* A))
= (((
Partial_Sums (Prob
* A))
. n)
+ (
Sum ((Prob
* A)
^\ (n
+ 1)))) by
A50,
SERIES_1: 15,
SERIES_1:def 2;
then (B1
. n)
= (((
Partial_Sums (Prob
* A))
. n)
+ (((
Sum_Shift_Seq (Prob,A))
^\ 1)
. n)) by
A81,
FUNCOP_1: 7,
ORDINAL1:def 12;
hence thesis by
A71,
A72,
VALUED_1:def 1,
ORDINAL1:def 12;
end;
A82: (
lim B1)
= (
lim B)
proof
ex k be
Nat st for n be
Nat st k
<= n holds (B1
. n)
= (B
. n)
proof
take 1;
thus thesis by
A74;
end;
hence thesis by
SEQ_4: 19;
end;
A83: (
Sum (Prob
* A))
= (B1
. 1)
.= (
lim B) by
A82,
SEQ_4: 26;
(
lim B)
= ((
lim ((
Sum_Shift_Seq (Prob,A))
^\ 1))
+ (
lim (
Partial_Sums (Prob
* A)))) by
A72,
A70,
SEQ_2: 6;
then (
Sum (Prob
* A))
= ((
lim ((
Sum_Shift_Seq (Prob,A))
^\ 1))
+ (
Sum (Prob
* A))) by
A83,
SERIES_1:def 3;
hence thesis by
A70,
SEQ_4: 21,
SEQ_4: 22;
end;
hence thesis by
A5,
A7,
A38,
A39,
A1;
end;
theorem ::
BOR_CANT:14
Th14: (for X be
set, A be
SetSequence of X holds for n be
Nat, x be
object holds ((ex k be
Nat st x
in ((A
^\ n)
. k)) iff (ex k be
Nat st k
>= n & x
in (A
. k)))) & (for X be
set, A be
SetSequence of X holds for x be
object holds x
in (
Intersection (
superior_setsequence A)) iff for m be
Nat holds ex n be
Nat st n
>= m & x
in (A
. n)) & (for A be
SetSequence of Sigma holds for x be
object holds x
in (
@Intersection (
superior_setsequence A)) iff for m be
Nat holds ex n be
Nat st n
>= m & x
in (A
. n)) & (for X be
set, A be
SetSequence of X holds for x be
object holds ((x
in (
Union (
inferior_setsequence A))) iff (ex n be
Nat st for k be
Nat st k
>= n holds x
in (A
. k)))) & (for A be
SetSequence of Sigma holds for x be
object holds ((x
in (
Union (
inferior_setsequence A))) iff (ex n be
Nat st for k be
Nat st k
>= n holds x
in (A
. k)))) & (for A be
SetSequence of Sigma holds for x be
Element of Omega holds ((x
in (
Union (
inferior_setsequence (
Complement A)))) iff (ex n be
Nat st for k be
Nat st k
>= n holds not x
in (A
. k))))
proof
A1: for X be
set, A be
SetSequence of X holds for n be
Nat, x be
set holds ((ex k be
Nat st x
in ((A
^\ n)
. k)) iff (ex k be
Nat st k
>= n & x
in (A
. k)))
proof
let X be
set, A be
SetSequence of X;
let n be
Nat, x be
set;
hereby
given k be
Nat such that
A2: x
in ((A
^\ n)
. k);
A3: x
in (A
. (k
+ n)) by
A2,
NAT_1:def 3;
consider k be
Nat such that
A4: x
in (A
. (k
+ n)) by
A3;
consider k be
Nat such that
A5: k
>= n & x
in (A
. k) by
A4,
NAT_1: 11;
thus ex k be
Nat st k
>= n & x
in (A
. k) by
A5;
end;
given k be
Nat such that
A6: k
>= n & x
in (A
. k);
consider knat be
Nat such that
A7: k
= (n
+ knat) by
A6,
NAT_1: 10;
reconsider knat as
Element of
NAT by
ORDINAL1:def 12;
x
in (A
. k) implies x
in ((A
^\ n)
. knat) by
A7,
NAT_1:def 3;
hence thesis by
A6;
end;
A8: for X be
set, A be
SetSequence of X holds for x be
object holds x
in (
Intersection (
superior_setsequence A)) iff for m be
Nat holds ex n be
Nat st n
>= m & x
in (A
. n)
proof
let X be
set, A be
SetSequence of X;
let x be
object;
hereby
assume
A9: x
in (
Intersection (
superior_setsequence A));
A10: for n be
Nat holds (x
in ((
superior_setsequence A)
. n) implies ex k be
Nat st k
>= n & x
in (A
. k))
proof
let n be
Nat;
assume
A11: x
in ((
superior_setsequence A)
. n);
x
in ((
superior_setsequence A)
. n) implies x
in (
Union (A
^\ n)) by
Def7;
then ex k be
Nat st x
in ((A
^\ n)
. k) by
A11,
PROB_1: 12;
then
consider k be
Nat such that
A14: k
>= n & x
in (A
. k) by
A1;
take k;
thus thesis by
A14;
end;
for m be
Nat holds ex n be
Nat st n
>= m & x
in (A
. n)
proof
let m be
Nat;
x
in ((
superior_setsequence A)
. m) by
A9,
PROB_1: 13;
hence thesis by
A10;
end;
hence for m be
Nat holds ex n be
Nat st n
>= m & x
in (A
. n);
end;
assume
A16: for m be
Nat holds ex n be
Nat st n
>= m & x
in (A
. n);
A17: for m be
Nat holds ((ex n be
Nat st n
>= m & x
in (A
. n)) implies (x
in ((
superior_setsequence A)
. m)))
proof
let m be
Nat;
given n be
Nat such that
A18: n
>= m & x
in (A
. n);
ex k be
Nat st x
in ((A
^\ m)
. k) by
A18,
A1;
then x
in (
Union (A
^\ m)) by
PROB_1: 12;
hence thesis by
Def7;
end;
for m be
Nat holds x
in ((
superior_setsequence A)
. m)
proof
let m be
Nat;
ex n be
Nat st n
>= m & x
in (A
. n) by
A16;
hence thesis by
A17;
end;
hence thesis by
PROB_1: 13;
end;
A19: for A be
SetSequence of Sigma holds for x be
object holds x
in (
@Intersection (
superior_setsequence A)) iff for m be
Nat holds ex n be
Nat st n
>= m & x
in (A
. n)
proof
let A be
SetSequence of Sigma;
let x be
object;
(
@Intersection (
superior_setsequence A))
= (
Intersection (
superior_setsequence A)) by
PROB_2:def 1;
hence thesis by
A8;
end;
A20: for X be
set, A be
SetSequence of X holds for x be
object holds (x
in (
Union (
inferior_setsequence A)) iff (ex n be
Nat st for k be
Nat st k
>= n holds x
in (A
. k)))
proof
let X be
set, A be
SetSequence of X;
let x be
object;
hereby
assume x
in (
Union (
inferior_setsequence A));
then
consider n be
Nat such that
A21: x
in ((
inferior_setsequence A)
. n) by
PROB_1: 12;
A22: ((
inferior_setsequence A)
. n)
= (
Intersection (A
^\ n)) by
Def9;
for k be
Nat st k
>= n holds x
in (A
. k)
proof
let k be
Nat;
assume n
<= k;
then
consider knat be
Nat such that
A24: k
= (n
+ knat) by
NAT_1: 10;
reconsider knat as
Element of
NAT by
ORDINAL1:def 12;
x
in (A
. k) iff x
in ((A
^\ n)
. knat) by
A24,
NAT_1:def 3;
hence thesis by
A22,
A21,
PROB_1: 13;
end;
hence ex n be
Nat st for k be
Nat st k
>= n holds x
in (A
. k);
end;
given n be
Nat such that
A26: for k be
Nat st k
>= n holds x
in (A
. k);
set knat = the
Nat;
for s be
Nat holds x
in ((A
^\ n)
. s)
proof
let s be
Nat;
x
in ((A
^\ n)
. s) iff x
in (A
. (n
+ s)) by
NAT_1:def 3;
hence thesis by
A26,
NAT_1: 12;
end;
then x
in (
Intersection (A
^\ n)) by
PROB_1: 13;
then x
in ((
inferior_setsequence A)
. n) by
Def9;
hence thesis by
PROB_1: 12;
end;
for A be
SetSequence of Sigma holds for x be
Element of Omega holds ((x
in (
Union (
inferior_setsequence (
Complement A)))) iff (ex n be
Nat st for k be
Nat st k
>= n holds not x
in (A
. k)))
proof
let A be
SetSequence of Sigma;
let x be
Element of Omega;
hereby
assume x
in (
Union (
inferior_setsequence (
Complement A)));
then
consider n be
Nat such that
A27: x
in ((
inferior_setsequence (
Complement A))
. n) by
PROB_1: 12;
A28: ((
inferior_setsequence (
Complement A))
. n)
= (
Intersection ((
Complement A)
^\ n)) by
Def9;
set m = the
Element of
NAT ;
for k be
Nat st k
>= n holds not x
in (A
. k)
proof
let k be
Nat;
assume
A29: n
<= k;
consider knat be
Nat such that
A30: k
= (n
+ knat) by
A29,
NAT_1: 10;
reconsider knat as
Element of
NAT by
ORDINAL1:def 12;
A31: x
in ((
Complement A)
. k) iff x
in (((
Complement A)
^\ n)
. knat) by
A30,
NAT_1:def 3;
x
in ((A
. k)
` ) by
A28,
A27,
A31,
PROB_1: 13,
PROB_1:def 2;
then x
in (Omega
\ (A
. k)) by
SUBSET_1:def 4;
hence thesis by
XBOOLE_0:def 5;
end;
hence ex n be
Nat st for k be
Nat st k
>= n holds not x
in (A
. k);
end;
given n be
Nat such that
A32: for k be
Nat st k
>= n holds not x
in (A
. k);
set k = the
Element of
NAT ;
A33: for k be
Nat st n
<= k holds x
in ((
Complement A)
. k)
proof
let k be
Nat;
assume
A34: n
<= k;
A35: not x
in (A
. k) by
A34,
A32;
x
in (Omega
\ (A
. k)) by
A35,
XBOOLE_0:def 5;
then x
in ((A
. k)
` ) by
SUBSET_1:def 4;
hence thesis by
PROB_1:def 2;
end;
for s be
Nat holds x
in (((
Complement A)
^\ n)
. s)
proof
let s be
Nat;
x
in (((
Complement A)
^\ n)
. s) iff x
in ((
Complement A)
. (n
+ s)) by
NAT_1:def 3;
hence thesis by
A33,
NAT_1: 12;
end;
then x
in (
Intersection ((
Complement A)
^\ n)) by
PROB_1: 13;
then x
in ((
inferior_setsequence (
Complement A))
. n) by
Def9;
hence x
in (
Union (
inferior_setsequence (
Complement A))) by
PROB_1: 12;
end;
hence thesis by
A1,
A8,
A19,
A20;
end;
Lemma: (
lim_inf A)
= (
@lim_inf A);
theorem ::
BOR_CANT:15
Th15: (
@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
A18: for A holds (
lim_inf A)
= (
@lim_inf A);
A23: (
@lim_inf (
Complement A))
= ((
@lim_sup A)
` )
proof
reconsider CA = (
Complement A) as
SetSequence of Sigma;
for x be
object holds (x
in (
@lim_inf (
Complement A)) iff x
in ((
@lim_sup A)
` ))
proof
let x be
object;
hereby
assume x
in (
@lim_inf (
Complement A));
then x
in (
@lim_inf CA);
then x
in Omega & ex n be
Nat st for k be
Nat st k
>= n holds not x
in (A
. k) by
Th14;
then x
in Omega & not (x
in (
@lim_sup A)) by
Th14;
then x
in (Omega
\ (
@lim_sup A)) by
XBOOLE_0:def 5;
hence x
in ((
@lim_sup A)
` ) by
SUBSET_1:def 4;
end;
assume
A24: x
in ((
@lim_sup A)
` );
x
in (Omega
\ (
@lim_sup A)) by
A24,
SUBSET_1:def 4;
then not x
in (
Intersection (
superior_setsequence A)) by
XBOOLE_0:def 5;
then ex m be
Nat st for n be
Nat st n
>= m holds not x
in (A
. n) by
Th14;
then x
in (
@lim_inf CA) by
A24,
Th14;
hence thesis;
end;
hence thesis by
TARSKI: 2;
end;
((Prob
. (
@lim_inf (
Complement A)))
+ (Prob
. (
@lim_sup A)))
= 1
proof
((Prob
. ((
[#] Sigma)
\ (
@lim_sup A)))
+ (Prob
. (
@lim_sup A)))
= 1 by
PROB_1: 31;
hence thesis by
A23,
SUBSET_1:def 4;
end;
hence thesis by
A18,
A23;
end;
theorem ::
BOR_CANT:16
Th16: ((
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
A1: (
Partial_Sums (Prob
* A)) is
convergent implies (Prob
. (
lim_inf (
Complement A)))
= 1
proof
assume
A2: (
Partial_Sums (Prob
* A)) is
convergent;
A3: (Prob
. (
lim_inf (
Complement A)))
= (Prob
. (
@lim_inf (
Complement A))) by
Lemma;
for A be
SetSequence of Sigma holds (
Partial_Sums (Prob
* A)) is
convergent implies ((Prob
. (
@lim_inf (
Complement A)))
= 1 & (
lim (
Sum_Shift_Seq (Prob,A)))
=
0 & (
Sum_Shift_Seq (Prob,A)) is
convergent)
proof
let A be
SetSequence of Sigma;
assume
A4: (
Partial_Sums (Prob
* A)) is
convergent;
(((Prob
. (
@lim_sup A))
+ (Prob
. (
@lim_inf (
Complement A))))
= (
0
+ (Prob
. (
@lim_inf (
Complement A)))) & (
lim (
Sum_Shift_Seq (Prob,A)))
=
0 & (
Sum_Shift_Seq (Prob,A)) is
convergent) by
A4,
Th13;
hence thesis by
Th15;
end;
hence thesis by
A2,
A3;
end;
A5: for A be
SetSequence of Sigma st (
Partial_Sums (Prob
* A)) is
convergent holds (Prob
. (
lim_sup A))
=
0
proof
let A be
SetSequence of Sigma;
assume
A6: (
Partial_Sums (Prob
* A)) is
convergent;
(Prob
. (
lim_sup A))
= (Prob
. (
@lim_sup A));
hence thesis by
A6,
Th13;
end;
for B be
SetSequence of Sigma st B
is_all_independent_wrt Prob & (
Partial_Sums (Prob
* B)) is
divergent_to+infty holds (Prob
. (
lim_inf (
Complement B)))
=
0 & (Prob
. (
lim_sup B))
= 1
proof
let B be
SetSequence of Sigma;
assume that
A7: B
is_all_independent_wrt Prob and
A8: (
Partial_Sums (Prob
* B)) is
divergent_to+infty;
A9: (Prob
. (
@lim_sup B))
= (Prob
. (
lim_sup B));
A10: (Prob
. (
@lim_inf (
Complement B)))
= (Prob
. (
lim_inf (
Complement B))) by
Lemma;
for B be
SetSequence of Sigma st B
is_all_independent_wrt Prob & (
Partial_Sums (Prob
* B)) is
divergent_to+infty holds (Prob
. (
@lim_inf (
Complement B)))
=
0 & (Prob
. (
@lim_sup B))
= 1
proof
let B be
SetSequence of Sigma;
assume that
A11: B
is_all_independent_wrt Prob and
A12: (
Partial_Sums (Prob
* B)) is
divergent_to+infty;
reconsider CB = (
Complement B) as
SetSequence of Sigma;
A15: (Prob
. (
@lim_inf CB))
= (
lim (Prob
* (
inferior_setsequence (
Complement B)))) by
PROB_2: 10;
A16: for n be
Nat holds ((Prob
* (
inferior_setsequence (
Complement B)))
. n)
=
0
proof
let n be
Nat;
(
dom (Prob
* (
inferior_setsequence (
Complement B))))
=
NAT by
FUNCT_2:def 1;
then
A18: ((Prob
* (
inferior_setsequence (
Complement B)))
. n)
= (Prob
. ((
inferior_setsequence (
Complement B))
. n)) by
FUNCT_1: 12,
ORDINAL1:def 12;
((
inferior_setsequence (
Complement B))
. n)
= (
Intersection ((
Complement B)
^\ n)) by
Def9;
then
A19: ((Prob
* (
inferior_setsequence (
Complement B)))
. n)
= (Prob
. (
Intersection (
Partial_Intersection ((
Complement B)
^\ n)))) by
A18,
PROB_3: 29;
(
Partial_Intersection ((
Complement B)
^\ n)) is
non-ascending by
PROB_3: 27;
then
A20: ((Prob
* (
inferior_setsequence (
Complement B)))
. n)
= (
lim (Prob
* (
Partial_Intersection ((
Complement B)
^\ n)))) by
A19,
PROB_1:def 8;
A21: for k be
Nat holds ((Prob
* (
Partial_Intersection (
Complement (B
^\ n))))
. k)
<= (((1
+ (
Partial_Sums (Prob
* (B
^\ n))))
" )
. k)
proof
let k be
Nat;
A22: for k be
Nat holds (B
^\ k)
is_all_independent_wrt Prob
proof
let k be
Nat;
for C be
SetSequence of Sigma st (ex e be
sequence of
NAT st (e is
one-to-one & (for n be
Nat holds ((B
^\ k)
. (e
. n))
= (C
. n)))) holds (for n be
Nat holds ((
Partial_Product (Prob
* C))
. n)
= (Prob
. ((
Partial_Intersection C)
. n)))
proof
let C be
SetSequence of Sigma;
given e be
sequence of
NAT such that
A23: e is
one-to-one and
A24: for n be
Nat holds ((B
^\ k)
. (e
. n))
= (C
. n);
A25: (B
^\ k)
= (B
* (
Special_Function2 k))
proof
for n be
object st n
in
NAT holds ((B
^\ k)
. n)
= ((B
* (
Special_Function2 k))
. n)
proof
let n be
object;
assume n
in
NAT ;
then
reconsider n as
Element of
NAT ;
(
dom (B
* (
Special_Function2 k)))
=
NAT by
FUNCT_2:def 1;
then
A26: ((B
* (
Special_Function2 k))
. n)
= (B
. ((
Special_Function2 k)
. n)) by
FUNCT_1: 12;
((
Special_Function2 k)
. n)
= (n
+ k) by
Def3;
hence thesis by
A26,
NAT_1:def 3;
end;
hence thesis;
end;
A27: for n be
Nat holds ((B
* (
Special_Function2 k))
. (e
. n))
= (B
. (((
Special_Function2 k)
* e)
. n))
proof
let n be
Nat;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
(
dom (B
* (
Special_Function2 k)))
=
NAT & (
dom ((
Special_Function2 k)
* e))
=
NAT by
FUNCT_2:def 1;
then ((B
* (
Special_Function2 k))
. (e
. n))
= (B
. ((
Special_Function2 k)
. (e
. n))) & (((
Special_Function2 k)
* e)
. n)
= ((
Special_Function2 k)
. (e
. n)) by
FUNCT_1: 12;
hence thesis;
end;
A28: for n be
Nat holds (B
. (((
Special_Function2 k)
* e)
. n))
= (C
. n)
proof
let n be
Nat;
((B
* (
Special_Function2 k))
. (e
. n))
= (C
. n) by
A25,
A24;
hence thesis by
A27;
end;
((
Special_Function2 k)
* e) is
one-to-one by
A23,
FUNCT_1: 24;
hence thesis by
A11,
A28;
end;
hence thesis by
Def6;
end;
A29: for A be
SetSequence of Sigma holds for n be
Nat holds ((
Partial_Product (Prob
* (
Complement A)))
. n)
<= (((1
+ (
Partial_Sums (Prob
* A)))
. n)
" )
proof
let A be
SetSequence of Sigma;
let n be
Nat;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
A30: ((
Partial_Product (Prob
* (
Complement A)))
. n)
<= (1
/ (1
+ ((
Partial_Sums (Prob
* A))
. n)))
proof
((
Partial_Product (Prob
* (
Complement A)))
. n)
<= ((
Partial_Product (
JSum (Prob
* A)))
. n) by
Th4;
then
A31: ((
Partial_Product (Prob
* (
Complement A)))
. n)
<= (
exp_R
. (
- ((
Partial_Sums (Prob
* A))
. n))) by
Th3;
(
exp_R
. (
- ((
Partial_Sums (Prob
* A))
. n)))
<= (1
/ (1
+ ((
Partial_Sums (Prob
* A))
. n)))
proof
A32: for n be
Nat holds ((Prob
* A)
. n)
>=
0
proof
let n be
Nat;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
(
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* A)
. n)
= (Prob
. (A
. n)) by
FUNCT_1: 12;
hence thesis by
PROB_1:def 8;
end;
A33: for n be
Nat holds ((
Partial_Sums (Prob
* A))
. n)
>=
0
proof
let n be
Nat;
defpred
J[
Nat] means ((
Partial_Sums (Prob
* A))
. $1)
>=
0 ;
((
Partial_Sums (Prob
* A))
.
0 )
= ((Prob
* A)
.
0 ) by
SERIES_1:def 1;
then
A34:
J[
0 ] by
A32;
A35: for k be
Nat st
J[k] holds
J[(k
+ 1)]
proof
let k be
Nat;
assume
A36:
J[k];
A37: ((Prob
* A)
. (k
+ 1))
>=
0 by
A32;
((
Partial_Sums (Prob
* A))
. (k
+ 1))
= (((
Partial_Sums (Prob
* A))
. k)
+ ((Prob
* A)
. (k
+ 1))) by
SERIES_1:def 1;
hence thesis by
A36,
A37;
end;
for k be
Nat holds
J[k] from
NAT_1:sch 2(
A34,
A35);
hence thesis;
end;
for x be
Element of
REAL st x
>=
0 holds (
exp_R
. (
- x))
<= (1
/ (1
+ x))
proof
let x be
Element of
REAL ;
assume
A38: x
>=
0 ;
per cases ;
suppose
A39: x
>
0 ;
A40: (
exp_R
. (
- x))
>=
0 by
SIN_COS: 54;
set z = (
- x);
A41: ((
exp_R x)
* (
exp_R z))
= (
exp_R (x
+ z)) by
SIN_COS: 50;
((
exp_R
. (
- x))
* (1
+ x))
<= 1 by
Th2,
A40,
A41,
SIN_COS: 51,
XREAL_1: 64;
hence thesis by
A39,
XREAL_1: 77;
end;
suppose x
<=
0 ;
then x
=
0 by
A38;
hence thesis by
SIN_COS: 51;
end;
end;
hence thesis by
A33;
end;
hence thesis by
A31,
XXREAL_0: 2;
end;
for A be
SetSequence of Sigma holds for n be
Nat holds (1
/ (1
+ ((
Partial_Sums (Prob
* A))
. n)))
= (((1
+ (
Partial_Sums (Prob
* A)))
. n)
" )
proof
let A be
SetSequence of Sigma;
let n be
Nat;
n
in
NAT by
ORDINAL1:def 12;
then (1
/ (1
+ ((
Partial_Sums (Prob
* A))
. n)))
= (1
/ ((1
+ (
Partial_Sums (Prob
* A)))
. n)) by
VALUED_1: 2;
then (1
/ (1
+ ((
Partial_Sums (Prob
* A))
. n)))
= (1
* (((1
+ (
Partial_Sums (Prob
* A)))
. n)
" )) by
XCMPLX_0:def 9;
hence thesis;
end;
hence thesis by
A30;
end;
reconsider k as
Element of
NAT by
ORDINAL1:def 12;
(
dom (Prob
* (
Partial_Intersection (
Complement (B
^\ n)))))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* (
Partial_Intersection (
Complement (B
^\ n))))
. k)
= (Prob
. ((
Partial_Intersection (
Complement (B
^\ n)))
. k)) by
FUNCT_1: 12;
then ((Prob
* (
Partial_Intersection (
Complement (B
^\ n))))
. k)
= ((
Partial_Product (Prob
* (
Complement (B
^\ n))))
. k) by
A22,
Th10;
then ((Prob
* (
Partial_Intersection (
Complement (B
^\ n))))
. k)
<= (((1
+ (
Partial_Sums (Prob
* (B
^\ n))))
. k)
" ) by
A29;
hence thesis by
VALUED_1: 10;
end;
A42: (
Partial_Sums (Prob
* (B
^\ n))) is
divergent_to+infty
proof
per cases ;
suppose n
=
0 ;
hence thesis by
A12,
NAT_1: 47;
end;
suppose n
<>
0 ;
then
reconsider y = (n
- 1) as
Element of
NAT by
NAT_1: 20;
set B2 = (
NAT
--> (
- ((
Partial_Sums (Prob
* B))
. y)));
A44: ((
Partial_Sums (Prob
* B))
+ B2) is
divergent_to+infty by
A12,
LIMFUNC1: 18;
for r be
Real holds ex q be
Nat st for m be
Nat st q
<= m holds r
< ((
Partial_Sums (Prob
* (B
^\ n)))
. m)
proof
let r be
Real;
for r be
Real holds ex q be
Nat st for m be
Nat st q
<= m holds r
< ((
Partial_Sums (Prob
* (B
^\ n)))
. m)
proof
let r be
Real;
A45: for m be
Nat st n
<= m holds (((
Partial_Sums (Prob
* B))
+ B2)
. m)
= ((
Partial_Sums (Prob
* (B
^\ n)))
. (m
- n))
proof
let m be
Nat;
assume n
<= m;
then
consider knat be
Nat such that
A46: m
= (n
+ knat) by
NAT_1: 10;
reconsider knat as
Nat;
defpred
J[
Nat] means (((
Partial_Sums (Prob
* B))
+ B2)
. (n
+ $1))
= ((
Partial_Sums (Prob
* (B
^\ n)))
. ((n
+ $1)
- n));
A47:
J[
0 ]
proof
(
dom ((
Partial_Sums (Prob
* B))
+ B2))
=
NAT by
FUNCT_2:def 1;
then (((
Partial_Sums (Prob
* B))
+ B2)
. n)
= (((
Partial_Sums (Prob
* B))
. n)
+ (B2
. n)) by
VALUED_1:def 1,
ORDINAL1:def 12;
then (((
Partial_Sums (Prob
* B))
+ B2)
. n)
= (((
Partial_Sums (Prob
* B))
. n)
+ (
- ((
Partial_Sums (Prob
* B))
. (n
- 1)))) by
FUNCOP_1: 7,
ORDINAL1:def 12;
then (((
Partial_Sums (Prob
* B))
+ B2)
. n)
= (((
Partial_Sums (Prob
* B))
. n)
- ((
Partial_Sums (Prob
* B))
. (n
- 1)));
then
A49: (((
Partial_Sums (Prob
* B))
+ B2)
. n)
= ((((
Partial_Sums (Prob
* B))
. (n
- 1))
+ ((Prob
* B)
. ((n
- 1)
+ 1)))
- ((
Partial_Sums (Prob
* B))
. (n
- 1))) by
SERIES_1:def 1;
(
dom (Prob
* (B
^\ n)))
=
NAT by
FUNCT_2:def 1;
then
A50: ((Prob
* (B
^\ n))
.
0 )
= (Prob
. ((B
^\ n)
.
0 )) by
FUNCT_1: 12;
A51: ((B
^\ n)
.
0 )
= (B
. (
0
+ n)) by
NAT_1:def 3;
(
dom (Prob
* B))
=
NAT by
FUNCT_2:def 1;
then (((
Partial_Sums (Prob
* B))
+ B2)
. n)
= ((Prob
* (B
^\ n))
.
0 ) by
A51,
A50,
A49,
FUNCT_1: 12,
ORDINAL1:def 12;
hence thesis by
SERIES_1:def 1;
end;
A52: for k be
Nat st
J[k] holds
J[(k
+ 1)]
proof
let k be
Nat;
assume
A54:
J[k];
A55: (
dom ((
Partial_Sums (Prob
* B))
+ B2))
=
NAT by
FUNCT_2:def 1;
(((
Partial_Sums (Prob
* B))
+ B2)
. ((n
+ k)
+ 1))
= (((
Partial_Sums (Prob
* B))
. ((n
+ k)
+ 1))
+ (B2
. ((n
+ k)
+ 1))) by
A55,
VALUED_1:def 1;
then (((
Partial_Sums (Prob
* B))
+ B2)
. ((n
+ k)
+ 1))
= ((((
Partial_Sums (Prob
* B))
. (n
+ k))
+ ((Prob
* B)
. ((n
+ k)
+ 1)))
+ (B2
. ((n
+ k)
+ 1))) by
SERIES_1:def 1;
then (((
Partial_Sums (Prob
* B))
+ B2)
. ((n
+ k)
+ 1))
= ((((
Partial_Sums (Prob
* B))
. (n
+ k))
+ ((Prob
* B)
. ((n
+ k)
+ 1)))
+ (B2
. (n
+ k))) by
FUNCOP_1: 7,
ORDINAL1:def 12;
then (((
Partial_Sums (Prob
* B))
+ B2)
. ((n
+ k)
+ 1))
= ((((
Partial_Sums (Prob
* B))
. (n
+ k))
+ (B2
. (n
+ k)))
+ ((Prob
* B)
. ((n
+ k)
+ 1)));
then
A56: (((
Partial_Sums (Prob
* B))
+ B2)
. ((n
+ k)
+ 1))
= (((
Partial_Sums (Prob
* (B
^\ n)))
. ((n
+ k)
- n))
+ ((Prob
* B)
. ((n
+ k)
+ 1))) by
A55,
A54,
VALUED_1:def 1,
ORDINAL1:def 12;
((Prob
* (B
^\ n))
. (((n
+ k)
- n)
+ 1))
= ((Prob
* B)
. ((n
+ k)
+ 1))
proof
(
dom (Prob
* (B
^\ n)))
=
NAT by
FUNCT_2:def 1;
then
A57: ((Prob
* (B
^\ n))
. (((n
+ k)
- n)
+ 1))
= (Prob
. ((B
^\ n)
. (k
+ 1))) by
FUNCT_1: 12;
A58: ((B
^\ n)
. (k
+ 1))
= (B
. (n
+ (k
+ 1))) by
NAT_1:def 3;
(
dom (Prob
* B))
=
NAT by
FUNCT_2:def 1;
hence thesis by
A58,
A57,
FUNCT_1: 12;
end;
hence thesis by
A56,
SERIES_1:def 1;
end;
for k be
Nat holds
J[k] from
NAT_1:sch 2(
A47,
A52);
hence thesis by
A46;
end;
A59: ex q be
Nat st for m be
Nat st (q
+ n)
<= (m
+ n) holds r
< (((
Partial_Sums (Prob
* B))
+ B2)
. (m
+ n))
proof
consider q be
Nat such that
A60: for m be
Nat st q
<= m holds r
< (((
Partial_Sums (Prob
* B))
+ B2)
. m) by
A44,
LIMFUNC1:def 4;
take q;
let m be
Nat;
assume (q
+ n)
<= (m
+ n);
then q
<= (q
+ n) & (q
+ n)
<= (m
+ n) by
NAT_1: 11;
then q
<= (m
+ n) by
XXREAL_0: 2;
hence thesis by
A60;
end;
consider q be
Nat such that
A61: for m be
Nat st (q
+ n)
<= (m
+ n) holds r
< (((
Partial_Sums (Prob
* B))
+ B2)
. (m
+ n)) by
A59;
take s = (q
+ n);
let m be
Nat;
assume
A62: s
<= m;
set z = (m
+ n);
(((
Partial_Sums (Prob
* B))
+ B2)
. z)
= ((
Partial_Sums (Prob
* (B
^\ n)))
. (z
- n)) by
A45,
NAT_1: 12;
hence thesis by
A62,
A61,
NAT_1: 12;
end;
hence thesis;
end;
hence thesis by
LIMFUNC1:def 4;
end;
end;
A63: for A be
SetSequence of Sigma holds (
Partial_Sums (Prob
* A)) is
divergent_to+infty implies (
lim ((1
+ (
Partial_Sums (Prob
* A)))
" ))
=
0 & ((1
+ (
Partial_Sums (Prob
* A)))
" ) is
convergent
proof
let A be
SetSequence of Sigma;
A64: for A be
SetSequence of Sigma holds (for r be
Real holds ex n be
Nat st for m be
Nat st n
<= m holds r
< ((
Partial_Sums (Prob
* A))
. m)) implies (for r be
Real holds ex n be
Nat st for m be
Nat st n
<= m holds r
< ((1
+ (
Partial_Sums (Prob
* A)))
. m))
proof
let A be
SetSequence of Sigma;
assume
A65: (for r be
Real holds ex n be
Nat st for m be
Nat st n
<= m holds r
< ((
Partial_Sums (Prob
* A))
. m));
let r be
Real;
consider n be
Nat such that
A66: for m be
Nat st n
<= m holds r
< ((
Partial_Sums (Prob
* A))
. m) by
A65;
take n;
for m be
Nat st n
<= m holds r
< ((1
+ (
Partial_Sums (Prob
* A)))
. m)
proof
let m be
Nat;
A67: m
in
NAT by
ORDINAL1:def 12;
assume n
<= m;
then
A68: r
< ((
Partial_Sums (Prob
* A))
. m) by
A66;
A69: ((
Partial_Sums (Prob
* A))
. m)
< (((
Partial_Sums (Prob
* A))
. m)
+ 1) by
XREAL_1: 29;
((1
+ (
Partial_Sums (Prob
* A)))
. m)
= (((
Partial_Sums (Prob
* A))
. m)
+ 1) by
VALUED_1: 2,
A67;
hence thesis by
A68,
A69,
XXREAL_0: 2;
end;
hence thesis;
end;
assume (
Partial_Sums (Prob
* A)) is
divergent_to+infty;
then for r be
Real holds ex n be
Nat st for m be
Nat st n
<= m holds r
< ((
Partial_Sums (Prob
* A))
. m) by
LIMFUNC1:def 4;
then for r be
Real holds ex n be
Nat st for m be
Nat st n
<= m holds r
< ((1
+ (
Partial_Sums (Prob
* A)))
. m) by
A64;
then (1
+ (
Partial_Sums (Prob
* A))) is
divergent_to+infty by
LIMFUNC1:def 4;
hence thesis by
LIMFUNC1: 34;
end;
(
Partial_Intersection (
Complement (B
^\ n))) is
non-ascending by
PROB_3: 27;
then
A70: (Prob
* (
Partial_Intersection (
Complement (B
^\ n)))) is
convergent & ((1
+ (
Partial_Sums (Prob
* (B
^\ n))))
" ) is
convergent by
A42,
A63,
PROB_1:def 8;
A71: (
lim ((1
+ (
Partial_Sums (Prob
* (B
^\ n))))
" ))
=
0 by
A42,
A63;
A72: for k be
Nat holds
0
<= ((Prob
* (
Partial_Intersection (
Complement (B
^\ n))))
. k)
proof
let k be
Nat;
(
dom (Prob
* (
Partial_Intersection (
Complement (B
^\ n)))))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* (
Partial_Intersection (
Complement (B
^\ n))))
. k)
= (Prob
. ((
Partial_Intersection (
Complement (B
^\ n)))
. k)) by
FUNCT_1: 12,
ORDINAL1:def 12;
hence thesis by
PROB_1:def 8;
end;
A74: (
lim (Prob
* (
Partial_Intersection (
Complement (B
^\ n)))))
<=
0 by
A70,
A21,
A71,
SEQ_2: 18;
(
Complement (B
^\ n))
= ((
Complement B)
^\ n)
proof
for k be
object st k
in
NAT holds ((
Complement (B
^\ n))
. k)
= (((
Complement B)
^\ n)
. k)
proof
let k be
object;
assume k
in
NAT ;
then
reconsider k as
Nat;
A75: ((
Complement (B
^\ n))
. k)
= (((B
^\ n)
. k)
` ) by
PROB_1:def 2;
(((
Complement B)
^\ n)
. k)
= ((
Complement B)
. (k
+ n)) by
NAT_1:def 3;
then (((
Complement B)
^\ n)
. k)
= ((B
. (k
+ n))
` ) by
PROB_1:def 2;
hence thesis by
A75,
NAT_1:def 3;
end;
hence thesis;
end;
hence thesis by
A72,
A70,
A74,
A20,
SEQ_2: 17;
end;
set B2 = (
seq_const
0 );
ex n be
Nat st (B2
. n)
=
0
proof
take 1;
thus thesis;
end;
then
A77: (
lim B2)
=
0 by
SEQ_4: 25;
A78: B2 is
convergent & ex k be
Nat st for n be
Nat st k
<= n holds (B2
. n)
= ((Prob
* (
inferior_setsequence (
Complement B)))
. n)
proof
ex k be
Nat st for n be
Nat st k
<= n holds (B2
. n)
= ((Prob
* (
inferior_setsequence (
Complement B)))
. n)
proof
take
0 ;
thus thesis by
A16;
end;
hence thesis;
end;
(Prob
. (
@lim_inf (
Complement B)))
=
0 & ((Prob
. (
@lim_inf (
Complement B)))
+ (Prob
. (
@lim_sup B)))
= 1 by
A15,
A78,
A77,
Th15,
SEQ_4: 19;
hence thesis;
end;
hence thesis by
A9,
A10,
A7,
A8;
end;
hence thesis by
A5,
A1;
end;
theorem ::
BOR_CANT:17
Th17: ( 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)
proof
assume
A1: not (
Partial_Sums (Prob
* A)) is
convergent;
assume
A2: A
is_all_independent_wrt Prob;
A3: for n be
Nat holds ((Prob
* A)
. n)
>=
0
proof
let n be
Nat;
(
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
then ((Prob
* A)
. n)
= (Prob
. (A
. n)) by
FUNCT_1: 12,
ORDINAL1:def 12;
hence thesis by
PROB_1:def 8;
end;
A5: ( not (Prob
* A) is
summable implies not (
Partial_Sums (Prob
* A)) is
bounded_above) & not (Prob
* A) is
summable by
A3,
A1,
SERIES_1: 17,
SERIES_1:def 2;
(
Partial_Sums (Prob
* A)) is
divergent_to+infty by
A5,
A3,
LIMFUNC1: 29,
SERIES_1: 16;
hence thesis by
A2,
Th16;
end;
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)
proof
assume
A1: A
is_all_independent_wrt Prob;
per cases ;
suppose (
Partial_Sums (Prob
* A)) is
convergent;
hence thesis by
Th16;
end;
suppose not (
Partial_Sums (Prob
* A)) is
convergent;
hence thesis by
A1,
Th17;
end;
end;
theorem ::
BOR_CANT:19
((
Partial_Sums (Prob
* (A
^\ (n1
+ 1))))
. n)
<= (((
Partial_Sums (Prob
* A))
. ((n1
+ 1)
+ n))
- ((
Partial_Sums (Prob
* A))
. n1))
proof
A1: (
dom (Prob
* (A
^\ (n1
+ 1))))
=
NAT by
FUNCT_2:def 1;
A2: (
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
defpred
P[
Nat] means ((
Partial_Sums (Prob
* (A
^\ (n1
+ 1))))
. $1)
<= (((
Partial_Sums (Prob
* A))
. (($1
+ n1)
+ 1))
- ((
Partial_Sums (Prob
* A))
. n1));
A3: (((
Partial_Sums (Prob
* A))
. (n1
+ 1))
- ((
Partial_Sums (Prob
* A))
. n1))
= ((((
Partial_Sums (Prob
* A))
. n1)
+ ((Prob
* A)
. (n1
+ 1)))
- ((
Partial_Sums (Prob
* A))
. n1)) by
SERIES_1:def 1;
A4: (Prob
. ((A
^\ (n1
+ 1))
.
0 ))
= (Prob
. (A
. ((n1
+ 1)
+
0 ))) by
NAT_1:def 3;
A5: (Prob
. (A
. (n1
+ 1)))
= ((Prob
* A)
. (n1
+ 1)) by
A2,
FUNCT_1: 12;
A6: ((Prob
* (A
^\ (n1
+ 1)))
.
0 )
= ((Prob
* A)
. (n1
+ 1)) by
A1,
A4,
A5,
FUNCT_1: 12;
A7:
P[
0 ] by
A6,
A3,
SERIES_1:def 1;
A8: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A9: ((
Partial_Sums (Prob
* (A
^\ (n1
+ 1))))
. k)
<= (((
Partial_Sums (Prob
* A))
. ((k
+ n1)
+ 1))
- ((
Partial_Sums (Prob
* A))
. n1));
A10: (((
Partial_Sums (Prob
* (A
^\ (n1
+ 1))))
. k)
+ ((Prob
* (A
^\ (n1
+ 1)))
. (k
+ 1)))
<= ((((
Partial_Sums (Prob
* A))
. ((k
+ n1)
+ 1))
- ((
Partial_Sums (Prob
* A))
. n1))
+ ((Prob
* (A
^\ (n1
+ 1)))
. (k
+ 1))) by
A9,
XREAL_1: 6;
A11: ((
Partial_Sums (Prob
* (A
^\ (n1
+ 1))))
. (k
+ 1))
<= ((((
Partial_Sums (Prob
* A))
. ((k
+ n1)
+ 1))
- ((
Partial_Sums (Prob
* A))
. n1))
+ ((Prob
* (A
^\ (n1
+ 1)))
. (k
+ 1))) by
A10,
SERIES_1:def 1;
A12: (((
Partial_Sums (Prob
* (A
^\ (n1
+ 1))))
. (k
+ 1))
+ ((
Partial_Sums (Prob
* A))
. n1))
<= (((((
Partial_Sums (Prob
* A))
. ((k
+ n1)
+ 1))
+ ((Prob
* (A
^\ (n1
+ 1)))
. (k
+ 1)))
- ((
Partial_Sums (Prob
* A))
. n1))
+ ((
Partial_Sums (Prob
* A))
. n1)) by
A11,
XREAL_1: 6;
A13: ((((
Partial_Sums (Prob
* (A
^\ (n1
+ 1))))
. (k
+ 1))
+ ((
Partial_Sums (Prob
* A))
. n1))
- ((
Partial_Sums (Prob
* A))
. ((k
+ n1)
+ 1)))
<= ((((Prob
* (A
^\ (n1
+ 1)))
. (k
+ 1))
+ ((
Partial_Sums (Prob
* A))
. ((k
+ n1)
+ 1)))
- ((
Partial_Sums (Prob
* A))
. ((k
+ n1)
+ 1))) by
A12,
XREAL_1: 9;
A14: ((A
^\ (n1
+ 1))
. (k
+ 1))
= (A
. ((n1
+ 1)
+ (k
+ 1))) by
NAT_1:def 3;
A15: (
dom (Prob
* A))
=
NAT by
FUNCT_2:def 1;
A16: (
dom (Prob
* (A
^\ (n1
+ 1))))
=
NAT by
FUNCT_2:def 1;
A17: (Prob
. ((A
^\ (n1
+ 1))
. (k
+ 1)))
= ((Prob
* (A
^\ (n1
+ 1)))
. (k
+ 1)) by
A16,
FUNCT_1: 12;
A18: ((((
Partial_Sums (Prob
* (A
^\ (n1
+ 1))))
. (k
+ 1))
+ ((
Partial_Sums (Prob
* A))
. n1))
- ((
Partial_Sums (Prob
* A))
. ((k
+ n1)
+ 1)))
<= ((Prob
* A)
. ((n1
+ k)
+ 2)) by
A13,
A17,
A14,
A15,
FUNCT_1: 12;
A19: (((((
Partial_Sums (Prob
* (A
^\ (n1
+ 1))))
. (k
+ 1))
+ ((
Partial_Sums (Prob
* A))
. n1))
- ((
Partial_Sums (Prob
* A))
. ((k
+ n1)
+ 1)))
+ ((
Partial_Sums (Prob
* A))
. ((k
+ n1)
+ 1)))
<= (((Prob
* A)
. ((n1
+ k)
+ 2))
+ ((
Partial_Sums (Prob
* A))
. ((k
+ n1)
+ 1))) by
A18,
XREAL_1: 6;
A20: ((
Partial_Sums (Prob
* A))
. (((k
+ n1)
+ 1)
+ 1))
= (((
Partial_Sums (Prob
* A))
. ((k
+ n1)
+ 1))
+ ((Prob
* A)
. (((k
+ n1)
+ 1)
+ 1))) by
SERIES_1:def 1;
((((
Partial_Sums (Prob
* (A
^\ (n1
+ 1))))
. (k
+ 1))
+ ((
Partial_Sums (Prob
* A))
. n1))
- ((
Partial_Sums (Prob
* A))
. n1))
<= (((
Partial_Sums (Prob
* A))
. ((k
+ n1)
+ 2))
- ((
Partial_Sums (Prob
* A))
. n1)) by
A19,
A20,
XREAL_1: 9;
hence thesis;
end;
for n be
Nat holds
P[n] from
NAT_1:sch 2(
A7,
A8);
then
P[n];
hence thesis;
end;
theorem ::
BOR_CANT:20
(Prob
. ((
inferior_setsequence (
Complement A))
. n))
= (1
- (Prob
. ((
superior_setsequence A)
. n)))
proof
A1: (Prob
. ((
inferior_setsequence (
Complement A))
. n))
= (Prob
. (((
superior_setsequence A)
. n)
` )) by
Th9;
(Prob
. (((
superior_setsequence A)
. n)
` ))
= (Prob
. ((
[#] Sigma)
\ ((
superior_setsequence A)
. n))) by
SUBSET_1:def 4;
hence thesis by
A1,
PROB_1: 32;
end;
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))
proof
thus (
Complement A)
is_all_independent_wrt Prob implies (Prob
. ((
Partial_Intersection A)
. n))
= ((
Partial_Product (Prob
* A))
. n)
proof
assume
A1: (
Complement A)
is_all_independent_wrt Prob;
((
Partial_Intersection (
Complement (
Complement A)))
. n)
= ((
Partial_Intersection A)
. n) & ((
Partial_Product (Prob
* (
Complement (
Complement A))))
. n)
= ((
Partial_Product (Prob
* A))
. n) & (Prob
. ((
Partial_Intersection (
Complement (
Complement A)))
. n))
= ((
Partial_Product (Prob
* (
Complement (
Complement A))))
. n) by
A1,
Th10;
hence thesis;
end;
assume A
is_all_independent_wrt Prob;
then (Prob
. ((
Partial_Intersection (
Complement A))
. n))
= ((
Partial_Product (Prob
* (
Complement A)))
. n) & (Prob
. ((
Partial_Intersection (
Complement A))
. n))
= (1
- (Prob
. ((
Partial_Union A)
. n))) by
Th10,
Th8;
hence thesis;
end;