:: Borel-Cantelli Lemma
:: by Peter Jaeger
::
:: Received January 31, 2011
:: Copyright (c) 2011-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies BOR_CANT, REALSET1, ABIAN, SIN_COS, ARYTM_3, CARD_3, EQREL_1,
COMPLEX1, NUMBERS, ZFMISC_1, CARD_1, XXREAL_0, NEWTON, REAL_1, RELAT_1,
PROB_1, SEQ_1, SEQ_2, ARYTM_1, ORDINAL2, RPR_1, XBOOLE_0, SUBSET_1,
PROB_2, SERIES_1, NAT_1, FUNCT_1, PROB_3, SERIES_3, LIMFUNC1, SETLIM_1,
XXREAL_2, FUNCOP_1, FUNCT_7, ASYMPT_1, TARSKI, SETFAM_1;
notations TARSKI, XXREAL_0, XCMPLX_0, XREAL_0, ORDINAL1, REAL_1, XBOOLE_0,
SUBSET_1, SETFAM_1, NUMBERS, NAT_1, COMPLEX1, SEQ_1, COMSEQ_2, SEQ_2,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, PROB_1, PROB_2,
SERIES_1, PROB_3, VALUED_0, VALUED_1, ZFMISC_1, LIMFUNC1, SERIES_3,
NEWTON, ABIAN, SIN_COS, SETLIM_1, FUNCT_6;
constructors RELSET_1, BINARITH, SQUARE_1, COMSEQ_3, RVSUM_1, SIN_COS, REAL_1,
LIMFUNC1, SETLIM_1, SEQ_2, SERIES_1, KURATO_0, RINFSUP1, PROB_3,
SERIES_3, ABIAN, NEWTON, NUMBERS, NAT_D, SEQ_4, RFUNCT_1, RCOMP_1,
SEQM_3, FUNCT_4, COMSEQ_2, SEQ_1, SETFAM_1;
registrations FUNCT_2, XCMPLX_0, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS,
XREAL_0, NAT_1, MEMBERED, VALUED_0, VALUED_1, ABIAN, XXREAL_0, RELAT_1,
SEQ_4, NEWTON, FUNCOP_1, PROB_2, PROB_3, SETLIM_1, RELSET_1, SIN_COS,
INT_1, SEQ_1, SEQ_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FUNCT_1, FUNCT_2;
equalities SIN_COS, PROB_1, PROB_2, CARD_3, SETLIM_1;
expansions FUNCT_2;
theorems XCMPLX_0, SIN_COS, SERIES_1, PROB_1, SEQ_2, PROB_3, SUBSET_1,
XBOOLE_0, XBOOLE_1, ABIAN, NAT_1, FUNCT_1, FUNCT_2, XXREAL_0, ORDINAL1,
TARSKI, XREAL_1, PROB_2, ABSVALUE, VALUED_1, SEQ_4, LIMFUNC1, SETLIM_1,
SERIES_3, NEWTON, POWER, FUNCOP_1, XREAL_0;
schemes NAT_1, FUNCT_2;
begin
reserve Omega for non empty set,
Sigma for SigmaField of Omega,
Prob for Probability of Sigma,
A for SetSequence of Sigma,
n,n1,n2 for Nat;
definition
let D be set;
let x,y be ExtReal, a,b be Element of D;
redefine func IFGT(x,y,a,b) -> Element of D; :: redefines IFGT (XXREAL_0, definition)
coherence by XXREAL_0:def 11;
end;
theorem Th1:
for k being Element of NAT,x being Element of REAL st k is odd & x>0 & x<=1
holds ((-x) rExpSeq).(k+1) + ((-x) rExpSeq).(k+2) >= 0
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 being 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 being Nat such that A6: k=2*m+1 by A1,ABIAN:9;
A7: for k being 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 being 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 being 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 being 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 being 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 being Nat holds J3[k] from NAT_1:sch 2(A30,A31);
consider m being 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 Th2:
for x being 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 being 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,12;
(x rExpSeq).1 = x |^ 1 / (1!) by SIN_COS:def 5; then
A5: J[0] by A4,A3,NEWTON:13;
A6: for k being 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 being 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 being 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 being 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,12; then
A22: J[0] by A21,A20;
A23: for k being 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 being 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 being Element of NAT st k is even & k>0 holds
for y being 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 being 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 being Nat such that A36: k=2*m+1 by ABIAN:9;
for k being Element of NAT,x being 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,12;
((-x) rExpSeq).1 = (-x) |^ 1 /(1!) by SIN_COS:def 5; then
A44: J[0] by A41,A42,NEWTON:13;
A45: for k being 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 being Nat holds J[k] from NAT_1:sch 2(A44,A45);
consider m being 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 being Nat holds J[k] from NAT_1:sch 2(A22,A23);
hence thesis;
end;
A50: for n being 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;
func JSum(s) -> Real_Sequence means :Def1:
for d being Nat holds it.d = Sum ((-s.d) rExpSeq);
existence
proof
deffunc U(Nat) = In(Sum( (-s.$1) rExpSeq),REAL);
consider f being 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 being Nat holds f1.d=Sum( (-s.d) rExpSeq) and
A3: for d being 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 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 being 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 being Nat holds J[k] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem 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 being 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 being 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 being 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 being Nat holds J[k] from NAT_1:sch 2(A7,A8);
hence thesis;
end;
definition
let n1,n2 be Nat;
func Special_Function(n1,n2) -> sequence of NAT means :Def2:
for n being 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 being sequence of NAT such that
A1: for n being 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 being Nat holds s1.n=IFGT(n,n1,n+n2,n) and
A3: for n being 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;
func Special_Function2(k) -> sequence of NAT means :Def3:
for n being Nat holds it.n = n+k;
existence
proof
deffunc U(Nat) = In($1+k,NAT);
consider f being sequence of NAT such that
A1: for n being 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 being Nat holds s1.n=n+k and
A3: for n being 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;
func Special_Function3(k) -> sequence of NAT means :Def4:
for n being Nat holds it.n = IFGT(n,k,0,1);
existence
proof
deffunc U(Nat) = IFGT($1,k,0,1);
consider f being sequence of NAT such that
A1: for n being 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 being Nat holds s1.n=IFGT(n,k,0,1) and
A3: for n being 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;
func Special_Function4(n1,n2) -> sequence of NAT means :Def5:
for n being 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 being sequence of NAT such that
A1: for n being 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 being Nat holds s1.n=IFGT(n,n1+1,n+n2,n) and
A3: for n being 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,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,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 Th5:
( for A,B being SetSequence of Sigma
st n>n1 & B=A*Special_Function(n1,n2) holds
(Partial_Product (Prob*B)).n =
(Partial_Product (Prob*A)).n1 *
(Partial_Product (Prob*(A^\(n1+n2+1)))).(n-n1-1) ) &
( for A,B,C being SetSequence of Sigma,
e being sequence of NAT
st n>n1 & C = A*e & B=C*Special_Function(n1,n2) holds
(Partial_Intersection B).n =
(Partial_Intersection C).n1 /\
(Partial_Intersection (C^\(n1+n2+1))).(n-n1-1) )
proof
A1:
for A,B being SetSequence of Sigma
st n>n1 & B=A*Special_Function(n1,n2) holds
(Partial_Product (Prob*B)).n =
(Partial_Product (Prob*A)).n1 *
(Partial_Product (Prob*(A^\(n1+n2+1)))).(n-n1-1)
proof
let A,B be SetSequence of Sigma;
assume that A2: n>n1 and
A3: B=A*Special_Function(n1,n2);
A4: for q being 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 being 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 being 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 being 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 being 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 being 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 being SetSequence of Sigma,
n1,n2,n being Nat,
e being sequence of NAT
st n>n1 & C = A*e & B=C*Special_Function(n1,n2) holds
(Partial_Intersection B).n =
(Partial_Intersection C).n1 /\
(Partial_Intersection (C^\(n1+n2+1))).(n-n1-1)
proof
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 being 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 being 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 being 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 being set holds
((for knat being Nat st knat<=n holds x in B.knat) implies
(for knat being Nat st knat<=n1 holds x in B.knat) &
(for knat being Nat st n1<knat & knat<=n holds x in B.knat)
) by A45,XXREAL_0:2;
A58: for x being object holds
x in (Partial_Intersection (C^\(n1+n2+1))).(n-n1-1) implies
(for qnat being 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 being 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 being 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 being 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 being object holds
(for qnat being 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 being 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 being 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 being 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 being 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 being set holds (x in (Partial_Intersection B).n iff
(for knat being Nat st knat<=n1 holds x in B.knat) &
(for knat being 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 being Nat st knat<=n holds x in B.knat by PROB_3:25;
hence thesis by A57;
end;
A83: for x being set holds ((x in (Partial_Intersection B).n) iff
(x in (Partial_Intersection B).n1 &
(for knat being 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 being Nat st knat<=n1 holds x in B.knat by PROB_3:25;
hence thesis by A82;
end;
for x being 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 being 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;
pred A is_all_independent_wrt Prob means :Def6:
for B being SetSequence of Sigma st
(ex e being sequence of NAT st
(e is one-to-one &
(for n being Nat holds A.(e.n) = B.n) )) holds
(for n being Nat holds (Partial_Product(Prob*B)).n=
Prob.((Partial_Intersection B).n) );
end;
theorem 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 being SetSequence of Sigma,
k,n being 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 being 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 being Nat holds J[k] from NAT_1:sch 2(A10,A11);
hence thesis;
end;
A17: for m,m1,m2 being Element of NAT,
e being sequence of NAT,
C,B being 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 being Nat holds A.((e*Special_Function(m1,m2)).n)=B.n)
proof
for n being 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 being Element of NAT,
e being sequence of NAT,
C,B being 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 being Nat holds A.((e*(Special_Function2(m1))).n)=B.n)
proof
for n being 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 being 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 being sequence of NAT,
q,n2 being Nat,
C being 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 being 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 being 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 being SetSequence of Sigma,
k,n being Element of NAT,
e being 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 being set holds
(for knat being Nat st knat<=n holds x in (C^\k).knat) iff
(for knat being Nat st knat<=n holds x in B.knat)
proof
let x be set;
hereby assume A52: for knat being Nat st knat<=n holds x in (C^\k).knat;
thus for knat being 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 being Nat st knat<=n holds x in B.knat;
thus for knat being 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 being 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 being Nat st knat<=n holds x in ((C^\k)).knat) &
(x in (Partial_Intersection B).n iff
for knat being 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 being 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 being SetSequence of Omega such that
A67: F=C*Special_Function4(k,n2);
F is SetSequence of Sigma
proof
for n being 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 being sequence of NAT such that
A70: f=e*(Special_Function4(k,n2)) & f is one-to-one & dom f <>{};
A71: for q being 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 being set holds
(for knat being 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 being object holds
( (for knat being Nat st knat<=k holds x in (Complement C).knat) iff
(for knat being Nat st knat<=k holds x in (Complement F).knat) )
proof
let x be object;
hereby assume A81: (for knat being Nat st knat<=k holds
x in (Complement C).knat);
thus (for knat being 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 being Nat st knat<=k holds
x in (Complement F).knat);
thus (for knat being 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 being 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 being 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 being 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 being set holds
(for knat being 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,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 being object holds
( (for knat being Nat st knat<=q holds x in ((C^\(k+1+n2+1))).knat) iff
(for knat being Nat st knat<=q holds x in ((F^\(k+1+1))).knat) )
proof
let x be object;
hereby assume A89: for knat being Nat st knat<=q holds
x in ((C^\(k+1+n2+1))).knat;
thus (for knat being 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 being Nat st knat<=q holds
x in ((F^\(k+1+1))).knat);
thus for knat being 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 being 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 being 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 being 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 being 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 being 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 being 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 being Nat holds J[k] from NAT_1:sch 2(A101,A111);
hence thesis;
end;
defpred J[Nat] means
(for k being 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 being Nat st J[q] holds J[q+1]
proof
let q be Nat;
assume A122:J[q];
A123: (for k being Element of NAT st k<=(q+1) holds C.k=F.k) implies
(for k being Element of NAT st k<=q holds C.k=F.k)
proof
assume A124: (for k being 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 being 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 being 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 being Nat holds J[k] from NAT_1:sch 2(A120,A121);
for q being 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 being Nat holds J[k] from NAT_1:sch 2(A36,A59);
ex e being 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 being object st n in NAT holds (A*e).n = A.n
proof
for n being 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 Th7:
(Partial_Intersection Complement A).n = ((Partial_Union A).n)`
proof
for x being 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 being 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 being 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 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: :: MESFUNC8
for X being set
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 is 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;
redefine func superior_setsequence A -> SetSequence of X means :Def7: :: redefines superior_setsequence (SETLIM_1, definition)
for n being Nat holds it.n = Union (A^\n);
compatibility
proof
let f be SetSequence of X;
thus f = superior_setsequence A implies
for n being Nat holds f.n = Union (A^\n) by Lemacik0;
assume
A1: for n being Nat holds f.n = Union (A^\n);
for n being 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 is 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 being 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;
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;
redefine func inferior_setsequence A -> SetSequence of X means :Def9: :: redefines inferior_setsequence (SETLIM_1, definition)
for n being Nat holds it.n = Intersection (A^\n);
coherence
proof
for n holds (inferior_setsequence A).n =
meet {A.k where k is 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 being Nat holds f.n = Intersection (A^\n)
proof
assume
AA: f = inferior_setsequence A;
let n be Nat;
for x being 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 being 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 being 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 being Nat holds f.n = Intersection (A^\n);
for n being Element of NAT holds f.n = (inferior_setsequence A).n
proof
let n be Element of NAT;
for x being 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 being 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 being 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 being 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;
func @lim_inf A -> Event of Sigma equals
lim_inf A;
coherence by PROB_1:26;
end;
theorem 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 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 being 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 being SetSequence of Sigma holds
for k being 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 being Nat holds J[k] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
::$CT 2
definition
let Omega be non empty set;
let Sigma be SigmaField of Omega;
let Prob be Probability of Sigma;
let A be SetSequence of Sigma;
func Sum_Shift_Seq(Prob,A) -> Real_Sequence means :Def11:
for n being Nat holds it.n = Sum (Prob*(A^\n));
existence
proof
deffunc J(Nat) = In(Sum(Prob*(A^\$1)),REAL);
consider f being Real_Sequence such that
A1: for k being 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 being Nat holds J1.n=Sum(Prob*(A^\n)) and
A3: for n being 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 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 being 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 being SetSequence of Sigma holds
for n,s being 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 being 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 being Nat holds P[k] from NAT_1:sch 2(A14,A15);
hence thesis;
end;
A24: for k being 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 being SetSequence of Sigma holds
for n being Nat holds (Prob*(A^\n))=( (Prob*A)^\n )
proof
let A be SetSequence of Sigma;
let n be Nat;
for k being 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 being 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 being Nat holds
lim (Prob * Partial_Union (A^\n)) <=
lim(Partial_Sums(Prob*(A^\n)))
proof
let n be Nat;
A30: for k being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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,def 2;
hence thesis;
end;
A53: for n,m being 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 being SetSequence of Sigma holds
for n being 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 being 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 being 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 being Real st
0<sr ex n being Nat st
for m being Nat st n<=m holds
|.(Partial_Sums(Prob*A)).m -(Partial_Sums(Prob*A)).n.|<sr)
implies
(for sr being Real st 0<sr ex n being Nat st
for m being 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 being Real st 0<sr ex n being Nat st
for m being 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 being Nat such that
A68: for m being 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 being 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 being Nat holds B1.n=B.n
proof
let n be Nat;
A75: for n being 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 being SetSequence of Sigma holds
for n being 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 being 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,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 being Nat st
for n being 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,22;
end;
hence thesis by A5,A7,A38,A39,A1;
end;
theorem Th14:
( for X being set, A being SetSequence of X holds
for n being Nat, x being object holds
( (ex k being Nat st x in (A^\n).k)
iff (ex k being Nat st k>=n & x in A.k) ) ) &
( for X being set, A being SetSequence of X holds
for x being object holds x in Intersection superior_setsequence A iff
for m being Nat holds
ex n being Nat st n>=m & x in A.n ) &
( for A being SetSequence of Sigma holds
for x being object holds
x in @Intersection superior_setsequence A iff
for m being Nat holds
ex n being Nat st n>=m & x in A.n ) &
( for X being set, A being SetSequence of X holds
for x being object holds
( (x in Union inferior_setsequence A ) iff
(ex n being Nat st
for k being Nat st k>=n holds x in A.k ) ) ) &
( for A being SetSequence of Sigma holds
for x being object holds
( (x in Union inferior_setsequence A ) iff
(ex n being Nat st
for k being Nat st k>=n holds x in A.k ) ) ) &
( for A being SetSequence of Sigma holds
for x being Element of Omega holds
( (x in Union inferior_setsequence (Complement A) ) iff
(ex n being Nat st
for k being Nat st k>=n holds not x in A.k ) ) )
proof
A1: for X being set, A being SetSequence of X holds
for n being Nat, x being set holds
( (ex k being Nat st x in (A^\n).k)
iff (ex k being 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 being Nat such that
A2: x in (A^\n).k;
A3: x in A.(k+n) by A2,NAT_1:def 3;
consider k being Nat such that A4: x in A.(k+n) by A3;
consider k being Nat such that A5: k>=n & x in A.k by A4,NAT_1:11;
thus ex k being Nat st k>=n & x in A.k by A5;
end;
given k being Nat such that A6: k>=n & x in A.k;
consider knat being 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 being set, A being SetSequence of X holds
for x being object holds x in Intersection superior_setsequence A iff
for m being Nat holds
ex n being Nat st n>=m & x in A.n
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 being Nat holds
(x in (superior_setsequence A).n implies
ex k being 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 being Nat st x in (A^\n).k by A11,PROB_1:12; then
consider k being Nat such that A14: k>=n & x in A.k by A1;
take k;
thus thesis by A14;
end;
for m being Nat holds
ex n being 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 being Nat holds
ex n being Nat st n>=m & x in A.n;
end;
assume A16: for m being Nat holds
ex n being Nat st n>=m & x in A.n;
A17: for m being Nat holds
( (ex n being Nat st n>=m & x in A.n) implies
(x in (superior_setsequence A).m ) )
proof
let m be Nat;
given n being Nat such that A18: n>=m & x in A.n;
ex k being 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 being Nat holds x in (superior_setsequence A).m
proof
let m be Nat;
ex n being 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 being SetSequence of Sigma holds
for x being object holds
x in @Intersection superior_setsequence A iff
for m being Nat holds
ex n being Nat st n>=m & x in A.n
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 being set, A being SetSequence of X holds
for x being object holds
( x in Union inferior_setsequence A iff
(ex n being Nat st for k being Nat st k>=n holds x in A.k ) )
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 being 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 being Nat st k>=n holds x in A.k
proof
let k be Nat;
assume n<=k; then
consider knat being 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 being Nat st
for k being Nat st k>=n holds x in A.k;
end;
given n being Nat such that
A26: for k being Nat st k>=n holds x in A.k;
set knat = the Nat;
for s being 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 being SetSequence of Sigma holds
for x being Element of Omega holds
( (x in Union inferior_setsequence (Complement A) ) iff
(ex n being Nat st
for k being Nat st k>=n holds not x in A.k ) )
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 being 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 being Nat st k>=n holds not x in A.k
proof
let k be Nat;
assume A29: n<=k;
consider knat being 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,def 2; then
x in Omega \ A.k by SUBSET_1:def 4;
hence thesis by XBOOLE_0:def 5;
end;
hence ex n being Nat st
for k being Nat st k>=n holds not x in A.k;
end;
given n being Nat such that
A32: for k being Nat st k>=n holds not x in A.k;
set k = the Element of NAT;
A33: for k being 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 being 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 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 being 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 being Nat st
for k being 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 being Nat st
for n being 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 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 being 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 being 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 being 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 being 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 being 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 being Nat holds
(Prob*(Partial_Intersection (Complement (B^\n)))).k <=
((1+(Partial_Sums(Prob*(B^\n))))").k
proof
let k be Nat;
A22: for k being Nat holds (B^\k) is_all_independent_wrt Prob
proof
let k be Nat;
for C being SetSequence of Sigma st
(ex e being sequence of NAT st
(e is one-to-one &
(for n being Nat holds
((B^\k)).(e.n) = C.n))) holds
(for n being Nat holds (Partial_Product(Prob*C)).n=
Prob.((Partial_Intersection C).n) )
proof
let C be SetSequence of Sigma;
given e being sequence of NAT such that
A23: e is one-to-one and
A24: for n being Nat holds ((B^\k)).(e.n) = C.n;
A25: (B^\k)=(B*Special_Function2(k))
proof
for n being 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 being 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 being 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 being SetSequence of Sigma holds
for n being 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 being 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 being 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 being 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 being Nat holds J[k] from NAT_1:sch 2(A34,A35);
hence thesis;
end;
for x being 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 being SetSequence of Sigma holds
for n being 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 being Real ex q being Nat st
for m being Nat st q<=m holds r<(Partial_Sums(Prob*(B^\n))).m
proof
let r be Real;
for r being Real ex q being Nat st
for m being Nat st q<=m holds
r<(Partial_Sums(Prob*(B^\n))).m
proof
let r be Real;
A45: for m being 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 being 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 being 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 being Nat holds J[k] from NAT_1:sch 2(A47,A52);
hence thesis by A46;
end;
A59: ex q being Nat st
for m being Nat st (q+n)<=(m+n) holds
r<(Partial_Sums(Prob*B) + B2).(m+n)
proof
consider q being Nat such that
A60: for m being 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 being Nat such that
A61: for m being 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 being 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 being SetSequence of Sigma holds
(for r being Real ex n being Nat st
for m being Nat st n <= m holds
r < (Partial_Sums(Prob*A)).m) implies
(for r being Real ex n being Nat st
for m being Nat st n <= m holds
r < (1+(Partial_Sums(Prob*A))).m )
proof
let A be SetSequence of Sigma;
assume A65: (for r being Real ex n being Nat st
for m being Nat st n <= m holds r < (Partial_Sums(Prob*A)).m);
let r be Real;
consider n being Nat such that
A66: for m being Nat st n <= m holds
r < (Partial_Sums(Prob*A)).m by A65;
take n;
for m being 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 being Real ex n being Nat st
for m being Nat st n <= m holds
r < (Partial_Sums(Prob*A)).m by LIMFUNC1:def 4; then
for r being Real ex n being Nat st
for m being 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 being 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 being 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 being 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 being Nat
st for n being Nat st k<=n
holds B2.n = (Prob*(inferior_setsequence (Complement B) )).n
proof
ex k being Nat st for n being 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 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 being 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,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
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
(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 being 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 being Nat holds P[n] from NAT_1:sch 2(A7,A8); then
P[n];
hence thesis;
end;
theorem
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
( 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;