:: Borel-Cantelli Lemma :: by Peter Jaeger :: :: Received January 31, 2011 :: Copyright (c) 2011 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, XREAL_0, EQREL_1, COMPLEX1, NUMBERS, ORDINAL1, 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; notations XXREAL_0, XCMPLX_0, XREAL_0, SIN_COS, ORDINAL1, REAL_1, XBOOLE_0, SUBSET_1, NUMBERS, NAT_1, COMPLEX1, SEQ_1, SEQ_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, PROB_1, PROB_2, SETLIM_1, SERIES_1, PROB_3, VALUED_0, VALUED_1, ZFMISC_1, LIMFUNC1, SERIES_3, NEWTON, ABIAN; constructors RELSET_1, BINARITH, SQUARE_1, COMSEQ_3, RVSUM_1, SIN_COS, REAL_1, LIMFUNC1, SETLIM_1, SEQ_2, SERIES_1, KURATO_2, RINFSUP1, SEQ_1, PROB_3, SERIES_3, ABIAN, NEWTON, NUMBERS; registrations FUNCT_2, FINSEQ_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, FINSEQ_1, NEWTON, FUNCOP_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions FUNCT_1, FUNCT_2, SIN_COS, PROB_1, SETLIM_1, NEWTON; 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; schemes NAT_1, RECDEF_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 Element of NAT; definition let D be set; let x,y be ext-real number, a,b be Element of D; redefine func IFGT(x,y,a,b) -> Element of D; 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 Element of 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 Element of 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 Element of NAT such that A8: k=2*m by ABIAN:def 2; defpred J2[Element of NAT] means (-x) |^ (2*\$1) > 0; A9: J2[0] by NEWTON:9; A10: for k being Element of NAT st J2[k] holds J2[k+1] proof let k be Element of 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:13; ((-x)*(-x)) >0 by A2; then ((-x)) |^ 2 >0 by NEWTON:100; hence thesis by A11,A12; end; for k being Element of NAT holds J2[k] from NAT_1:sch 1(A9,A10); hence thesis by A8; end; A13: x|^(k+2) / (-x)|^(k+1) = x proof x|^(k+2) = x|^((k+1)+1); then A14: x|^(k+2) = x|^(k+1)*x by NEWTON:11; x|^(k+2) = x*(-x)|^(k+1) by A6,A14,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 A16: 0 < (-x)|^(k+1) by A6,A7; A17: 1 <= ((-x)|^(k+1)) / ((-x)|^(k+1)) by A6,A7,XREAL_1:183; A18: ((-x)|^(k+1)) / ((-x)|^(k+1)) <=1 by A16,XREAL_1:187; ((-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:21; then A20: ((k+2)!)*(((k+1)!)") = ((k+1)+1) * (((k+1)!) * (((k+1)!)")); A21: 1 <= ((k+1)!) / ((k+1)!) by XREAL_1:183; A22: ((k+1)!) / ((k+1)!) <= 1 by XREAL_1:185; ((k+1)!) / ((k+1)!) = 1 by A21,A22,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 A23: x|^(k+2) / (-x)|^(k+1) <= ((k+2)!)/((k+1)!); x|^(k+2) * ((-x)|^(k+1))" <= ((k+2)!)/((k+1)!) by XCMPLX_0:def 9,A23; 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:104; 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 9; then (x rExpSeq).(k+2) <= ((-x) rExpSeq).(k+1) by SIN_COS:def 9; then (x rExpSeq).(k+2) - ((-x) rExpSeq).(k+1) <= (((-x) rExpSeq).(k+1)-((-x) rExpSeq).(k+1)) by XREAL_1:11; 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[Element of NAT] means -(x|^(2*\$1+1)) = (-x)|^(2*\$1+1); A29: (-x)|^(2*0+1) = -x by NEWTON:10; A30: J3[0] by NEWTON:10,A29; A31: for k being Element of NAT st J3[k] holds J3[k+1] proof let k be Element of NAT; assume A32: J3[k]; -(x|^(2*(k+1)+1)) = -((x|^(2*k+1+1))*x) by NEWTON:11; then -(x|^(2*(k+1)+1)) = -((x|^(2*k+1)*x)*x) by NEWTON:11; 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:11; hence thesis by NEWTON:11; end; A33: for k being Element of NAT holds J3[k] from NAT_1:sch 1(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 9; 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 9; end; hence thesis by A28; end; hence thesis by A3,A19,XXREAL_0:2,A13; 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; set B2 = NAT --> (1+x); A2: for n being Element of NAT st x>0 holds B2.n <= (Partial_Sums(x rExpSeq)).(n+1) proof let n be Element of NAT; defpred J[natural number] 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 9 .= 1 by NEWTON:9,18; (x rExpSeq).1 = x |^ 1 / (1!) by SIN_COS:def 9; then (x rExpSeq).1 = x by NEWTON:10,NEWTON:19; then A5: J[0] by A4,A3,FUNCOP_1:13; A6: for k being Element of NAT st J[k] holds J[k+1] proof let k be Element of 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:102; then x |^ ((k+1)+1) / (((k+1)+1)!) >0; hence thesis by SIN_COS:def 9; end; A10: 1+x<=(Partial_Sums(x rExpSeq)).(k+1) by A7,FUNCOP_1:13; (Partial_Sums(x rExpSeq)).(k+1)<= (x rExpSeq).((k+1)+1)+(Partial_Sums(x rExpSeq)).(k+1) by A9,XREAL_1:33; then 1+x<=(Partial_Sums(x rExpSeq)).(k+1)+(x rExpSeq).((k+1)+1) by A10,XXREAL_0:2; hence thesis by A8,FUNCOP_1:13; end; for k being Element of NAT holds J[k] from NAT_1:sch 1(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:41 .= 1+x by FUNCOP_1:13; x rExpSeq is summable by SIN_COS:49; then A13: Partial_Sums (x rExpSeq) is convergent by SERIES_1:def 2; then A14: lim ((Partial_Sums (x rExpSeq))^\1) = lim Partial_Sums (x rExpSeq) & (Partial_Sums (x rExpSeq))^\1 is convergent by SEQ_4:33; lim B2 <= lim ((Partial_Sums(x rExpSeq))^\1) by A13,A11,SEQ_2:32; then lim B2 <= Sum(x rExpSeq) by A14,SERIES_1:def 3; hence thesis by SIN_COS:def 26,A12; end; suppose x=0; hence thesis by SIN_COS:56; 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; set B2 = NAT --> (1-x); A19: for n being Element of NAT holds B2.n <= Partial_Sums( (-x) rExpSeq ).(n+1) proof let n be Element of NAT; defpred J[Element of 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 9; then A21: ((-x) rExpSeq).1 = (-x) by NEWTON:10,NEWTON:19; ((-x) rExpSeq).0 = (-x) |^ 0 / (0!) by SIN_COS:def 9 .= 1 by NEWTON:9,18; then A22: J[0] by A21,A20,FUNCOP_1:13; A23: for k being Element of NAT st J[k] holds J[k+1] proof let k be Element of NAT; assume A24: J[k]; per cases; suppose k is even; then consider m being Element of NAT such that A25: k=2*m by ABIAN:def 2; A26: 1-x <= Partial_Sums( (-x) rExpSeq ).(k+1) by A24,FUNCOP_1:13; 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:102; then y |^ k / (k!) > 0; hence thesis by SIN_COS:def 9; end; suppose y=0; then A30: y|^k=0 by A29,NEWTON:103; y |^ k / (k!) = 0 by A30; hence thesis by SIN_COS:def 9; end; suppose A31:y<0; consider m being Element of 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:13; then A33: y |^ k = (y * y) |^m by NEWTON:12; y |^k >=0 by A31,NEWTON:102,A33; then y |^ k / (k!) >= 0; hence thesis by SIN_COS:def 9; end; end; A34: ((-x) rExpSeq).(k+2) >= 0 by A25,A27; A35: Partial_Sums( (-x) rExpSeq ).(k+1) <= (Partial_Sums( (-x) rExpSeq ).(k+1) + ((-x) rExpSeq).(k+2)) by A34,XREAL_1:33; 1-x <= (Partial_Sums( (-x) rExpSeq ).(k+1) + ((-x) rExpSeq).((k+1)+1)) by A26,A35,XXREAL_0:2; then 1-x <= (Partial_Sums( (-x) rExpSeq )).(k+2) by SERIES_1:def 1; hence thesis by FUNCOP_1:13; end; suppose k is odd; then consider m being Element of NAT such that A36: k=2*m+1 by ABIAN:9; A37: 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[Element of 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 9 .= 1 by NEWTON:9,18; ((-x) rExpSeq).1 = (-x) |^ 1 /(1!) by SIN_COS:def 9; then A43: ((-x) rExpSeq).(1+0) = (-x) by NEWTON:10,NEWTON:19; A44: J[0] by A43,A41,A42; A45: for k being Element of NAT st J[k] holds J[k+1] proof let k be Element of 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 XREAL_1:33,A47; end; hence thesis by A46,XXREAL_0:2; end; A48: for k being Element of NAT holds J[k] from NAT_1:sch 1(A44,A45); consider m being Element of NAT such that A49: k=2*m+1 by A38,ABIAN:9; thus thesis by A48,A49; end; 1-x <= (Partial_Sums( (-x) rExpSeq )).(k+2) by A36,A17,A18,A37; hence thesis by FUNCOP_1:13; end; end; for k being Element of NAT holds J[k] from NAT_1:sch 1(A22,A23); hence thesis; end; A50: for n being Element of NAT holds B2.n <= ((Partial_Sums( (-x) rExpSeq ))^\1).n proof let n be Element of 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:41 .= 1-x by FUNCOP_1:13; ((-x) rExpSeq) is summable by SIN_COS:49; then A52: Partial_Sums ((-x) rExpSeq) is convergent by SERIES_1:def 2; then A53: lim ((Partial_Sums ((-x) rExpSeq))^\1) = lim Partial_Sums ((-x) rExpSeq) & (Partial_Sums ((-x) rExpSeq))^\1 is convergent by SEQ_4:33; lim B2 <= lim ((Partial_Sums((-x) rExpSeq))^\1) by A52,A50,SEQ_2:32; then lim B2 <= Sum((-x) rExpSeq) by A53,SERIES_1:def 3; hence thesis by SIN_COS:def 26,A51; end; hence thesis by A15,A16; end; suppose A54: y>1; 0 < exp_R.(-y) by A54,SIN_COS:58; hence thesis by A54,XREAL_1:51; 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(Element of NAT) = Sum( (-s.\$1) rExpSeq); 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 13; hence thesis by A1; 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[Element of 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 SIN_COS:def 26,A1; A3: for k being Element of NAT st J[k] holds J[k+1] proof let k be Element of NAT; assume A4: J[k]; A5: Partial_Product(JSum(Prob*A)).(k+1) = Partial_Product(JSum(Prob*A)).k * (JSum(Prob*A)).(k+1) by SERIES_3:def 1; A6: Partial_Product(JSum(Prob*A)).(k+1) = exp_R.(-Partial_Sums(Prob*A).k) * Sum( (-(Prob*A).(k+1)) rExpSeq) by A4,A5,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:55; - (Partial_Sums(Prob*A).k + (Prob*A).(k+1)) = - Partial_Sums(Prob*A).(k+1) by SERIES_1:def 1; hence thesis by A7,SIN_COS:def 26,A6; end; for k being Element of NAT holds J[k] from NAT_1:sch 1(A2,A3); hence thesis; end; theorem Th4: Partial_Product(Prob*(@Complement A)).n <= Partial_Product(JSum(Prob*A)).n proof defpred J[Element of 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:22; A3: Partial_Product(Prob*(@Complement A)).0 = Prob.((A.0)`) by PROB_1:def 4,A2,A1; Prob.((A.0)`) = Prob.(([#] Sigma) \ A.0) by SUBSET_1:def 5; then A4: Partial_Product(Prob*(@Complement A)).0 = 1 - Prob.(A.0) by PROB_1:68,A3; 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 26; 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,FUNCT_1:22,A5; A8: for k being Element of NAT st J[k] holds J[k+1] proof let k be Element of 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 4,SUBSET_1:def 5; then A10: Prob.((@Complement A).(k+1)) = 1 - Prob.(A.(k+1)) by PROB_1:68; 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 FUNCT_1:22,A11,A10; 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 Element of NAT holds (JSum(Prob*A)).n > 0 proof let n be Element of NAT; A14: exp_R.(-(Prob*A).n) > 0 by SIN_COS:59; (JSum(Prob*A)).n = Sum( (-(Prob*A).n) rExpSeq) by Def1; hence thesis by SIN_COS:def 26,A14; end; then (Partial_Product JSum(Prob*A)).k>0 by SERIES_3:43; hence thesis by A12,XREAL_1:66; 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 13; dom(Prob*(@Complement A))=NAT by FUNCT_2:def 1; hence thesis by FUNCT_1:22,A16; end; then (Prob*(@Complement A)).(k+1)>=0; hence thesis by A9,XREAL_1:66; 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 26; 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 26; then A17: Partial_Product(Prob*(@Complement A)).(k+1) <= exp_R( (-(Prob.(A.(k+1)))) + (-Partial_Sums(Prob*A).k)) by SIN_COS:55; dom(Prob*A)=NAT by FUNCT_2:def 1; then (Prob*A).(k+1) = Prob.(A.(k+1)) by FUNCT_1:22; 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 SERIES_1:def 1,A17; hence thesis by Th3; end; for k being Element of NAT holds J[k] from NAT_1:sch 1(A7,A8); hence thesis; end; definition let n1,n2 be Element of NAT; func Special_Function(n1,n2) -> sequence of NAT means :Def2: for n being Element of NAT holds it.n = IFGT(n,n1,n+n2,n); existence proof deffunc U(Element of NAT) = IFGT(\$1,n1,\$1+n2,\$1); ex f being sequence of NAT st for n being Element of NAT holds f.n=U(n) from FUNCT_2:sch 4; hence thesis; end; uniqueness proof let s1,s2 be sequence of NAT; assume that A1: for n being Element of NAT holds s1.n=IFGT(n,n1,n+n2,n) and A2: for n being Element of 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 A1,A2; hence thesis; end; end; definition let k be Element of NAT; func Special_Function2(k) -> sequence of NAT means :Def3: for n being Element of NAT holds it.n = n+k; existence proof deffunc U(Element of NAT) = \$1+k; 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; thus thesis by A1; end; uniqueness proof let s1,s2 be sequence of NAT; assume that A2: for n being Element of NAT holds s1.n=n+k and A3: for n being Element of 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 Element of NAT; func Special_Function3(k) -> sequence of NAT means :Def4: for n being Element of NAT holds it.n = IFGT(n,k,0,1); existence proof deffunc U(Element of NAT) = IFGT(\$1,k,0,1); ex f being sequence of NAT st for n being Element of NAT holds f.n=U(n) from FUNCT_2:sch 4; hence thesis; end; uniqueness proof let s1,s2 be sequence of NAT; assume that A1: for n being Element of NAT holds s1.n=IFGT(n,k,0,1) and A2: for n being Element of 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 A1,A2; hence thesis; end; end; definition let n1,n2 be Element of NAT; func Special_Function4(n1,n2) -> sequence of NAT means :Def5: for n being Element of NAT holds it.n = IFGT(n,n1+1,n+n2,n); existence proof deffunc U(Element of NAT) = IFGT(\$1,n1+1,\$1+n2,\$1); ex f being sequence of NAT st for n being Element of NAT holds f.n=U(n) from FUNCT_2:sch 4; hence thesis; end; uniqueness proof let s1,s2 be sequence of NAT; assume that A1: for n being Element of NAT holds s1.n=IFGT(n,n1+1,n+n2,n) and A2: for n being Element of 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 A1,A2; hence thesis; end; end; registration let n1,n2 be Element of NAT; cluster Special_Function(n1,n2) -> one-to-one; coherence proof let x1,x2 be set; 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 A5: x1 <= n1 & x2 <= n1; IFGT(x2,n1,x2+n2,x2) = x2 & IFGT(x1,n1,x1+n2,x1) = x1 by A5,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; A8: IFGT(x1,n1,x1+n2,x1) = x1 by A6,XXREAL_0:def 11; A9: Special_Function(n1,n2).x1 = x1 by Def2,A8; 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 XREAL_1:33,A9,A7; end; hence thesis by A3; end; suppose A10: x2 <= n1 & x1 > n1; A11: Special_Function(n1,n2).x1 = IFGT(x1,n1,x1+n2,x1) by Def2; A12: Special_Function(n1,n2).x1=x1+n2 by A11,A10,XXREAL_0:def 11; A13: Special_Function(n1,n2).x2 = IFGT(x2,n1,x2+n2,x2) by Def2; A14: Special_Function(n1,n2).x2 = x2 by A13,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 XREAL_1:33,A14,A12; 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 set; 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; A22: 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; A23: Special_Function4(n1,n2).x2 = x2 & Special_Function4(n1,n2).x1 = x1+n2 by A22,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:8,XREAL_1:33; hence thesis by XXREAL_0:2,A21,A23; end; hence thesis by A18; end; suppose A24:x1<=n1+1 & x2>n1+1; 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,A24,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:8,XREAL_1:33; hence thesis by XXREAL_0:2,A24,A25; 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 Element of NAT; cluster Special_Function2(n) -> one-to-one; coherence proof let x1,x2 be set; 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; definition let X be set, s be Element of NAT, A be SetSequence of X; func Shift_Seq(A,s) -> SetSequence of X equals A^\s; correctness; end; definition let Omega be non empty set; let Sigma be SigmaField of Omega; let s be Element of NAT; let A be SetSequence of Sigma; func @Shift_Seq(A,s) -> SetSequence of Sigma equals Shift_Seq(A,s); coherence proof defpred P[set] means (Shift_Seq(A,s)).\$1 is Event of Sigma; A1: (Shift_Seq(A,s)).0=A.(0+s) by NAT_1:def 3; A2: P[0] by A1; A3: for k be Element of NAT st P[k] holds P[k+1] proof let k be Element of NAT; assume (Shift_Seq(A,s)).k is Event of Sigma; A.(s+(k+1)) is Event of Sigma; hence thesis by NAT_1:def 3; end; for k being Element of NAT holds P[k] from NAT_1:sch 1(A2,A3); hence thesis by PROB_1:57; end; 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*@Shift_Seq(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 @Shift_Seq(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*@Shift_Seq(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:22; 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,FUNCT_1:22,A3,A9; dom (Prob*A) = NAT by FUNCT_2:def 1; hence thesis by FUNCT_1:22,A11,A7,A8; end; A12: for k being Element of NAT st J[k] holds J[k+1] proof let k be Element of NAT; assume A13: J[k]; per cases; suppose A14: kn1 & C = A*e & B=C*Special_Function(n1,n2) holds (@Partial_Intersection B).n = (@Partial_Intersection C).n1 /\ (@Partial_Intersection @Shift_Seq(C,n1+n2+1)).(n-n1-1) proof let A,B,C be SetSequence of Sigma; let n1,n2,n be Element of NAT; let e be sequence of NAT; assume A44: n>n1; assume C = A*e; assume A45: B=C*Special_Function(n1,n2); reconsider B as SetSequence of Sigma; A46: (@Partial_Intersection B).n1 = (@Partial_Intersection C).n1 proof for x being set holds x in (@Partial_Intersection B).n1 iff x in (@Partial_Intersection C).n1 proof let x be set; hereby assume A47: x in (@Partial_Intersection B).n1; x in (@Partial_Intersection C).n1 proof A48: for knat being Nat st knat<=n1 holds x in C.knat proof let knat be Nat; assume A49: knat <= n1; reconsider knat as Element of NAT by ORDINAL1:def 13; A50: x in B.knat by A49,A47,PROB_3:29; A51: 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,A49,XXREAL_0:def 11; hence thesis by A51,FUNCT_1:22,A45,A50; end; reconsider n1 as Nat; thus thesis by A48,PROB_3:29; end; hence x in (@Partial_Intersection C).n1; end; assume A52: 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 A53: knat<=n1; reconsider knat as Element of NAT by ORDINAL1:def 13; A54: x in C.knat by A53,A52,PROB_3:29; A55: 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,A53,XXREAL_0:def 11; hence thesis by A55,FUNCT_1:22,A45,A54; end; hence thesis by PROB_3:29; end; hence x in (@Partial_Intersection B).n1; end; hence thesis by TARSKI:2; end; A56: 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=0 & (n-n1-1) is Element of NAT proof (n-n1) is Element of NAT by A44,NAT_1:21; hence thesis by A44,XREAL_1:52,NAT_1:20; 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 @Shift_Seq(C,n1+n2+1).knat by A60,A59,PROB_3:29; hence thesis by NAT_1:def 3; end; for qnat being Nat st n1=0 & n-n1-1 is Element of NAT proof n-n1 is Element of NAT by A44,NAT_1:21; hence thesis by A44,XREAL_1:52,NAT_1:20; end; x in (@Partial_Intersection @Shift_Seq(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:8; then n1+1-1<=qnat-1 by XREAL_1:11; then n1<=qnat-1 & qnat<(qnat+1) by NAT_1:13; then n1<=qnat-1 & qnat-1n1 & A is_all_independent_wrt Prob implies Prob.( (@Partial_Intersection @Complement A).n1 /\ (@Partial_Intersection @Shift_Seq(A,n1+n2+1)).(n-n1-1)) = (Partial_Product (Prob*@Complement A)).n1 * (Partial_Product (Prob*@Shift_Seq(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*@Shift_Seq(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[Element of NAT] means (Partial_Product(Prob*@Shift_Seq(A,k))).\$1 = (Partial_Product(Prob*B)).\$1; dom (Prob*(@Shift_Seq(A,k))) = NAT by FUNCT_2:def 1; then A5: (Prob*(@Shift_Seq(A,k))).0 = Prob.(@Shift_Seq(A,k).0) by FUNCT_1:22; (Prob*(@Shift_Seq(A,k))).0 = Prob.(A.(0+k)) by NAT_1:def 3,A5; then A6: Partial_Product(Prob*(@Shift_Seq(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 FUNCT_1:22,A8,A4; dom (Prob*B) = NAT by FUNCT_2:def 1; then A10: J[0] by FUNCT_1:22,A9,A7,A6; A11: for q being Element of NAT st J[q] holds J[q+1] proof let q be Element of NAT; assume A12: J[q]; A13: (Partial_Product(Prob*@Shift_Seq(A,k))).(q+1) = (Partial_Product(Prob*B)).q * (Prob*@Shift_Seq(A,k)).(q+1) by SERIES_3:def 1,A12; (Prob*@Shift_Seq(A,k)).(q+1) = (Prob*B).(q+1) proof dom (Prob*@Shift_Seq(A,k)) = NAT by FUNCT_2:def 1; then A14: (Prob*@Shift_Seq(A,k)).(q+1) = Prob.(@Shift_Seq(A,k).(q+1)) by FUNCT_1:22; dom (Prob*B) = NAT by FUNCT_2:def 1; then A15: (Prob*B).(q+1) = Prob.(B.(q+1)) by FUNCT_1:22; dom (A*Special_Function2(k)) = NAT by FUNCT_2:def 1; then A16: B.(q+1) = A.((Special_Function2(k)).(q+1)) by FUNCT_1:22,A4; (Special_Function2(k)).(q+1) = q+1+k & q+1+k = (q+1)+k by Def3; hence thesis by A16,A15,NAT_1:def 3,A14; end; hence thesis by A13,SERIES_3:def 1; end; for k being Element of NAT holds J[k] from NAT_1:sch 1(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 {} & e*Special_Function2(m1) is one-to-one & (for n being Element of NAT holds A.((e*(Special_Function2(m1))).n)=B.n) proof A30: for n being Element of NAT holds A.((e*(Special_Function2(m1))).n)=B.n proof let n be Element of NAT; 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:22; 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:22; 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 FUNCT_1:22,A32,A31; dom((A*e)*Special_Function2(m1)) = NAT by FUNCT_2:def 1; then A34: B.n = (A*(e*Special_Function2(m1))).n by FUNCT_1:22,A33,A28,A26; dom(A*(e*Special_Function2(m1))) = NAT by FUNCT_2:def 1; hence thesis by FUNCT_1:22,A34; end; thus thesis by A27,FUNCT_1:46,A30; end; Prob.((@Partial_Intersection B).m) = (Partial_Product(Prob*B)).m by A2,A29,Def8; hence thesis by A28,A3; end; A35: for q being Element of NAT holds Prob.((@Partial_Intersection (@Complement A)).n1 /\ (@Partial_Intersection @Shift_Seq(A,n1+n2+1)).q) = Partial_Product(Prob*(@Complement A)).n1 * Partial_Product(Prob*@Shift_Seq(A,n1+n2+1)).q proof let q be Element of NAT; defpred J[Element of NAT] means for e being sequence of NAT, q,n2 being Element of NAT, C being SetSequence of Sigma st e is one-to-one & C=A*e holds Prob.((@Partial_Intersection (@Complement C)).\$1 /\ (@Partial_Intersection @Shift_Seq(C,\$1+n2+1)).q) = Partial_Product(Prob*(@Complement C)).\$1 * Partial_Product(Prob*@Shift_Seq(C,\$1+n2+1)).q; A36: J[0] proof let e be sequence of NAT; let q,n2 be Element of 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 @Shift_Seq(C,0+n2+1)).q) = Prob.((@Complement C).0 /\ (@Partial_Intersection @Shift_Seq(C,0+n2+1)).q) by PROB_3:25; then Prob.((@Partial_Intersection (@Complement C)).0 /\ (@Partial_Intersection @Shift_Seq(C,0+n2+1)).q) = Prob.((C.0)` /\ (@Partial_Intersection @Shift_Seq(C,0+n2+1)).q) by PROB_1:def 4; then Prob.((@Partial_Intersection (@Complement C)).0 /\ (@Partial_Intersection @Shift_Seq(C,0+n2+1)).q) = Prob.((Omega \ C.0) /\ (@Partial_Intersection @Shift_Seq(C,0+n2+1)).q) by SUBSET_1:def 5; then A39: Prob.((@Partial_Intersection (@Complement C)).0 /\ (@Partial_Intersection @Shift_Seq(C,0+n2+1)).q) = Prob.( (Omega /\ (@Partial_Intersection @Shift_Seq(C,0+n2+1)).q) \ (C.0 /\ (@Partial_Intersection @Shift_Seq(C,0+n2+1)).q)) by XBOOLE_1:111; A40: Prob.((@Partial_Intersection (@Complement C)).0 /\ (@Partial_Intersection @Shift_Seq(C,0+n2+1)).q) = Prob.( (@Partial_Intersection @Shift_Seq(C,0+n2+1)).q \ (C.0 /\ (@Partial_Intersection @Shift_Seq(C,0+n2+1)).q)) by XBOOLE_1:28,A39; A41: Prob.((@Partial_Intersection (@Complement C)).0 /\ (@Partial_Intersection @Shift_Seq(C,0+n2+1)).q) = Prob.((@Partial_Intersection @Shift_Seq(C,0+n2+1)).q) - Prob.((C.0 /\ (@Partial_Intersection @Shift_Seq(C,0+n2+1)).q)) by XBOOLE_1:17,PROB_1:69,A40; consider m1 being Element of NAT such that A42: m1=0; consider m being Element of NAT such that A43: m=m1+1+q; consider m2 being Element of NAT such that A44: m2=n2; consider B being SetSequence of Omega such that A45: B=(C*Special_Function(m1,m2)); reconsider B as SetSequence of Sigma by A45; A46: m1{} by A63,FUNCT_1:46; then consider f being sequence of NAT such that A71: f=e*(Special_Function4(k,n2)) & f is one-to-one & dom f <>{}; A72: for q being set st q in NAT holds F.q = (A*f).q proof let q be set; assume q in NAT; then reconsider q as Element of NAT; dom(A*e) = NAT by FUNCT_2:def 1; then A73: (A*e).((Special_Function4(k,n2)).q) = A.(e.((Special_Function4(k,n2)).q)) by FUNCT_1:22; dom((A*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 FUNCT_1:22,A73; dom(e*(Special_Function4(k,n2))) = NAT by FUNCT_2:def 1; then A75: ((A*e)*(Special_Function4(k,n2))).q = A.((e*(Special_Function4(k,n2))).q) by FUNCT_1:22,A74; dom(A*f)=NAT by FUNCT_2:def 1; hence thesis by FUNCT_1:22,A71,A75,A64,A69; end; A76: Prob.((@Partial_Intersection (@Complement F)).k /\ (@Partial_Intersection @Shift_Seq(F,k+0+1)).(q+1)) = Partial_Product(Prob*(@Complement F)).k * Partial_Product(Prob*@Shift_Seq(F,k+0+1)).(q+1) by A71,A72,FUNCT_2:18,A62; A77: (@Partial_Intersection @Complement C).k = (@Partial_Intersection @Complement F).k proof A78: 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 A79: knat<=k+1 by NAT_1:13; reconsider knat as Element of NAT by ORDINAL1:def 13; dom (C*(Special_Function4(k,n2))) = NAT by FUNCT_2:def 1; then A80: (C*(Special_Function4(k,n2))).knat = C.((Special_Function4(k,n2)).knat) by FUNCT_1:22; (Special_Function4(k,n2)).knat = IFGT(knat,k+1,knat+n2,knat) & IFGT(knat,k+1,knat+n2,knat) = knat by Def5,A79,XXREAL_0:def 11; then (Complement F).knat = (C.knat)` by A69,A80,PROB_1:def 4; hence thesis by PROB_1:def 4; end; A81: for x being set 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 set; hereby assume A82: (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 A83: knat<=k; then x in (@Complement C).knat iff x in (@Complement F).knat by A78; hence thesis by A83,A82; end; end; assume A84: (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 A85: knat<=k; then x in (@Complement C).knat iff x in (@Complement F).knat by A78; hence thesis by A85,A84; end; end; for x being set holds (x in (@Partial_Intersection (@Complement C)).k iff x in (@Partial_Intersection (@Complement F)).k) proof let x be set; x in (@Partial_Intersection (@Complement C)).k iff for knat being Nat st knat<=k holds x in (@Complement C).knat by PROB_3:29; then x in (@Partial_Intersection (@Complement C)).k iff for knat being Nat st knat<=k holds x in (@Complement F).knat by A81; hence thesis by PROB_3:29; end; hence thesis by TARSKI:2; end; A86: (@Partial_Intersection @Shift_Seq(F,k+1)).(q+1) = C.(k+1) /\ (@Partial_Intersection @Shift_Seq(C,(k+1)+n2+1)).q proof A87: for x being set holds (for knat being Nat st knat<=q holds (x in (@Shift_Seq(F,k+1+1)).knat iff x in (@Shift_Seq(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 13; A88: 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:13,NAT_1:12; 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 A69,A88,FUNCT_1:22; then @Shift_Seq(F,k+1+1).knat = C.(knat+((k+1)+n2+1)) by NAT_1:def 3; hence thesis by NAT_1:def 3; end; A89: for x being set holds ( (for knat being Nat st knat<=q holds x in (@Shift_Seq(C,(k+1)+n2+1)).knat) iff (for knat being Nat st knat<=q holds x in (@Shift_Seq(F,k+1+1)).knat) ) proof let x be set; hereby assume A90: for knat being Nat st knat<=q holds x in (@Shift_Seq(C,(k+1)+n2+1)).knat; thus (for knat being Nat st knat<=q holds x in (@Shift_Seq(F,k+1+1)).knat) proof let knat be Nat; assume A91: knat<=q; then x in (@Shift_Seq(C,(k+1)+n2+1)).knat iff x in (@Shift_Seq(F,k+1+1)).knat by A87; hence thesis by A91,A90; end; end; assume A92: (for knat being Nat st knat<=q holds x in (@Shift_Seq(F,k+1+1)).knat); thus (for knat being Nat st knat<=q holds x in (@Shift_Seq(C,(k+1)+n2+1)).knat) proof let knat be Nat; assume A93: knat<=q; then x in (@Shift_Seq(C,(k+1)+n2+1)).knat iff x in (@Shift_Seq(F,k+1+1)).knat by A87; hence thesis by A93,A92; end; end; A94: for x being set holds (x in (@Partial_Intersection (@Shift_Seq(C,(k+1)+n2+1))).q iff x in (@Partial_Intersection (@Shift_Seq(F,k+1+1)) ).q) proof let x be set; x in (@Partial_Intersection (@Shift_Seq(C,(k+1)+n2+1)) ).q iff for knat being Nat st knat<=q holds x in (@Shift_Seq(C,(k+1)+n2+1)).knat by PROB_3:29; then x in (@Partial_Intersection (@Shift_Seq(C,(k+1)+n2+1)) ).q iff for knat being Nat st knat<=q holds x in (@Shift_Seq(F,k+1+1)).knat by A89; hence thesis by PROB_3:29; end; (@Partial_Intersection (@Shift_Seq(F,k+1+1))).q /\ C.(k+1) = (@Partial_Intersection (@Shift_Seq(F,k+1))).(q+1) proof defpred J[Element of NAT] means (@Partial_Intersection (@Shift_Seq(F,k+1+1))).\$1 /\ C.(k+1) = (@Partial_Intersection (@Shift_Seq(F,k+1))).(\$1+1); A95: J[0] proof (@Partial_Intersection (@Shift_Seq(F,k+1+1))).0 /\ C.(k+1) = ((@Shift_Seq(F,k+1+1))).0 /\ C.(k+1) by PROB_3:25; then (@Partial_Intersection (@Shift_Seq(F,k+1+1))).0 /\ C.(k+1) =F.(0+(k+1+1)) /\ C.(k+1) by NAT_1:def 3; then A96: (@Partial_Intersection (@Shift_Seq(F,k+1+1))).0 /\ C.(k+1) = (@Shift_Seq(F,k+1)).(0+1) /\ C.(k+1) by NAT_1:def 3; A97: 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 (@Shift_Seq(F,k+1+1))).0 /\ C.(k+1) = (@Shift_Seq(F,k+1)).(0+1) /\ F.(0+(k+1)) by A69,A97,FUNCT_1:22,A96; then (@Partial_Intersection (@Shift_Seq(F,k+1+1))).0 /\ C.(k+1) = (@Shift_Seq(F,k+1)).(0+1) /\ @Shift_Seq(F,k+1).0 by NAT_1:def 3; then (@Partial_Intersection (@Shift_Seq(F,k+1+1))).0 /\ C.(k+1) = (@Partial_Intersection @Shift_Seq(F,k+1)).0 /\ (@Shift_Seq(F,k+1)).(0+1) by PROB_3:25; hence thesis by PROB_3:25; end; A98: for q being Element of NAT st J[q] holds J[q+1] proof let q be Element of NAT; assume A99: J[q]; (@Partial_Intersection (@Shift_Seq(F,k+1+1))).(q+1) /\ C.(k+1) = (@Partial_Intersection (@Shift_Seq(F,k+1+1))).q /\ (@Shift_Seq(F,k+1+1)).(q+1) /\ C.(k+1) by PROB_3:25; then A100: ( (@Partial_Intersection (@Shift_Seq(F,k+1+1))).(q+1) /\ C.(k+1) ) = (@Partial_Intersection (@Shift_Seq(F,k+1))).(q+1) /\ (@Shift_Seq(F,k+1+1)).(q+1) by XBOOLE_1:16,A99; (@Shift_Seq(F,k+1+1)).(q+1) = (@Shift_Seq(F,k+1)).((q+1)+1) proof (@Shift_Seq(F,k+1+1)).(q+1) = F.((q+1)+(k+1+1)) by NAT_1:def 3; then (@Shift_Seq(F,k+1+1)).(q+1) = F.(((q+1)+1)+(k+1)); hence thesis by NAT_1:def 3; end; hence thesis by A100,PROB_3:25; end; for k being Element of NAT holds J[k] from NAT_1:sch 1(A95,A98); hence thesis; end; hence thesis by A94,TARSKI:2; end; A101: Partial_Product(Prob*@Shift_Seq(F,k+1)).(q+1) = (Prob*C).(k+1) * Partial_Product(Prob*@Shift_Seq(C,(k+1)+n2+1)).q proof defpred J[Element of NAT] means Partial_Product(Prob*@Shift_Seq(F,k+1)).(\$1+1) = (Prob*C).(k+1) * Partial_Product(Prob*@Shift_Seq(C,(k+1)+n2+1)).\$1; A102: J[0] proof A103: @Shift_Seq(F,k+1).(0+1) = (C*Special_Function4(k,n2)).(k+1+1) by NAT_1:def 3,A69; A104: 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 @Shift_Seq(F,k+1).(0+1) = C.(0+((k+1)+n2+1)) by A104,FUNCT_1:22,A103; then A105: Prob.(@Shift_Seq(F,k+1).(0+1)) = Prob.((@Shift_Seq(C,(k+1)+n2+1)).0) by NAT_1:def 3; dom(Prob*(@Shift_Seq(F,k+1)))=NAT & dom(Prob*(@Shift_Seq(C,(k+1)+n2+1)))=NAT by FUNCT_2:def 1; then (Prob*(@Shift_Seq(F,k+1))).(0+1) = Prob.((@Shift_Seq(C,(k+1)+n2+1)).0) & Prob.(@Shift_Seq(F,k+1).(0+1)) = (Prob*(@Shift_Seq(C,(k+1)+n2+1))).0 & Prob.(@Shift_Seq(F,k+1).(0+1)) = Prob.((@Shift_Seq(C,(k+1)+n2+1)).0) by FUNCT_1:22,A105; then A106: (Partial_Product (Prob*@Shift_Seq(F,k+1))).0 * (Prob*(@Shift_Seq(F,k+1))).(0+1) = (Prob*@Shift_Seq(F,k+1)).0 * (Prob*(@Shift_Seq(C,(k+1)+n2+1))).0 by SERIES_3:def 1; (Prob*@Shift_Seq(F,k+1)).0 = (Prob*C).(k+1) proof A107: (@Shift_Seq(F,k+1)).0 = F.(0+(k+1)) by NAT_1:def 3; A108: dom (C*(Special_Function4(k,n2))) = NAT by FUNCT_2:def 1; A109: F.(k+1) = C.((Special_Function4(k,n2)).(k+1)) by A69,A108,FUNCT_1:22; A110: (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 A111: Prob.((@Shift_Seq(F,k+1)).0) = (Prob*C).(k+1) by FUNCT_1:22,A110,A109,A107; dom(Prob*(@Shift_Seq(F,k+1))) = NAT by FUNCT_2:def 1; hence thesis by FUNCT_1:22,A111; end; then (Partial_Product (Prob*@Shift_Seq(F,k+1))).(0+1) = (Prob*C).(k+1) * (Prob*(@Shift_Seq(C,(k+1)+n2+1))).0 by A106,SERIES_3:def 1; hence thesis by SERIES_3:def 1; end; A112: for q being Element of NAT st J[q] holds J[q+1] proof let q be Element of NAT; assume A113:J[q]; A114: (Prob*@Shift_Seq(F,k+1)).((q+1)+1) = (Prob*@Shift_Seq(C,(k+1)+n2+1)).(q+1) proof A115: @Shift_Seq(F,k+1).((q+1)+1) = (C*Special_Function4(k,n2)).(((q+1)+1)+(k+1)) by NAT_1:def 3,A69; A116: 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:33; 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 @Shift_Seq(F,k+1).((q+1)+1) = C.((q+1)+((k+1)+n2+1)) by A116,FUNCT_1:22,A115; then A117: Prob.(@Shift_Seq(F,k+1).((q+1)+1)) = Prob.((@Shift_Seq(C,(k+1)+n2+1)).(q+1)) by NAT_1:def 3; dom(Prob*(@Shift_Seq(F,k+1)))=NAT & dom(Prob*(@Shift_Seq(C,(k+1)+n2+1)))=NAT by FUNCT_2:def 1; then (Prob*(@Shift_Seq(F,k+1))).((q+1)+1) = Prob.((@Shift_Seq(C,(k+1)+n2+1)).(q+1)) & Prob.(@Shift_Seq(F,k+1).((q+1)+1)) = (Prob*(@Shift_Seq(C,(k+1)+n2+1))).(q+1) & Prob.(@Shift_Seq(F,k+1).((q+1)+1)) = Prob.((@Shift_Seq(C,(k+1)+n2+1)).(q+1)) by FUNCT_1:22,A117; hence thesis; end; Partial_Product(Prob*@Shift_Seq(F,k+1)).((q+1)+1) = ((Prob*C).(k+1) * Partial_Product(Prob*@Shift_Seq(C,(k+1)+n2+1)).q) * (Prob*@Shift_Seq(C,(k+1)+n2+1)).(q+1) by SERIES_3:def 1,A113,A114; then Partial_Product(Prob*@Shift_Seq(F,k+1)).((q+1)+1) = (Prob*C).(k+1) * ( Partial_Product(Prob*@Shift_Seq(C,(k+1)+n2+1)).q * (Prob*@Shift_Seq(C,(k+1)+n2+1)).(q+1) ); hence thesis by SERIES_3:def 1; end; for k being Element of NAT holds J[k] from NAT_1:sch 1(A102,A112); hence thesis; end; defpred J[Element of 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 A118: (C*Special_Function4(k,n2)).0 = C.((Special_Function4(k,n2)).0) by FUNCT_1:22; A119: IFGT(0,k+1,0+n2,0) = 0 by XXREAL_0:def 11; then (F.0)` = (C.0)` by Def5,A118,A69; then (@Complement F).0 = (C.0)` by PROB_1:def 4; then Prob.((@Complement F).0) = Prob.((@Complement C).0) & dom(Prob*(@Complement F)) = NAT & dom(Prob*(@Complement C)) = NAT by PROB_1:def 4,FUNCT_2:def 1; 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:22; then A120: Partial_Product(Prob*(@Complement F)).0 = (Prob*(@Complement C)).0 & F.0 = C.0 by SERIES_3:def 1,A119,Def5,A118,A69; A121: J[0] by A120,SERIES_3:def 1; A122: for q being Element of NAT st J[q] holds J[q+1] proof let q be Element of NAT; assume A123:J[q]; A124: (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 A125: (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 A125; 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 A126: (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 4; then A127: Partial_Product(Prob*(@Complement F)).q * Prob.((@Complement F).(q+1)) = Partial_Product(Prob*(@Complement C)).q * Prob.((@Complement C).(q+1)) by PROB_1:def 4,A126,A124,A123; 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:22; then Partial_Product(Prob*(@Complement F)).(q+1) = Partial_Product(Prob*(@Complement C)).q * (Prob*@Complement C).(q+1) by A127,SERIES_3:def 1; hence thesis by SERIES_3:def 1; end; hence thesis; end; A128: for k being Element of NAT holds J[k] from NAT_1:sch 1(A121,A122); 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 A129: q<=k+1 by NAT_1:13; A130: 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,A129,XXREAL_0:def 11; hence thesis by A130,FUNCT_1:22,A69; end; then Prob.( (@Partial_Intersection (@Complement C)).k /\ (C.(k+1) /\ (@Partial_Intersection @Shift_Seq(C,(k+1)+n2+1)).q) ) = Partial_Product(Prob*(@Complement C)).k * ( (Prob*C).(k+1) * Partial_Product(Prob*@Shift_Seq(C,(k+1)+n2+1)).q) by A128,A101,A86,A77,A76; hence thesis by XBOOLE_1:16; end; hence thesis by A67,XBOOLE_1:17,PROB_1:69,A66; 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 5; then Prob.(C.(k+1))=Prob.([#]Sigma \ (C.(k+1))`) & (C.(k+1))`is Event of Sigma by PROB_1:50; then A131: Prob.(C.(k+1))=1-Prob.((C.(k+1))`) by PROB_1:68; dom (Prob*C) = NAT by FUNCT_2:def 1; then A132: (Prob*C).(k+1) = 1-Prob.((C.(k+1))`) by FUNCT_1:22,A131; dom (Prob*(@Complement C)) = NAT by FUNCT_2:def 1; then (Prob*(@Complement C)).(k+1) = Prob.((@Complement C).(k+1)) by FUNCT_1:22; hence thesis by PROB_1:def 4,A132; end; then Prob.((@Partial_Intersection (@Complement C)).(k+1) /\ (@Partial_Intersection @Shift_Seq(C,(k+1)+n2+1)).q) = (Prob*(@Complement C)).(k+1) * Partial_Product(Prob*(@Complement C)).k * Partial_Product(Prob*@Shift_Seq(C,(k+1)+n2+1)).q by A68; hence thesis by SERIES_3:def 1; end; A133: for k being Element of NAT holds J[k] from NAT_1:sch 1(A36,A61); ex e being sequence of NAT st A*e=A & e is one-to-one & dom(e)<>{} proof set e=Special_Function2(0); A134: dom(e)<>{}; A is sequence of bool Omega & A*e is sequence of bool Omega & for n being set st n in NAT holds (A*e).n = A.n proof A135: for n being set st n in NAT holds (A*e).n = A.n & A.(e.n) = A.n proof let n be set; assume n in NAT; then reconsider n as Element of NAT; A136: e.n = n+0 by Def3; dom(A*e) = NAT by FUNCT_2:def 1; hence thesis by FUNCT_1:22,A136; end; thus thesis by A135; end; hence thesis by FUNCT_2:18,A134; end; hence thesis by A133; 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:11; 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 set holds (x in (@Partial_Intersection @Complement A).n iff x in ((@Partial_Union A).n)`) proof let x be set; 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:29; reconsider knat as Element of NAT by ORDINAL1:def 13; (@Complement A).knat=(A.knat)` by PROB_1:def 4; then (@Complement A).knat=Omega \ A.knat by SUBSET_1:def 5; hence thesis by A2,XBOOLE_0:def 5; end; then A3: not x in (@Partial_Union A).n by PROB_3:30; 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 5; end; assume A4: x in ((@Partial_Union A).n)`; x in Omega \ (@Partial_Union A).n by A4,SUBSET_1:def 5; 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:30; then A6: x in Omega \ A.knat by XBOOLE_0:def 5; reconsider knat as Element of NAT by ORDINAL1:def 13; x in (A.knat)` by A6,SUBSET_1:def 5; hence thesis by PROB_1:def 4; end; hence x in (@Partial_Intersection (@Complement A)).n by PROB_3:29; 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 5; hence thesis by PROB_1:68,A1; end; definition let X be set, A be SetSequence of X; func Union_Shift_Seq A -> SetSequence of X means :Def9: for n being Element of NAT holds it.n = Union Shift_Seq(A,n); existence proof for X being set, A being SetSequence of X holds ex S being SetSequence of X st (for n being Element of NAT holds S.n = Union Shift_Seq(A,n) ) proof let X be set, A be SetSequence of X; ex J being SetSequence of X st J.0 = Union Shift_Seq(A,0) & for n being Element of NAT holds J.(n+1) = Union Shift_Seq(A,(n+1)) proof defpred P[set,set,set] means for x,y being Subset of X, k being Element of NAT holds (k = \$1 & x = \$2 & y = \$3 implies y = Union Shift_Seq(A,(k+1)) ); A1: for n being Element of NAT for x being Subset of X ex y being Subset of X st P[n,x,y] proof let n be Element of NAT; let x be Subset of X; take y = Union Shift_Seq(A,(n+1)); thus thesis; end; consider J being SetSequence of X such that A2: J.0 = Union Shift_Seq(A,0) and A3: for n being Element of NAT holds P[n,J.n,J.(n+1)] from RECDEF_1:sch 2(A1); take J; thus J.0 = Union Shift_Seq(A,0) by A2; let n be Element of NAT; P[n,J.n,J.(n+1)] by A3; hence thesis; end; then consider J being SetSequence of X such that A4: J.0 = Union Shift_Seq(A,0) & for n being Element of NAT holds J.(n+1) = Union Shift_Seq(A,(n+1)); A5: ( J.0 = Union Shift_Seq(A,0) & for n being Element of NAT holds J.(n+1) = Union Shift_Seq(A,(n+1)) ) implies ( for n being Element of NAT holds J.n = Union Shift_Seq(A,n) ) proof assume A6: J.0 = Union Shift_Seq(A,0) & for n being Element of NAT holds J.(n+1) = Union Shift_Seq(A,(n+1)); let n be Nat; per cases by NAT_1:6; suppose n=0; hence thesis by A6; end; suppose ex q being Nat st n=q+1; then consider q being Nat such that A7: n=q+1; reconsider q as Element of NAT by ORDINAL1:def 13; J.(q+1)=Union Shift_Seq(A,(q+1)) by A6; hence thesis by A7; end; end; take J; thus thesis by A4,A5; end; hence thesis; end; uniqueness proof let J1,J2 be SetSequence of X such that A8: for n being Element of NAT holds J1.n=Union Shift_Seq(A,n) and A9: for n being Element of NAT holds J2.n=Union Shift_Seq(A,n); for n being Element of NAT holds J1.n=J2.n proof let n being Element of NAT; J1.n=Union Shift_Seq(A,n) by A8; hence thesis by A9; end; then for n being set holds n in NAT implies J1.n=J2.n; hence thesis by FUNCT_2:18; end; end; definition let Omega be non empty set, Sigma be SigmaField of Omega, A be SetSequence of Sigma; func @Union_Shift_Seq A -> SetSequence of Sigma equals Union_Shift_Seq A; coherence proof defpred P[set] means (Union_Shift_Seq A).\$1 is Event of Sigma; (Union_Shift_Seq A).0 = Union @Shift_Seq(A,0) by Def9; then A1: P[0] by PROB_1:46; A2: for k be Element of NAT st P[k] holds P[k+1] proof let k be Element of NAT; assume (Union_Shift_Seq A).k is Event of Sigma; Union @Shift_Seq(A,(k+1)) in Sigma by PROB_1:46; hence thesis by Def9; end; for k being Element of NAT holds P[k] from NAT_1:sch 1(A1,A2); hence thesis by PROB_1:57; 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 @Intersection @Union_Shift_Seq A; correctness; end; definition let X be set, A be SetSequence of X; func Intersect_Shift_Seq A -> SetSequence of X means :Def12: for n being Element of NAT holds it.n = Intersection Shift_Seq(A,n); existence proof for X being set, A being SetSequence of X holds ex S being SetSequence of X st (for n being Element of NAT holds S.n = Intersection Shift_Seq(A,n) ) proof let X be set, A be SetSequence of X; A1: ex J being SetSequence of X st J.0 = Intersection Shift_Seq(A,0) & for n being Element of NAT holds J.(n+1) = Intersection Shift_Seq(A,(n+1)) proof defpred P[set,set,set] means for x,y being Subset of X, k being Element of NAT holds (k = \$1 & x = \$2 & y = \$3 implies y = Intersection Shift_Seq(A,(k+1)) ); A2: for n being Element of NAT for x being Subset of X ex y being Subset of X st P[n,x,y] proof let n be Element of NAT; let x be Subset of X; take y = Intersection Shift_Seq(A,(n+1)); thus thesis; end; consider J being SetSequence of X such that A3: J.0 = Intersection Shift_Seq(A,0) and A4: for n being Element of NAT holds P[n,J.n,J.(n+1)] from RECDEF_1:sch 2(A2); take J; thus J.0 = Intersection Shift_Seq(A,0) by A3; let n be Element of NAT; P[n,J.n,J.(n+1)] by A4; hence thesis; end; consider J being SetSequence of X such that A5: J.0 = Intersection Shift_Seq(A,0) & for n being Element of NAT holds J.(n+1) = Intersection Shift_Seq(A,(n+1)) by A1; A6: ( J.0 = Intersection Shift_Seq(A,0) & for n being Element of NAT holds J.(n+1) = Intersection Shift_Seq(A,(n+1)) ) implies ( for n being Element of NAT holds J.n = Intersection Shift_Seq(A,n) ) proof assume A7: J.0 = Intersection Shift_Seq(A,0) & for n being Element of NAT holds J.(n+1) = Intersection Shift_Seq(A,(n+1)); let n be Nat; per cases by NAT_1:6; suppose n=0; hence thesis by A7; end; suppose ex q being Nat st n=q+1; then consider q being Nat such that A8: n=q+1; reconsider q as Element of NAT by ORDINAL1:def 13; J.(q+1)=Intersection Shift_Seq(A,(q+1)) by A7; hence thesis by A8; end; end; take J; thus thesis by A5,A6; end; hence thesis; end; uniqueness proof let J1,J2 be SetSequence of X such that A9: for n being Element of NAT holds J1.n = Intersection Shift_Seq(A,n) and A10: for n being Element of NAT holds J2.n = Intersection Shift_Seq(A,n); for n being Element of NAT holds J1.n=J2.n proof let n being Element of NAT; J1.n=Intersection Shift_Seq(A,n) by A9; hence thesis by A10; end; then for n being set holds n in NAT implies J1.n=J2.n; hence thesis by FUNCT_2:18; end; end; definition let Omega be non empty set, Sigma be SigmaField of Omega, A be SetSequence of Sigma; func @Intersect_Shift_Seq A -> SetSequence of Sigma equals Intersect_Shift_Seq A; coherence proof defpred P[set] means (Intersect_Shift_Seq A).\$1 is Event of Sigma; for n being Element of NAT holds (Complement @Shift_Seq(A,0)).n is Event of Sigma proof let n be Element of NAT; (@Shift_Seq(A,0).n)` is Event of Sigma by PROB_1:50; hence thesis by PROB_1:def 4; end; then A1: (Complement @Shift_Seq(A,0)) is SetSequence of Sigma by PROB_1:57; A2: Union Complement @Shift_Seq(A,0) is Event of Sigma by A1,PROB_1:58; (Intersect_Shift_Seq A).0 = Intersection @Shift_Seq(A,0) by Def12; then A3: P[0] by A2,PROB_1:50; A4: for k be Element of NAT st P[k] holds P[k+1] proof let k be Element of NAT; assume (Intersect_Shift_Seq A).k is Event of Sigma; for n being Element of NAT holds (Complement @Shift_Seq(A,(k+1))).n is Event of Sigma proof let n be Element of NAT; (@Shift_Seq(A,(k+1)).n)` is Event of Sigma by PROB_1:50; hence thesis by PROB_1:def 4; end; then A5: (Complement @Shift_Seq(A,(k+1))) is SetSequence of Sigma by PROB_1:57; A6: Union Complement @Shift_Seq(A,(k+1)) is Event of Sigma by A5,PROB_1:58; (Intersect_Shift_Seq A).(k+1) = Intersection @Shift_Seq(A,(k+1)) by Def12; hence thesis by A6,PROB_1:50; end; for k being Element of NAT holds P[k] from NAT_1:sch 1(A3,A4); hence thesis by PROB_1:57; 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 Union @Intersect_Shift_Seq A; correctness by PROB_1:58; end; theorem Th9: (@Intersect_Shift_Seq @Complement A).n = ((@Union_Shift_Seq A).n)` proof for x being set holds (x in (@Intersect_Shift_Seq @Complement A).n iff x in ((@Union_Shift_Seq A).n)`) proof let x be set; hereby assume A1: x in (@Intersect_Shift_Seq @Complement A).n; then A2: x in Intersection Shift_Seq(@Complement A,n) by Def12; A3: for k being Element of NAT holds not x in @Shift_Seq( A,n).k proof let k be Element of NAT; x in ((@Complement A)^\n).k by A2,PROB_1:29; then x in (@Complement A).(n+k) by NAT_1:def 3; then A4: x in (A.(n+k))` by PROB_1:def 4; x in Omega \ A.(n+k) by SUBSET_1:def 5,A4; then x in Omega & not x in A.(n+k) by XBOOLE_0:def 5; hence thesis by NAT_1:def 3; end; A5: not x in Union @Shift_Seq(A,n) by A3,PROB_1:25; A6: not x in (@Union_Shift_Seq A).n by Def9,A5; A7: x in Omega \ (@Union_Shift_Seq A).n by A1,A6,XBOOLE_0:def 5; thus x in ((@Union_Shift_Seq A).n)` by SUBSET_1:def 5,A7; end; assume A8: x in ((@Union_Shift_Seq A).n)`; A9: x in ((@Union_Shift_Seq A).n)` iff x in Omega \ (@Union_Shift_Seq A).n by SUBSET_1:def 5; A10: x in (@Union_Shift_Seq A).n iff x in Union @Shift_Seq(A,n) by Def9; A11: for k being Element of NAT holds x in @Shift_Seq(@Complement A,n).k proof let k be Element of NAT; A12: not x in @Shift_Seq(A,n).k by A10,A8,A9,XBOOLE_0:def 5,PROB_1:25; A13: not x in A.(n+k) by NAT_1:def 3,A12; A14: x in Omega \ A.(n+k) by A8,A13,XBOOLE_0:def 5; x in (A.(n+k))` iff x in (@Complement A).(n+k) by PROB_1:def 4; hence thesis by A14,SUBSET_1:def 5,NAT_1:def 3; end; x in Intersection @Shift_Seq(@Complement A,n) by A11,PROB_1:29; hence x in (@Intersect_Shift_Seq @Complement A).n by Def12; end; hence thesis by TARSKI:2; 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[Element of 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:22; A3: Partial_Product(Prob*(@Complement A)).0 = (Prob*(@Complement A)).0 by SERIES_3:def 1; A4: J[0] by PROB_3:25,A2,A3; A5: for k being Element of NAT st J[k] holds J[k+1] proof let k be Element of 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 4; 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 5; 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; A9: 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 XBOOLE_1:17,PROB_1:69; 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:25,A9; for A being SetSequence of Sigma holds for k being Element of 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 Element of NAT; assume that A11: A is_all_independent_wrt Prob; consider n being Element of NAT such that A12: n=k+1; consider n1 being Element of NAT such that A13: n1=k; n1 Real_Sequence means :Def15: for n being Element of NAT holds it.n = Sum( Prob*@Shift_Seq(A,n) ); existence proof deffunc J(Element of NAT) = Sum( Prob*@Shift_Seq(A,\$1) ); 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 knat be Nat; thus thesis by A1; end; uniqueness proof let J1,J2 be Real_Sequence; assume A2: for n being Element of NAT holds J1.n=Sum( Prob*@Shift_Seq(A,n) ); assume A3: for n being Element of NAT holds J2.n=Sum( Prob*@Shift_Seq(A,n) ); let n be Element of NAT; J1.n=Sum( Prob*@Shift_Seq(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; A2: (Prob*A) is summable by A1,SERIES_1:def 2; A3: for n being Element of NAT holds 0<=(Prob*@Partial_Intersection @Union_Shift_Seq A).n proof let n be Element of NAT; A4: dom(Prob*@Partial_Intersection @Union_Shift_Seq A)=NAT by FUNCT_2:def 1; (Prob*@Partial_Intersection @Union_Shift_Seq A).n =Prob.((@Partial_Intersection @Union_Shift_Seq A).n) by A4,FUNCT_1:22; hence thesis by PROB_1:def 13; end; A5: Intersection @Partial_Intersection @Union_Shift_Seq A= Intersection @Union_Shift_Seq A by PROB_3:33; A6: @Partial_Intersection @Union_Shift_Seq A is non-ascending by PROB_3:31; A7: lim(Prob*@Partial_Intersection @Union_Shift_Seq A) = Prob.Intersection @Partial_Intersection @Union_Shift_Seq A & Prob*@Partial_Intersection @Union_Shift_Seq A is convergent by A6,PROB_1:def 13; A8: for A being SetSequence of Sigma holds for n,s being Element of NAT holds (Prob*(@Partial_Union @Shift_Seq(A,s))).n <= (Partial_Sums(Prob*@Shift_Seq(A,s))).n proof let A be SetSequence of Sigma; let n,s be Element of NAT; defpred P[set] means (Prob*(@Partial_Union @Shift_Seq(A,s))).\$1 <= Partial_Sums(Prob*@Shift_Seq(A,s)).\$1; A9: @Partial_Union @Shift_Seq(A,s) =Partial_Union @Shift_Seq(A,s) by PROB_3:def 6; A10: Partial_Sums(Prob*@Shift_Seq(A,s)).0 = (Prob*@Shift_Seq(A,s)).0 by SERIES_1:def 1; A11: dom(Prob*@Shift_Seq(A,s))=NAT by FUNCT_2:def 1; A12: (Prob*@Shift_Seq(A,s)).0=Prob.(@Shift_Seq(A,s).0) by A11,FUNCT_1:22; A13: Prob.((@Partial_Union @Shift_Seq(A,s)).0)= Prob.(@Shift_Seq(A,s).0) by PROB_3:def 2,A9; A14: dom(Prob*(@Partial_Union @Shift_Seq(A,s)))=NAT by FUNCT_2:def 1; A15: P[0] by A14,FUNCT_1:22,A13,A12,A10; A16: for k being Element of NAT st P[k] holds P[k+1] proof let k be Element of NAT; assume A17: (Prob*(@Partial_Union @Shift_Seq(A,s))).k <= Partial_Sums(Prob*@Shift_Seq(A,s)).k; A18: dom(Prob*(@Partial_Union @Shift_Seq(A,s)))= NAT by FUNCT_2:def 1; A19: @Partial_Union @Shift_Seq(A,s) = Partial_Union @Shift_Seq(A,s) by PROB_3:def 6; A20: Prob.((@Partial_Union @Shift_Seq(A,s)).k \/ @Shift_Seq(A,s).(k+1)) <= Prob.((@Partial_Union @Shift_Seq(A,s)).k) + Prob.(@Shift_Seq(A,s).(k+1)) by PROB_1:75; dom(Prob*@Shift_Seq(A,s))=NAT by FUNCT_2:def 1; then A21: (Prob*@Shift_Seq(A,s)).(k+1) =Prob.(@Shift_Seq(A,s).(k+1)) by FUNCT_1:22; A22: Prob.((@Partial_Union @Shift_Seq(A,s)).(k+1)) <= Prob.((@Partial_Union @Shift_Seq(A,s)).k) + (Prob*@Shift_Seq(A,s)).(k+1) implies Prob.((@Partial_Union @Shift_Seq(A,s)).(k+1)) - Prob.((@Partial_Union @Shift_Seq(A,s)).k) <= (Prob*@Shift_Seq(A,s)).(k+1) by XREAL_1:22; A23: (Prob.((@Partial_Union @Shift_Seq(A,s)).(k+1)) - (Prob*@Shift_Seq(A,s)).(k+1)) <= Prob.((@Partial_Union @Shift_Seq(A,s)).k) & Prob.((@Partial_Union @Shift_Seq(A,s)).k) <= Partial_Sums(Prob*@Shift_Seq(A,s)).k implies (Prob.((@Partial_Union @Shift_Seq(A,s)).(k+1)) - (Prob*@Shift_Seq(A,s)).(k+1)) <= Partial_Sums(Prob*@Shift_Seq(A,s)).k by XXREAL_0:2; A24: Prob.((@Partial_Union @Shift_Seq(A,s)).(k+1)) - (Prob*@Shift_Seq(A,s)).(k+1) <= Partial_Sums(Prob*@Shift_Seq(A,s)).k implies Prob.((@Partial_Union @Shift_Seq(A,s)).(k+1)) <= Partial_Sums(Prob*@Shift_Seq(A,s)).k + (Prob*@Shift_Seq(A,s)).(k+1) by XREAL_1:22; A25: Prob.((@Partial_Union @Shift_Seq(A,s)).(k+1)) <= Partial_Sums(Prob*@Shift_Seq(A,s)).(k+1) by PROB_3:def 2,A19,A20,A21,A22,XREAL_1:14,A18, FUNCT_1:22,A17,A23,A24,SERIES_1:def 1; dom(Prob*(@Partial_Union @Shift_Seq(A,s)))=NAT by FUNCT_2:def 1; hence thesis by FUNCT_1:22,A25; end; for k being Element of NAT holds P[k] from NAT_1:sch 1(A15,A16); hence thesis; end; A26: for k being Element of NAT holds Partial_Sums( (Prob*A) ^\k ) is convergent proof let k be Element of NAT; (Prob*A) ^\ k is summable by A2,SERIES_1:15; hence thesis by SERIES_1:def 2; end; A27: 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*@Shift_Seq(A,n)).k=( (Prob*A)^\n ).k proof let k be Element of NAT; dom(Prob*@Shift_Seq(A,n))=NAT by FUNCT_2:def 1; then A28: (Prob*@Shift_Seq(A,n)).k =Prob.((@Shift_Seq(A,n)).k) by FUNCT_1:22; dom(Prob*A)=NAT by FUNCT_2:def 1; then A29: Prob.(A.(n+k))=(Prob*A).(n+k) by FUNCT_1:22; (Prob*A).(k+n)=((Prob*A)^\n).k by NAT_1:def 3; hence thesis by A28,NAT_1:def 3,A29; end; hence thesis by FUNCT_2:113; end; A30: for n being Element of NAT holds Partial_Sums( Prob*@Shift_Seq(A,n) ) is convergent proof let n be Element of NAT; Partial_Sums( Prob*@Shift_Seq(A,n) )= Partial_Sums( (Prob*A)^\n ) by A27; hence thesis by A26; end; A31: for n being Element of NAT holds lim (Prob * @Partial_Union @Shift_Seq(A,n)) <= lim(Partial_Sums(Prob*@Shift_Seq(A,n))) proof let n be Element of NAT; A32: for k being Element of NAT holds (Prob*(@Partial_Union @Shift_Seq(A,n))).k <= (Partial_Sums(Prob*@Shift_Seq(A,n))).k by A8; A33: Prob*@Partial_Union @Shift_Seq(A,n) is convergent by PROB_3:46; Partial_Sums( Prob*@Shift_Seq(A,n) ) is convergent by A30; hence thesis by A33,A32,SEQ_2:32; end; A34: for n being Element of NAT holds Prob.Union @Shift_Seq(A,n) <= lim(Partial_Sums(Prob*@Shift_Seq(A,n))) proof let n be Element of NAT; lim (Prob * @Partial_Union @Shift_Seq(A,n)) <= lim(Partial_Sums(Prob*@Shift_Seq(A,n))) by A31; hence thesis by PROB_3:46; end; A35: for n being Element of NAT holds Prob.Union @Shift_Seq(A,n)<= Sum(Prob*@Shift_Seq(A,n)) proof let n be Element of NAT; lim(Partial_Sums(Prob*@Shift_Seq(A,n)))= Sum(Prob*@Shift_Seq(A,n)) by SERIES_1:def 3; hence thesis by A34; end; A36: for n being Element of NAT holds (Prob*(@Union_Shift_Seq A)).n <=Sum_Shift_Seq(Prob,A).n proof let n be Element of NAT; A37: dom(Prob*(@Union_Shift_Seq A))=NAT by FUNCT_2:def 1; A38: (Prob*(@Union_Shift_Seq A)).n= Prob.((@Union_Shift_Seq A).n) by A37,FUNCT_1:22; A39: Prob.Union @Shift_Seq(A,n)<= Sum(Prob*@Shift_Seq(A,n)) by A35; Sum(Prob*@Shift_Seq(A,n))=Sum_Shift_Seq(Prob,A).n by Def15; hence thesis by Def9,A38,A39; end; A40: 0<=lim(Prob*@Partial_Intersection @Union_Shift_Seq A) by A7,A3,SEQ_2:31; A41: Sum_Shift_Seq(Prob,A) is convergent implies lim(Prob*@Partial_Intersection @Union_Shift_Seq A) <= lim(Sum_Shift_Seq(Prob,A)) proof assume A42: Sum_Shift_Seq(Prob,A) is convergent; A43:for n being Element of NAT holds (Prob*(@Partial_Intersection @Union_Shift_Seq A)).n <= (Prob*(@Union_Shift_Seq A)).n proof let n be Element of NAT; A44: Prob.((@Partial_Intersection @Union_Shift_Seq A).n) <= Prob.((@Union_Shift_Seq A).n) by PROB_3:27,PROB_1:70; A45: dom(Prob*(@Partial_Intersection @Union_Shift_Seq A))=NAT by FUNCT_2:def 1; A46: dom(Prob*(@Union_Shift_Seq A))=NAT by FUNCT_2:def 1; (Prob*(@Union_Shift_Seq A)).n= Prob.((@Union_Shift_Seq A).n) by A46,FUNCT_1:22; hence thesis by A45,FUNCT_1:22,A44; end; lim(Prob*@Partial_Intersection @Union_Shift_Seq A) <= lim(Sum_Shift_Seq(Prob,A)) proof A47: for n being Element of NAT holds (Prob*@Partial_Intersection @Union_Shift_Seq A).n <= Sum_Shift_Seq(Prob,A).n proof let n be Element of NAT; A48: (Prob*@Partial_Intersection @Union_Shift_Seq A).n <= (Prob*(@Union_Shift_Seq A)).n by A43; A49: (Prob*(@Union_Shift_Seq A)).n <= Sum_Shift_Seq(Prob,A).n by A36; thus thesis by A48,A49,XXREAL_0:2; end; thus thesis by A7,A42,A47,SEQ_2:32; end; hence thesis; end; A50: 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 A51: Partial_Sums(Prob*A) is convergent; then A52: (Prob*A) is summable by SERIES_1:def 2; A53: for n being Element of NAT holds Sum(Prob*A)-Sum((Prob*A)^\(n+1))=Partial_Sums(Prob*A).n proof let n be Element of 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 A52,SERIES_1:18; hence thesis; end; A54: for n being Element of NAT,m being Element of NAT st n<=m holds abs((Partial_Sums(Prob*A)).m -(Partial_Sums(Prob*A)).n) =abs((Sum_Shift_Seq(Prob,A)^\1).m -(Sum_Shift_Seq(Prob,A)^\1).n) proof let n be Element of NAT; let m be Element of NAT; assume n<=m; A55: Partial_Sums(Prob*A).m-Partial_Sums(Prob*A).n= Partial_Sums(Prob*A).m-(Sum(Prob*A)-Sum((Prob*A)^\(n+1))) by A53; A56: 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 A53,A55; A57: (Partial_Sums(Prob*A).m-Partial_Sums(Prob*A).n)= (Sum((Prob*A)^\(n+1))-Sum((Prob*A)^\(m+1))) by A56; A58: 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*@Shift_Seq(A,n)).k=( (Prob*A)^\n ).k proof let k be Element of NAT; dom(Prob*@Shift_Seq(A,n))=NAT by FUNCT_2:def 1; then A59: (Prob*@Shift_Seq(A,n)).k =Prob.((@Shift_Seq(A,n)).k) by FUNCT_1:22; dom(Prob*A)=NAT by FUNCT_2:def 1; then A60: Prob.(A.(n+k))=(Prob*A).(n+k) by FUNCT_1:22; (Prob*A).(k+n)=((Prob*A)^\n).k by NAT_1:def 3; hence thesis by A59,NAT_1:def 3,A60; end; hence thesis by FUNCT_2:113; end; A61: for n being Element of NAT holds (Sum_Shift_Seq(Prob,A)^\1).n=Sum((Prob*A)^\(n+1)) proof let n be Element of NAT; A62:(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*@Shift_Seq(A,n+1) ) by Def15; hence thesis by A58,A62; end; A64: abs((Partial_Sums(Prob*A)).m -(Partial_Sums(Prob*A)).n) =abs((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 A57,A61; hence thesis by A61; end; abs((Sum_Shift_Seq(Prob,A)^\1).n-(Sum_Shift_Seq(Prob,A)^\1).m)= abs((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 A65:-0>-((Sum_Shift_Seq(Prob,A)^\1).n- (Sum_Shift_Seq(Prob,A)^\1).m); abs((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 A65,ABSVALUE:def 1; hence thesis; end; suppose A66:(Sum_Shift_Seq(Prob,A)^\1).n- (Sum_Shift_Seq(Prob,A)^\1).m<0; abs((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 A66,ABSVALUE:def 1; hence thesis; end; end; hence thesis by A64; end; A67: (for sr being real number st 0 Sum(Prob*A); A75: (Prob*A) is summable by A51,SERIES_1:def 2; A76: for n being Element of NAT holds B1.n=B.n proof let n be Element of NAT; A77: for n being Element of NAT holds (Sum_Shift_Seq(Prob,A)^\1).n=Sum((Prob*A)^\(n+1)) proof let n be Element of NAT; A78: (Sum_Shift_Seq(Prob,A)^\1).n=Sum_Shift_Seq(Prob,A).(n+1) by NAT_1:def 3; A79: 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*@Shift_Seq(A,n)).k=( (Prob*A)^\n ).k proof let k be Element of NAT; dom(Prob*@Shift_Seq(A,n))=NAT by FUNCT_2:def 1; then A80: (Prob*@Shift_Seq(A,n)).k =Prob.((@Shift_Seq(A,n)).k) by FUNCT_1:22; dom(Prob*A)=NAT by FUNCT_2:def 1; then A81: Prob.(A.(n+k))=(Prob*A).(n+k) by FUNCT_1:22; (Prob*A).(k+n)=((Prob*A)^\n).k by NAT_1:def 3; hence thesis by A80,NAT_1:def 3,A81; end; hence thesis by FUNCT_2:113; end; Sum_Shift_Seq(Prob,A).(n+1)=Sum(Prob*@Shift_Seq(A,n+1) ) by Def15; hence thesis by A78,A79; end; A82: (Sum_Shift_Seq(Prob,A)^\1).n=Sum((Prob*A)^\(n+1)) by A77; Sum((Prob*A)) = Partial_Sums((Prob*A)).n + Sum((Prob*A)^\(n+1)) by A75,SERIES_1:18; then B1.n = Partial_Sums((Prob*A)).n + (Sum_Shift_Seq(Prob,A)^\1).n by A82,FUNCOP_1:13; hence thesis by A73,VALUED_1:def 1,A74; end; A83: lim B1 = lim B proof ex k being Element of NAT st for n being Element of NAT st k<=n holds B1.n=B.n proof take 1; thus thesis by A76; end; hence thesis by SEQ_4:32; end; A84: Sum(Prob*A)= B1.1 by FUNCOP_1:13 .= lim B by A83,SEQ_4:41; A85: lim B= lim (Sum_Shift_Seq(Prob,A)^\1)+ lim Partial_Sums((Prob*A)) by A74,A72,SEQ_2:20; Sum(Prob*A)=lim (Sum_Shift_Seq(Prob,A)^\1)+ Sum((Prob*A)) by A84,A85,SERIES_1:def 3; hence thesis by A72,SEQ_4:36,SEQ_4:35; end; lim(Sum_Shift_Seq(Prob,A))=0 & Sum_Shift_Seq(Prob,A) is convergent by A1,A50; hence thesis by PROB_2:def 1,A5,A7,A40,A41; end; theorem Th14: ( for X being set, A being SetSequence of X holds for n being Element of NAT, x being set holds ( (ex k being Element of NAT st x in Shift_Seq(A,n).k) iff (ex k being Element of NAT st k>=n & x in A.k) ) ) & ( for X being set, A being SetSequence of X holds for x being set holds x in Intersection Union_Shift_Seq A iff for m being Element of NAT holds ex n being Element of NAT st n>=m & x in A.n ) & ( for A being SetSequence of Sigma holds for x being set holds x in @Intersection @Union_Shift_Seq A iff for m being Element of NAT holds ex n being Element of NAT st n>=m & x in A.n ) & ( for X being set, A being SetSequence of X holds for x being set holds ( (x in Union Intersect_Shift_Seq A ) iff (ex n being Element of NAT st for k being Element of NAT st k>=n holds x in A.k ) ) ) & ( for A being SetSequence of Sigma holds for x being set holds ( (x in Union @Intersect_Shift_Seq A ) iff (ex n being Element of NAT st for k being Element of 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 @Intersect_Shift_Seq (@Complement A) ) iff (ex n being Element of NAT st for k being Element of 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 Element of NAT, x being set holds ( (ex k being Element of NAT st x in Shift_Seq(A,n).k) iff (ex k being Element of NAT st k>=n & x in A.k) ) proof let X be set, A be SetSequence of X; let n be Element of NAT, x be set; hereby assume ex k being Element of NAT st x in Shift_Seq(A,n).k; then consider k being Element of NAT such that A2: x in Shift_Seq(A,n).k; A3: x in A.(k+n) by NAT_1:def 3,A2; consider k being Element of NAT such that A4: x in A.(k+n) by A3; consider k being Element of NAT such that A5: k>=n & x in A.k by A4,NAT_1:11; thus ex k being Element of NAT st k>=n & x in A.k by A5; end; assume ex k being Element of NAT st k>=n & x in A.k; then consider k being Element of NAT such that A6: k>=n & x in A.k; consider knat being Nat such that A7: k=n+knat by NAT_1:10,A6; reconsider knat as Element of NAT by ORDINAL1:def 13; x in A.k implies x in Shift_Seq(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 set holds x in Intersection Union_Shift_Seq A iff for m being Element of NAT holds ex n being Element of NAT st n>=m & x in A.n proof let X be set,A be SetSequence of X; let x be set; hereby assume A9: x in Intersection Union_Shift_Seq A; A10: for n being Element of NAT holds (x in (Union_Shift_Seq A).n implies ex k being Element of NAT st k>=n & x in A.k) proof let n be Element of NAT; assume A11: x in (Union_Shift_Seq A).n; A12: x in (Union_Shift_Seq A).n implies x in Union Shift_Seq(A,n) by Def9; A13: ex k being Element of NAT st x in Shift_Seq(A,n).k by A11,A12,PROB_1:25; consider k being Element of NAT such that A14: k>=n & x in A.k by A13,A1; take k; thus thesis by A14; end; A15: for m being Element of NAT holds ex n being Element of NAT st n>=m & x in A.n proof let m be Element of NAT; x in (Union_Shift_Seq A).m by A9,PROB_1:29; hence thesis by A10; end; thus for m being Element of NAT holds ex n being Element of NAT st n>=m & x in A.n by A15; end; assume A16: for m being Element of NAT holds ex n being Element of NAT st n>=m & x in A.n; A17: for m being Element of NAT holds ( (ex n being Element of NAT st n>=m & x in A.n) implies (x in (Union_Shift_Seq A).m ) ) proof let m be Element of NAT; assume ex n being Element of NAT st n>=m & x in A.n; then consider n being Element of NAT such that A18: n>=m & x in A.n; ex k being Element of NAT st x in Shift_Seq(A,m).k by A18,A1; then x in Union Shift_Seq(A,m) by PROB_1:25; hence thesis by Def9; end; for m being Element of NAT holds x in (Union_Shift_Seq A).m proof let m be Element of NAT; ex n being Element of NAT st n>=m & x in A.n by A16; hence thesis by A17; end; hence thesis by PROB_1:29; end; A19: for A being SetSequence of Sigma holds for x being set holds x in @Intersection @Union_Shift_Seq A iff for m being Element of NAT holds ex n being Element of NAT st n>=m & x in A.n proof let A be SetSequence of Sigma; let x be set; @Intersection @Union_Shift_Seq A=Intersection Union_Shift_Seq 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 set holds ( (x in Union Intersect_Shift_Seq A ) iff (ex n being Element of NAT st for k being Element of NAT st k>=n holds x in A.k ) ) proof let X be set, A be SetSequence of X; let x be set; hereby assume x in Union Intersect_Shift_Seq A; then consider n being Element of NAT such that A21: x in (Intersect_Shift_Seq A).n by PROB_1:25; A22: (Intersect_Shift_Seq A).n = Intersection Shift_Seq(A,n) by Def12; for k being Element of NAT st k>=n holds x in A.k proof let k be Element of NAT; assume A23: n<=k; consider knat being Nat such that A24: k=n+knat by A23,NAT_1:10; reconsider knat as Element of NAT by ORDINAL1:def 13; A25: x in A.k iff x in (Shift_Seq(A,n)).knat by A24,NAT_1:def 3; thus thesis by A22,A21,PROB_1:29,A25; end; hence ex n being Element of NAT st for k being Element of NAT st k>=n holds x in A.k; end; assume ex n being Element of NAT st for k being Element of NAT st k>=n holds x in A.k; then consider n being Element of NAT such that A26: for k being Element of NAT st k>=n holds x in A.k; set knat = the Nat; for s being Element of NAT holds x in (Shift_Seq(A,n)).s proof let s be Element of NAT; x in (Shift_Seq(A,n)).s iff x in A.(n+s) by NAT_1:def 3; hence thesis by NAT_1:12,A26; end; then x in Intersection Shift_Seq(A,n) by PROB_1:29; then x in (Intersect_Shift_Seq A).n by Def12; hence thesis by PROB_1:25; end; for A being SetSequence of Sigma holds for x being Element of Omega holds ( (x in Union @Intersect_Shift_Seq (@Complement A) ) iff (ex n being Element of NAT st for k being Element of 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 @Intersect_Shift_Seq (@Complement A); then consider n being Element of NAT such that A27: x in (@Intersect_Shift_Seq (@Complement A)).n by PROB_1:25; A28: (@Intersect_Shift_Seq (@Complement A)).n = Intersection @Shift_Seq(@Complement A,n) by Def12; set m = the Element of NAT; for k being Element of NAT st k>=n holds not x in A.k proof let k be Element of 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 13; A31: x in (@Complement A).k iff x in (@Shift_Seq(@Complement A,n)).knat by A30,NAT_1:def 3; x in (A.k)` by PROB_1:def 4,A28, A27,PROB_1:29,A31; then x in Omega \ A.k by SUBSET_1:def 5; hence thesis by XBOOLE_0:def 5; end; hence ex n being Element of NAT st for k being Element of NAT st k>=n holds not x in A.k; end; assume ex n being Element of NAT st for k being Element of NAT st k>=n holds not x in A.k; then consider n being Element of NAT such that A32: for k being Element of NAT st k>=n holds not x in A.k; set k = the Element of NAT; A33: for k being Element of NAT st n<=k holds x in (@Complement A).k proof let k be Element of 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 5; hence thesis by PROB_1:def 4; end; for s being Element of NAT holds x in (@Shift_Seq(@Complement A,n)).s proof let s be Element of NAT; x in (@Shift_Seq(@Complement A,n)).s iff x in (@Complement A).(n+s) by NAT_1:def 3; hence thesis by NAT_1:12,A33; end; then x in Intersection @Shift_Seq(@Complement A,n) by PROB_1:29; then x in (@Intersect_Shift_Seq @Complement A).n by Def12; hence x in Union (@Intersect_Shift_Seq (@Complement A)) by PROB_1:25; end; hence thesis by A1,A8,A19,A20; end; theorem Th15: lim_sup A = @lim_sup A & lim_inf A = @lim_inf A & @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 thus A1: lim_sup A = @lim_sup A proof A2: for n being Element of NAT holds for x being set holds (ex k being Element of NAT st x in (A^\n).k) iff (ex k being Element of NAT st k>=n & x in A.k ) proof let n be Element of NAT; let x be set; hereby assume ex k being Element of NAT st x in (A^\n).k; then consider k being Element of NAT such that A3: x in (A^\n).k; A4: x in A.(k+n) by NAT_1:def 3,A3; consider k being Element of NAT such that A5: x in A.(k+n) by A4; consider k being Element of NAT such that A6: k>=n & x in A.k by NAT_1:11,A5; thus ex k being Element of NAT st k>=n & x in A.k by A6; end; assume ex k being Element of NAT st k>=n & x in A.k; then consider k being Element of NAT such that A7: k>=n & x in A.k; consider knat being Nat such that A8: k=n+knat by NAT_1:10,A7; reconsider knat as Element of NAT by ORDINAL1:def 13; A9: x in A.k implies x in (A^\n).knat by A8,NAT_1:def 3; thus thesis by A7,A9; end; A10: for x being set holds (for m being Element of NAT holds ex n being Element of NAT st n>=m & x in A.n ) iff (for m being Element of NAT holds ex n being Element of NAT st x in A.(m+n) ) proof let x be set; hereby assume A11: for m being Element of NAT holds ex n being Element of NAT st n>=m & x in A.n; thus for m being Element of NAT holds ex n being Element of NAT st x in A.(m+n) proof let m be Element of NAT; ex n being Element of NAT st n>=m & x in A.n by A11; then consider n being Element of NAT such that A12: x in (A^\m).n by A2; x in A.(m+n) by NAT_1:def 3,A12; hence thesis; end; end; assume A13:for m being Element of NAT holds ex n being Element of NAT st x in A.(m+n); thus for m being Element of NAT holds ex n being Element of NAT st n>=m & x in A.n proof let m be Element of NAT; consider n being Element of NAT such that A14: x in A.(m+n) by A13; x in (A^\m).n by NAT_1:def 3,A14; hence thesis by A2; end; end; A15: for x being set holds (x in @Intersection @Union_Shift_Seq A) iff (for m being Element of NAT holds ex n being Element of NAT st x in A.(m+n) ) proof let x be set; hereby assume x in @Intersection @Union_Shift_Seq A; then A16: for m being Element of NAT holds ex n being Element of NAT st n>=m & x in A.n by Th14; thus for m being Element of NAT holds ex n being Element of NAT st x in A.(m+n) by A16,A10; end; assume for m being Element of NAT holds ex n being Element of NAT st x in A.(m+n); then for m being Element of NAT holds ex n being Element of NAT st n>=m & x in A.n by A10; hence thesis by Th14; end; for x being set holds x in lim_sup A iff x in @Intersection @Union_Shift_Seq A proof let x be set; hereby assume x in lim_sup A; then A17: for m being Element of NAT holds ex n being Element of NAT st x in A.(m+n) by SETLIM_1:66; thus x in @Intersection @Union_Shift_Seq A by A17,A15; end; assume x in @Intersection @Union_Shift_Seq A; then for m being Element of NAT holds ex n being Element of NAT st x in A.(m+n) by A15; hence x in lim_sup A by SETLIM_1:66; end; hence thesis by TARSKI:2; end; A18: for A holds lim_inf A = @lim_inf A proof let A; A19: for x being set holds (ex n being Element of NAT st for k being Element of NAT st k>=n holds x in A.k) iff (ex n being Element of NAT st for k being Element of NAT holds x in A.(n+k)) proof let x be set; hereby assume ex n being Element of NAT st for k being Element of NAT st k>=n holds x in A.k; then consider n being Element of NAT such that A20: for k being Element of NAT st k>=n holds x in A.k; for k being Element of NAT holds x in A.(n+k) by NAT_1:11,A20; hence ex n being Element of NAT st for k being Element of NAT holds x in A.(n+k); end; assume ex n being Element of NAT st for k being Element of NAT holds x in A.(n+k); then consider n being Element of NAT such that A21: for k being Element of NAT holds x in A.(n+k); for k being Element of NAT st k>=n holds x in A.k proof let k be Element of NAT; assume n<=k; then consider knat being Nat such that A22: k=n+knat by NAT_1:10; reconsider knat as Element of NAT by ORDINAL1:def 13; x in A.((n+knat)) by A21; hence thesis by A22; end; hence thesis; end; for x being set holds x in @lim_inf A iff x in lim_inf A proof let x be set; hereby assume x in @lim_inf A; then ex n being Element of NAT st for k being Element of NAT st k>=n holds x in A.k by Th14; then ex n being Element of NAT st for k being Element of NAT holds x in A.(n+k) by A19; hence x in lim_inf A by SETLIM_1:67; end; assume x in lim_inf A; then ex n being Element of NAT st for k being Element of NAT holds x in A.(n+k) by SETLIM_1:67; then ex n being Element of NAT st for k being Element of NAT st k>=n holds x in A.k by A19; hence thesis by Th14; end; hence thesis by TARSKI:2; end; A23: @lim_inf @Complement A = (@lim_sup A)` proof for x being set holds (x in @lim_inf @Complement A iff x in (@lim_sup A)` ) proof let x be set; hereby assume x in @lim_inf @Complement A; then x in Omega & ex n being Element of NAT st for k being Element of 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 5; end; assume A24: x in (@lim_sup A)`; x in (Omega \ @lim_sup A) by A24,SUBSET_1:def 5; then not x in @Intersection @Union_Shift_Seq A by XBOOLE_0:def 5; then ex m being Element of NAT st for n being Element of NAT st n>=m holds not x in A.n by Th14; hence thesis by A24,Th14; 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:67; hence thesis by A23,SUBSET_1:def 5; end; hence thesis by A1,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 Th15; 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 by Th15; 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 by Th15; A10: Prob.@lim_inf @Complement B = Prob.lim_inf @Complement B by Th15; 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; A13: for Q being SetSequence of Sigma holds @Intersect_Shift_Seq Q is non-descending proof let Q be SetSequence of Sigma; (inferior_setsequence Q) = (@Intersect_Shift_Seq Q) by Th11; hence thesis by SETLIM_1:23; end; A14: @Intersect_Shift_Seq @Complement B is non-descending by A13; A15: Prob.(@lim_inf @Complement B)= lim (Prob*(@Intersect_Shift_Seq (@Complement B) ) ) by A14,PROB_2:20; A16: for n being Element of NAT holds (Prob*(@Intersect_Shift_Seq (@Complement B) )).n = 0 proof let n be Element of NAT; dom(Prob*(@Intersect_Shift_Seq (@Complement B) )) = NAT by FUNCT_2:def 1; then A17: (Prob*(@Intersect_Shift_Seq (@Complement B) )).n = Prob.( (@Intersect_Shift_Seq (@Complement B)).n ) by FUNCT_1:22; (@Intersect_Shift_Seq (@Complement B)).n = Intersection @Shift_Seq(@Complement B,n) by Def12; then A18: (Prob*(@Intersect_Shift_Seq (@Complement B) )).n = Prob.(Intersection @Partial_Intersection @Shift_Seq(@Complement B,n) ) by PROB_3:33,A17; @Partial_Intersection @Shift_Seq(@Complement B,n) is non-ascending by PROB_3:31; then A19: (Prob*(@Intersect_Shift_Seq (@Complement B) )).n = lim (Prob*(@Partial_Intersection @Shift_Seq(@Complement B,n))) by PROB_1:def 13,A18; A20: for k being Element of NAT holds (Prob*(@Partial_Intersection (@Complement @Shift_Seq(B,n)))).k <= ((1+(Partial_Sums(Prob*@Shift_Seq(B,n))))").k proof let k be Element of NAT; A21: for k being Element of NAT holds @Shift_Seq(B,k) is_all_independent_wrt Prob proof let k be Element of NAT; for C being SetSequence of Sigma st (ex e being sequence of NAT st (e is one-to-one & (for n being Element of NAT holds (@Shift_Seq(B,k)).(e.n) = C.n))) holds (for n being Element of 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 A22: e is one-to-one and A23: for n being Element of NAT holds (@Shift_Seq(B,k)).(e.n) = C.n; A24: @Shift_Seq(B,k)=(B*Special_Function2(k)) proof for n being set st n in NAT holds (@Shift_Seq(B,k)).n=(B*Special_Function2(k)).n proof let n be set; assume n in NAT; then reconsider n as Element of NAT; dom(B*Special_Function2(k))=NAT by FUNCT_2:def 1; then A25: (B*Special_Function2(k)).n = B.((Special_Function2(k)).n) by FUNCT_1:22; (Special_Function2(k)).n = n+k by Def3; hence thesis by NAT_1:def 3,A25; end; hence thesis by FUNCT_2:18; end; A26:for n being Element of NAT holds (B*Special_Function2(k)).(e.n) = B.( (Special_Function2(k)*e).n ) proof let n be Element of NAT; 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:22; hence thesis; end; A27: for n being Element of NAT holds B.( ( (Special_Function2(k)*e) ).n ) = C.n proof let n be Element of NAT; (B*Special_Function2(k)).(e.n) = C.n by A24,A23; hence thesis by A26; end; (Special_Function2(k))*e is one-to-one by A22,FUNCT_1:46; hence thesis by A11,A27,Def8; end; hence thesis by Def8; end; A28: for A being SetSequence of Sigma holds for n being Element of NAT holds Partial_Product(Prob*(@Complement A)).n <= ((1+(Partial_Sums(Prob*A))).n)" proof let A be SetSequence of Sigma; let n be Element of NAT; A29: 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 A30: 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 A31: for n being Element of NAT holds (Prob*A).n >=0 proof let n be Element of NAT; dom(Prob*A)=NAT by FUNCT_2:def 1; then (Prob*A).n=Prob.(A.n) by FUNCT_1:22; hence thesis by PROB_1:def 13; end; A32: for n being Element of NAT holds Partial_Sums(Prob*A).n >=0 proof let n be Element of NAT; defpred J[Element of NAT] means Partial_Sums(Prob*A).\$1 >= 0; Partial_Sums(Prob*A).0 = (Prob*A).0 by SERIES_1:def 1; then A33: J[0] by A31; A34: for k being Element of NAT st J[k] holds J[k+1] proof let k be Element of NAT; assume A35: J[k]; A36: (Prob*A).(k+1)>=0 by A31; Partial_Sums(Prob*A).(k+1) = Partial_Sums(Prob*A).k +(Prob*A).(k+1) by SERIES_1:def 1; hence thesis by A35,A36; end; for k being Element of NAT holds J[k] from NAT_1:sch 1(A33,A34); 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 A37: x>=0; per cases; suppose A38: x>0; A39: exp_R.(-x) >= 0 by SIN_COS:59; set z=-x; A40: exp_R(x)*exp_R(z) = exp_R(x+z) by SIN_COS:55; exp_R.(-x)*(1+x) <= 1 by Th2,A39,XREAL_1:66,A40,SIN_COS:56; hence thesis by A38,XREAL_1:79; end; suppose x<=0; then x=0 by A37; hence thesis by SIN_COS:56; end; end; hence thesis by A32; end; hence thesis by A30,XXREAL_0:2; end; for A being SetSequence of Sigma holds for n being Element of 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 Element of NAT; 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 A29; end; dom(Prob*(@Partial_Intersection (@Complement @Shift_Seq(B,n)))) =NAT by FUNCT_2:def 1; then (Prob*(@Partial_Intersection (@Complement @Shift_Seq(B,n)))).k = Prob.((@Partial_Intersection (@Complement @Shift_Seq(B,n))).k) by FUNCT_1:22; then (Prob*(@Partial_Intersection (@Complement @Shift_Seq(B,n)))).k = Partial_Product(Prob*@Complement @Shift_Seq(B,n)).k by A21,Th10; then (Prob*(@Partial_Intersection (@Complement @Shift_Seq(B,n)))).k <= ((1+(Partial_Sums(Prob*@Shift_Seq(B,n)))).k)" by A28; hence thesis by VALUED_1:10; end; A41: Partial_Sums(Prob*@Shift_Seq(B,n)) is divergent_to+infty proof per cases; suppose n=0; hence thesis by NAT_1:48,A12; end; suppose n<>0; then A42: n-1 is Element of NAT by NAT_1:20; consider y being Element of NAT such that A43: y=n-1 by A42; set B2 = NAT --> -(Partial_Sums(Prob*B)).y; A44: Partial_Sums(Prob*B) + B2 is divergent_to+infty by A12,LIMFUNC1:45; for r being Real ex q being Element of NAT st for m being Element of NAT st q<=m holds r<(Partial_Sums(Prob*@Shift_Seq(B,n))).m proof let r be Real; for r being Real ex q being Element of NAT st for m being Element of NAT st q<=m holds r<(Partial_Sums(Prob*@Shift_Seq(B,n))).m proof let r be Real; A45: for m being Element of NAT st n<=m holds (Partial_Sums(Prob*B) + B2).m = (Partial_Sums(Prob*@Shift_Seq(B,n))).(m-n) proof let m be Element of NAT; assume n<=m; then consider knat being Nat such that A46: m=n+knat by NAT_1:10; reconsider knat as Element of NAT by ORDINAL1:def 13; defpred J[Element of NAT] means (Partial_Sums(Prob*B) + B2).(n+\$1) = (Partial_Sums(Prob*@Shift_Seq(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; then (Partial_Sums(Prob*B) + B2).n = (Partial_Sums(Prob*B)).n + (-(Partial_Sums(Prob*B)).(n-1)) by A43,FUNCOP_1:13; then (Partial_Sums(Prob*B) + B2).n = (Partial_Sums(Prob*B)).n -(Partial_Sums(Prob*B)).(n-1); then A48: (Partial_Sums(Prob*B) + B2).n = ( (Partial_Sums(Prob*B)).(n-1) + (Prob*B).((n-1)+1) ) -(Partial_Sums(Prob*B)).(n-1) by A42,SERIES_1:def 1; dom(Prob*@Shift_Seq(B,n))=NAT by FUNCT_2:def 1; then A49: (Prob*@Shift_Seq(B,n)).0 = Prob.( (@Shift_Seq(B,n)).0 ) by FUNCT_1:22; A50: (@Shift_Seq(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*@Shift_Seq(B,n)).0 by FUNCT_1:22,A50,A49,A48; hence thesis by SERIES_1:def 1; end; A51: for k being Element of NAT st J[k] holds J[k+1] proof let k be Element of NAT; assume A52: J[k]; A53: 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 A53,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) ) + (-(Partial_Sums(Prob*B)).(n-1)) by A43,FUNCOP_1:13; then (Partial_Sums(Prob*B) + B2).(n+k+1) = (Partial_Sums(Prob*B)).(n+k) + (Prob*B).((n+k)+1) + B2.(n+k) by A43,FUNCOP_1:13; then (Partial_Sums(Prob*B) + B2).(n+k+1) = ( (Partial_Sums(Prob*B)).(n+k) + B2.(n+k) ) + (Prob*B).((n+k)+1); then A54: (Partial_Sums(Prob*B) + B2).(n+k+1) = (Partial_Sums(Prob*@Shift_Seq(B,n))).((n+k)-n) + (Prob*B).((n+k)+1) by A53,VALUED_1:def 1,A52; (Prob*@Shift_Seq(B,n)).((n+k-n)+1) = (Prob*B).((n+k)+1) proof dom(Prob*@Shift_Seq(B,n))=NAT by FUNCT_2:def 1; then A55: (Prob*@Shift_Seq(B,n)).((n+k-n)+1) = Prob.((@Shift_Seq(B,n)).(k+1)) by FUNCT_1:22; A56: (@Shift_Seq(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 FUNCT_1:22,A56,A55; end; hence thesis by A54,SERIES_1:def 1; end; for k being Element of NAT holds J[k] from NAT_1:sch 1(A47,A51); then (Partial_Sums(Prob*B) + B2).(n+knat) = (Partial_Sums(Prob*@Shift_Seq(B,n))).((n+knat)-n); hence thesis by A46; end; A57: ex q being Element of NAT st for m being Element of NAT st (q+n)<=(m+n) holds r<(Partial_Sums(Prob*B) + B2).(m+n) proof consider q being Element of NAT such that A58: for m being Element of NAT st q<=m holds r<(Partial_Sums(Prob*B) + B2).m by A44,LIMFUNC1:def 4; for m being Element of NAT st (q+n)<=(m+n) holds r<(Partial_Sums(Prob*B) + B2).(m+n) proof let m be Element of 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 A58; end; hence thesis; end; ex s being Element of NAT st for m being Element of NAT st s<=m holds r<(Partial_Sums(Prob*@Shift_Seq(B,n))).m proof consider q being Element of NAT such that A59: for m being Element of NAT st (q+n)<=(m+n) holds r<(Partial_Sums(Prob*B) + B2).(m+n) by A57; take s=q+n; let m be Element of NAT; assume A60: s<=m; set z=m+n; (Partial_Sums(Prob*B) + B2).z = (Partial_Sums(Prob*@Shift_Seq(B,n))).(z-n) by NAT_1:12,A45; hence thesis by A60,NAT_1:12,A59; end; hence thesis; end; hence thesis; end; hence thesis by LIMFUNC1:def 4; end; end; A61: 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; A62: for A being SetSequence of Sigma holds (for r being Real ex n being Element of NAT st for m being Element of NAT st n <= m holds r < (Partial_Sums(Prob*A)).m) implies (for r being Real ex n being Element of NAT st for m being Element of NAT st n <= m holds r < (1+(Partial_Sums(Prob*A))).m ) proof let A be SetSequence of Sigma; assume A63: (for r being Real ex n being Element of NAT st for m being Element of NAT st n <= m holds r < (Partial_Sums(Prob*A)).m); let r be Real; consider n being Element of NAT such that A64: for m being Element of NAT st n <= m holds r < (Partial_Sums(Prob*A)).m by A63; take n; for m being Element of NAT st n<=m holds r < (1+(Partial_Sums(Prob*A))).m proof let m be Element of NAT; assume n<=m; then A65: r < (Partial_Sums(Prob*A)).m by A64; A66: (Partial_Sums(Prob*A)).m < ((Partial_Sums(Prob*A)).m+1) by XREAL_1:31; (1+(Partial_Sums(Prob*A))).m = (Partial_Sums(Prob*A)).m + 1 by VALUED_1:2; hence thesis by A65,A66,XXREAL_0:2; end; hence thesis; end; assume Partial_Sums(Prob*A) is divergent_to+infty; then for r being Real ex n being Element of NAT st for m being Element of NAT st n <= m holds r < (Partial_Sums(Prob*A)).m by LIMFUNC1:def 4; then for r being Real ex n being Element of NAT st for m being Element of NAT st n <= m holds r < (1+(Partial_Sums(Prob*A))).m by A62; then 1+(Partial_Sums(Prob*A)) is divergent_to+infty by LIMFUNC1:def 4; hence thesis by LIMFUNC1:61; end; (@Partial_Intersection (@Complement @Shift_Seq(B,n))) is non-ascending by PROB_3:31; then A67: (Prob*(@Partial_Intersection (@Complement @Shift_Seq(B,n)))) is convergent & (1+(Partial_Sums(Prob*@Shift_Seq(B,n))))" is convergent by PROB_1:def 13,A41,A61; A68: lim( (1+(Partial_Sums(Prob*@Shift_Seq(B,n))))" ) = 0 by A41,A61; A69: for k being Element of NAT holds 0<=(Prob*(@Partial_Intersection (@Complement @Shift_Seq(B,n)))).k proof let k be Element of NAT; dom(Prob*(@Partial_Intersection (@Complement @Shift_Seq(B,n)))) = NAT by FUNCT_2:def 1; then (Prob*(@Partial_Intersection (@Complement @Shift_Seq(B,n)))).k = Prob.( (@Partial_Intersection (@Complement @Shift_Seq(B,n))).k) by FUNCT_1:22; hence thesis by PROB_1:def 13; end; A70: lim (Prob*(@Partial_Intersection (@Complement @Shift_Seq(B,n)))) <= 0 by A67,A20,SEQ_2:32,A68; @Complement @Shift_Seq(B,n) = @Shift_Seq(@Complement B,n) proof for k being set st k in NAT holds (@Complement @Shift_Seq(B,n)).k = (@Shift_Seq(@Complement B,n)).k proof let k be set; assume k in NAT; then reconsider k as Element of NAT; A71: (@Complement @Shift_Seq(B,n)).k = ( ( B^\n ).k )` by PROB_1:def 4; (@Shift_Seq(@Complement B,n)).k = (@Complement B).(k+n) by NAT_1:def 3; then (@Shift_Seq(@Complement B,n)).k = (B.(k+n))` by PROB_1:def 4; hence thesis by A71,NAT_1:def 3; end; hence thesis by FUNCT_2:18; end; hence thesis by A69,A67,SEQ_2:31,A70,A19; end; set B2 = NAT --> (0 qua Real); A72: ex n being Element of NAT st B2.n=0 proof take 1; thus thesis by FUNCOP_1:13; end; A73: lim B2 = 0 by A72,SEQ_4:40; A74: B2 is convergent & ex k being Element of NAT st for n being Element of NAT st k<=n holds B2.n = (Prob*(@Intersect_Shift_Seq (@Complement B) )).n proof ex k being Element of NAT st for n being Element of NAT st k<=n holds B2.n = (Prob*(@Intersect_Shift_Seq (@Complement B) )).n proof A75: for n being Element of NAT st n>=0 holds B2.n = (Prob*(@Intersect_Shift_Seq (@Complement B) )).n proof let n be Element of NAT; assume n>=0; B2.n = 0 & (Prob*(@Intersect_Shift_Seq (@Complement B) )).n = 0 by A16,FUNCOP_1:13; hence thesis; end; take 0; thus thesis by A75; end; hence thesis; end; Prob.(@lim_inf @Complement B)=0 & Prob.(@lim_inf @Complement B) + Prob.(@lim_sup B) = 1 by A15,A74,SEQ_4:32,A73,Th15; 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 Element of NAT holds (Prob*A).n >= 0 proof let n be Element of NAT; dom(Prob*A)=NAT by FUNCT_2:def 1; then (Prob*A).n = Prob.(A.n) by FUNCT_1:22; hence thesis by PROB_1:def 13; end; A4: (not (Prob*A) is summable implies not Partial_Sums(Prob*A) is bounded_above) & not (Prob*A) is summable by A3,SERIES_1:20,A1,SERIES_1:def 2; Partial_Sums(Prob*A) is divergent_to+infty by A4,A3,SERIES_1:19,LIMFUNC1:56; 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*@Shift_Seq(A,n1+1))).n <= Partial_Sums(Prob*A).(n1+1+n) - Partial_Sums(Prob*A).n1 proof A1: dom(Prob*@Shift_Seq(A,(n1+1)))=NAT by FUNCT_2:def 1; A2: dom(Prob*A)=NAT by FUNCT_2:def 1; defpred P[Element of NAT] means (Partial_Sums(Prob*@Shift_Seq(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.(@Shift_Seq(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:22; A6: (Prob*@Shift_Seq(A,n1+1)).0 = (Prob*A).(n1+1) by A1,FUNCT_1:22,A4,A5; A7: P[0] by SERIES_1:def 1,A6,A3; A8: for k being Element of NAT st P[k] holds P[k+1] proof let k being Element of NAT; assume A9: (Partial_Sums(Prob*@Shift_Seq(A,n1+1))).k <= Partial_Sums(Prob*A).(k+n1+1) - Partial_Sums(Prob*A).n1; A10: (Partial_Sums(Prob*@Shift_Seq(A,n1+1))).k+ (Prob*@Shift_Seq(A,n1+1)).(k+1)<= Partial_Sums(Prob*A).(k+n1+1) - Partial_Sums(Prob*A).n1+ (Prob*@Shift_Seq(A,n1+1)).(k+1) by A9,XREAL_1:8; A11: (Partial_Sums(Prob*@Shift_Seq(A,n1+1))).(k+1)<= Partial_Sums(Prob*A).(k+n1+1) - Partial_Sums(Prob*A).n1+ (Prob*@Shift_Seq(A,n1+1)).(k+1) by SERIES_1:def 1,A10; A12: (Partial_Sums(Prob*@Shift_Seq(A,n1+1))).(k+1) + Partial_Sums(Prob*A).n1<= Partial_Sums(Prob*A).(k+n1+1)+(Prob*@Shift_Seq(A,n1+1)).(k+1) - Partial_Sums(Prob*A).n1 + Partial_Sums(Prob*A).n1 by A11,XREAL_1:8; A13: (Partial_Sums(Prob*@Shift_Seq(A,n1+1))).(k+1) + Partial_Sums(Prob*A).n1-Partial_Sums(Prob*A).(k+n1+1)<= (Prob*@Shift_Seq(A,n1+1)).(k+1)+Partial_Sums(Prob*A).(k+n1+1) -Partial_Sums(Prob*A).(k+n1+1) by A12,XREAL_1:11; A14: @Shift_Seq(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*@Shift_Seq(A,n1+1))=NAT by FUNCT_2:def 1; A17: Prob.(@Shift_Seq(A,n1+1).(k+1))= (Prob*@Shift_Seq(A,n1+1)).(k+1) by A16,FUNCT_1:22; A18: ((Partial_Sums(Prob*@Shift_Seq(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:22; A19: (Partial_Sums(Prob*@Shift_Seq(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:8; 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*@Shift_Seq(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:11; hence thesis; end; for n being Element of NAT holds P[n] from NAT_1:sch 1(A7,A8); then P[n]; hence thesis; end; theorem Prob.( (@Intersect_Shift_Seq @Complement A).n ) = 1-Prob.( (@Union_Shift_Seq A).n ) proof A1: Prob.((@Intersect_Shift_Seq @Complement A).n) = Prob.((@Union_Shift_Seq A).n)` by Th9; Prob.((@Union_Shift_Seq A).n)` = Prob.( ([#] Sigma) \ (@Union_Shift_Seq A).n) by SUBSET_1:def 5; hence thesis by PROB_1:68,A1; 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;