let Omega, I be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for P being Probability of Sigma

for a being Element of Sigma

for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds

P . a = 1

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma

for a being Element of Sigma

for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds

P . a = 1

let P be Probability of Sigma; :: thesis: for a being Element of Sigma

for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds

P . a = 1

let a be Element of Sigma; :: thesis: for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds

P . a = 1

let F be ManySortedSigmaField of I,Sigma; :: thesis: ( F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 implies P . a = 1 )

reconsider T = tailSigmaField (F,I) as SigmaField of Omega by Th15;

set Ie = I \ ({} I);

A1: ( a in tailSigmaField (F,I) implies a in sigUn (F,(I \ ({} I))) )

A4: for E being finite Subset of I

for p, q being Event of Sigma st p in sigUn (F,E) & q in tailSigmaField (F,I) holds

p,q are_independent_respect_to P

p,q are_independent_respect_to P

A25: for u, v being Event of Sigma st u in sigUn (F,(I \ ({} I))) & v in tailSigmaField (F,I) holds

u,v are_independent_respect_to P

then a,a are_independent_respect_to P by A1, A25;

then P . (a /\ a) = (P . a) * (P . a) by PROB_2:def 4;

hence ( P . a = 0 or P . a = 1 ) by Th2; :: thesis: verum

for P being Probability of Sigma

for a being Element of Sigma

for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds

P . a = 1

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma

for a being Element of Sigma

for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds

P . a = 1

let P be Probability of Sigma; :: thesis: for a being Element of Sigma

for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds

P . a = 1

let a be Element of Sigma; :: thesis: for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds

P . a = 1

let F be ManySortedSigmaField of I,Sigma; :: thesis: ( F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 implies P . a = 1 )

reconsider T = tailSigmaField (F,I) as SigmaField of Omega by Th15;

set Ie = I \ ({} I);

A1: ( a in tailSigmaField (F,I) implies a in sigUn (F,(I \ ({} I))) )

proof

assume A3:
F is_independent_wrt P
; :: thesis: ( not a in tailSigmaField (F,I) or P . a = 0 or P . a = 1 )
assume A2:
a in tailSigmaField (F,I)
; :: thesis: a in sigUn (F,(I \ ({} I)))

sigUn (F,(I \ ({} I))) in futSigmaFields (F,I) by Def7;

hence a in sigUn (F,(I \ ({} I))) by A2, SETFAM_1:def 1; :: thesis: verum

end;sigUn (F,(I \ ({} I))) in futSigmaFields (F,I) by Def7;

hence a in sigUn (F,(I \ ({} I))) by A2, SETFAM_1:def 1; :: thesis: verum

A4: for E being finite Subset of I

for p, q being Event of Sigma st p in sigUn (F,E) & q in tailSigmaField (F,I) holds

p,q are_independent_respect_to P

proof

A13:
for p, q being Event of Sigma st p in finSigmaFields (F,I) & q in tailSigmaField (F,I) holds
let E be finite Subset of I; :: thesis: for p, q being Event of Sigma st p in sigUn (F,E) & q in tailSigmaField (F,I) holds

p,q are_independent_respect_to P

let p, q be Event of Sigma; :: thesis: ( p in sigUn (F,E) & q in tailSigmaField (F,I) implies p,q are_independent_respect_to P )

assume that

A5: p in sigUn (F,E) and

A6: q in tailSigmaField (F,I) ; :: thesis: p,q are_independent_respect_to P

for E being finite Subset of I holds q in sigUn (F,(I \ E))

end;p,q are_independent_respect_to P

let p, q be Event of Sigma; :: thesis: ( p in sigUn (F,E) & q in tailSigmaField (F,I) implies p,q are_independent_respect_to P )

assume that

A5: p in sigUn (F,E) and

A6: q in tailSigmaField (F,I) ; :: thesis: p,q are_independent_respect_to P

for E being finite Subset of I holds q in sigUn (F,(I \ E))

proof

then A7:
q in sigUn (F,(I \ E))
;
let E be finite Subset of I; :: thesis: q in sigUn (F,(I \ E))

sigUn (F,(I \ E)) in futSigmaFields (F,I) by Def7;

hence q in sigUn (F,(I \ E)) by A6, SETFAM_1:def 1; :: thesis: verum

end;sigUn (F,(I \ E)) in futSigmaFields (F,I) by Def7;

hence q in sigUn (F,(I \ E)) by A6, SETFAM_1:def 1; :: thesis: verum

per cases
( ( E <> {} & I \ E <> {} ) or not E <> {} or not I \ E <> {} )
;

end;

suppose A8:
( E <> {} & I \ E <> {} )
; :: thesis: p,q are_independent_respect_to P

then reconsider E = E as non empty Subset of I ;

reconsider IE = I \ E as non empty Subset of I by A8;

E misses IE by XBOOLE_1:79;

then P . (p /\ q) = (P . p) * (P . q) by A3, A5, A7, Th14;

hence p,q are_independent_respect_to P by PROB_2:def 4; :: thesis: verum

end;reconsider IE = I \ E as non empty Subset of I by A8;

E misses IE by XBOOLE_1:79;

then P . (p /\ q) = (P . p) * (P . q) by A3, A5, A7, Th14;

hence p,q are_independent_respect_to P by PROB_2:def 4; :: thesis: verum

suppose A9:
( not E <> {} or not I \ E <> {} )
; :: thesis: p,q are_independent_respect_to P

reconsider e = {} as Subset of I by XBOOLE_1:2;

A10: for u, v being Event of Sigma st u in {{},Omega} holds

u,v are_independent_respect_to P

then A12: sigUn (F,e) = {{},Omega} by Th3;

p,q are_independent_respect_to P

end;A10: for u, v being Event of Sigma st u in {{},Omega} holds

u,v are_independent_respect_to P

proof

Union (F | {}) = {}
by ZFMISC_1:2;
let u, v be Event of Sigma; :: thesis: ( u in {{},Omega} implies u,v are_independent_respect_to P )

assume A11: u in {{},Omega} ; :: thesis: u,v are_independent_respect_to P

end;assume A11: u in {{},Omega} ; :: thesis: u,v are_independent_respect_to P

per cases
( u = {} or u <> {} )
;

end;

suppose
u <> {}
; :: thesis: u,v are_independent_respect_to P

then
u = [#] Sigma
by A11, TARSKI:def 2;

hence u,v are_independent_respect_to P by PROB_2:19, PROB_2:24; :: thesis: verum

end;hence u,v are_independent_respect_to P by PROB_2:19, PROB_2:24; :: thesis: verum

then A12: sigUn (F,e) = {{},Omega} by Th3;

p,q are_independent_respect_to P

proof
end;

hence
p,q are_independent_respect_to P
; :: thesis: verumper cases
( E = {} or E <> {} )
;

end;

p,q are_independent_respect_to P

proof

Union (F | (I \ ({} I))) c= sigma (finSigmaFields (F,I))
let p, q be Event of Sigma; :: thesis: ( p in finSigmaFields (F,I) & q in tailSigmaField (F,I) implies p,q are_independent_respect_to P )

assume that

A14: p in finSigmaFields (F,I) and

A15: q in tailSigmaField (F,I) ; :: thesis: p,q are_independent_respect_to P

ex E being finite Subset of I st p in sigUn (F,E) by A14, Def10;

hence p,q are_independent_respect_to P by A4, A15; :: thesis: verum

end;assume that

A14: p in finSigmaFields (F,I) and

A15: q in tailSigmaField (F,I) ; :: thesis: p,q are_independent_respect_to P

ex E being finite Subset of I st p in sigUn (F,E) by A14, Def10;

hence p,q are_independent_respect_to P by A4, A15; :: thesis: verum

proof

then A24:
( T c= sigma T & sigUn (F,(I \ ({} I))) c= sigma (finSigmaFields (F,I)) )
by PROB_1:def 9;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (F | (I \ ({} I))) or x in sigma (finSigmaFields (F,I)) )

assume x in Union (F | (I \ ({} I))) ; :: thesis: x in sigma (finSigmaFields (F,I))

then x in union (rng F) ;

then consider y being set such that

A16: x in y and

A17: y in rng F by TARSKI:def 4;

consider i being object such that

A18: i in dom F and

A19: y = F . i by A17, FUNCT_1:def 3;

A20: x in finSigmaFields (F,I)

hence x in sigma (finSigmaFields (F,I)) by A20; :: thesis: verum

end;assume x in Union (F | (I \ ({} I))) ; :: thesis: x in sigma (finSigmaFields (F,I))

then x in union (rng F) ;

then consider y being set such that

A16: x in y and

A17: y in rng F by TARSKI:def 4;

consider i being object such that

A18: i in dom F and

A19: y = F . i by A17, FUNCT_1:def 3;

A20: x in finSigmaFields (F,I)

proof

finSigmaFields (F,I) c= sigma (finSigmaFields (F,I))
by PROB_1:def 9;
reconsider Fi = F . i as SigmaField of Omega by A18, Def2;

A21: ( sigma Fi c= Fi & Fi c= sigma Fi ) by PROB_1:def 9;

i in I by A18;

then for z being object st z in {i} holds

z in I by TARSKI:def 1;

then reconsider E = {i} as finite Subset of I by TARSKI:def 3;

A22: dom (F | {i}) = (dom F) /\ {i} by RELAT_1:61

.= {i} by A18, ZFMISC_1:46 ;

then rng (F | {i}) = {((F | {i}) . i)} by FUNCT_1:4;

then A23: union (rng (F | {i})) = (F | {i}) . i by ZFMISC_1:25;

i in dom (F | {i}) by A22, TARSKI:def 1;

then Union (F | {i}) = F . i by A23, FUNCT_1:47;

then sigUn (F,E) = F . i by A21;

hence x in finSigmaFields (F,I) by A16, A19, Def10; :: thesis: verum

end;A21: ( sigma Fi c= Fi & Fi c= sigma Fi ) by PROB_1:def 9;

i in I by A18;

then for z being object st z in {i} holds

z in I by TARSKI:def 1;

then reconsider E = {i} as finite Subset of I by TARSKI:def 3;

A22: dom (F | {i}) = (dom F) /\ {i} by RELAT_1:61

.= {i} by A18, ZFMISC_1:46 ;

then rng (F | {i}) = {((F | {i}) . i)} by FUNCT_1:4;

then A23: union (rng (F | {i})) = (F | {i}) . i by ZFMISC_1:25;

i in dom (F | {i}) by A22, TARSKI:def 1;

then Union (F | {i}) = F . i by A23, FUNCT_1:47;

then sigUn (F,E) = F . i by A21;

hence x in finSigmaFields (F,I) by A16, A19, Def10; :: thesis: verum

hence x in sigma (finSigmaFields (F,I)) by A20; :: thesis: verum

A25: for u, v being Event of Sigma st u in sigUn (F,(I \ ({} I))) & v in tailSigmaField (F,I) holds

u,v are_independent_respect_to P

proof

assume
a in tailSigmaField (F,I)
; :: thesis: ( P . a = 0 or P . a = 1 )
for x, y being set st x in finSigmaFields (F,I) & y in finSigmaFields (F,I) holds

x /\ y in finSigmaFields (F,I)

let u, v be Event of Sigma; :: thesis: ( u in sigUn (F,(I \ ({} I))) & v in tailSigmaField (F,I) implies u,v are_independent_respect_to P )

A37: not finSigmaFields (F,I) is empty

hence u,v are_independent_respect_to P by A13, A24, A37, A41, A36, A38, Th10; :: thesis: verum

end;x /\ y in finSigmaFields (F,I)

proof

then A36:
finSigmaFields (F,I) is intersection_stable
by FINSUB_1:def 2;
let x, y be set ; :: thesis: ( x in finSigmaFields (F,I) & y in finSigmaFields (F,I) implies x /\ y in finSigmaFields (F,I) )

assume that

A26: x in finSigmaFields (F,I) and

A27: y in finSigmaFields (F,I) ; :: thesis: x /\ y in finSigmaFields (F,I)

consider E1 being finite Subset of I such that

A28: x in sigUn (F,E1) by A26, Def10;

consider E2 being finite Subset of I such that

A29: y in sigUn (F,E2) by A27, Def10;

A30: for z being set

for E1, E2 being finite Subset of I st z in sigUn (F,E1) holds

z in sigUn (F,(E1 \/ E2))

x in sigUn (F,(E1 \/ E2)) by A28, A30;

then x /\ y in sigUn (F,(E1 \/ E2)) by A35, FINSUB_1:def 2;

hence x /\ y in finSigmaFields (F,I) by Def10; :: thesis: verum

end;assume that

A26: x in finSigmaFields (F,I) and

A27: y in finSigmaFields (F,I) ; :: thesis: x /\ y in finSigmaFields (F,I)

consider E1 being finite Subset of I such that

A28: x in sigUn (F,E1) by A26, Def10;

consider E2 being finite Subset of I such that

A29: y in sigUn (F,E2) by A27, Def10;

A30: for z being set

for E1, E2 being finite Subset of I st z in sigUn (F,E1) holds

z in sigUn (F,(E1 \/ E2))

proof

then A35:
y in sigUn (F,(E2 \/ E1))
by A29;
let z be set ; :: thesis: for E1, E2 being finite Subset of I st z in sigUn (F,E1) holds

z in sigUn (F,(E1 \/ E2))

let E1, E2 be finite Subset of I; :: thesis: ( z in sigUn (F,E1) implies z in sigUn (F,(E1 \/ E2)) )

reconsider E3 = E1 \/ E2 as finite Subset of I ;

A31: Union (F | E1) c= Union (F | E3)

then Union (F | E1) c= sigma (Union (F | E3)) by A31;

then A34: sigma (Union (F | E1)) c= sigma (Union (F | E3)) by PROB_1:def 9;

assume z in sigUn (F,E1) ; :: thesis: z in sigUn (F,(E1 \/ E2))

hence z in sigUn (F,(E1 \/ E2)) by A34; :: thesis: verum

end;z in sigUn (F,(E1 \/ E2))

let E1, E2 be finite Subset of I; :: thesis: ( z in sigUn (F,E1) implies z in sigUn (F,(E1 \/ E2)) )

reconsider E3 = E1 \/ E2 as finite Subset of I ;

A31: Union (F | E1) c= Union (F | E3)

proof

Union (F | E3) c= sigma (Union (F | E3))
by PROB_1:def 9;
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in Union (F | E1) or X in Union (F | E3) )

assume X in Union (F | E1) ; :: thesis: X in Union (F | E3)

then consider S being set such that

A32: X in S and

A33: S in rng (F | E1) by TARSKI:def 4;

F | E3 = (F | E1) \/ (F | E2) by RELAT_1:78;

then rng (F | E3) = (rng (F | E1)) \/ (rng (F | E2)) by RELAT_1:12;

then S in rng (F | E3) by A33, XBOOLE_0:def 3;

hence X in Union (F | E3) by A32, TARSKI:def 4; :: thesis: verum

end;assume X in Union (F | E1) ; :: thesis: X in Union (F | E3)

then consider S being set such that

A32: X in S and

A33: S in rng (F | E1) by TARSKI:def 4;

F | E3 = (F | E1) \/ (F | E2) by RELAT_1:78;

then rng (F | E3) = (rng (F | E1)) \/ (rng (F | E2)) by RELAT_1:12;

then S in rng (F | E3) by A33, XBOOLE_0:def 3;

hence X in Union (F | E3) by A32, TARSKI:def 4; :: thesis: verum

then Union (F | E1) c= sigma (Union (F | E3)) by A31;

then A34: sigma (Union (F | E1)) c= sigma (Union (F | E3)) by PROB_1:def 9;

assume z in sigUn (F,E1) ; :: thesis: z in sigUn (F,(E1 \/ E2))

hence z in sigUn (F,(E1 \/ E2)) by A34; :: thesis: verum

x in sigUn (F,(E1 \/ E2)) by A28, A30;

then x /\ y in sigUn (F,(E1 \/ E2)) by A35, FINSUB_1:def 2;

hence x /\ y in finSigmaFields (F,I) by Def10; :: thesis: verum

let u, v be Event of Sigma; :: thesis: ( u in sigUn (F,(I \ ({} I))) & v in tailSigmaField (F,I) implies u,v are_independent_respect_to P )

A37: not finSigmaFields (F,I) is empty

proof

A38:
tailSigmaField (F,I) c= Sigma
set E = the finite Subset of I;

{} in sigUn (F, the finite Subset of I) by PROB_1:4;

hence not finSigmaFields (F,I) is empty by Def10; :: thesis: verum

end;{} in sigUn (F, the finite Subset of I) by PROB_1:4;

hence not finSigmaFields (F,I) is empty by Def10; :: thesis: verum

proof

A41:
finSigmaFields (F,I) c= Sigma
set Ie = I \ ({} I);

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tailSigmaField (F,I) or x in Sigma )

assume A39: x in tailSigmaField (F,I) ; :: thesis: x in Sigma

Union (F | (I \ ({} I))) c= Sigma

sigUn (F,(I \ ({} I))) in futSigmaFields (F,I) by Def7;

then x in sigma (Union (F | (I \ ({} I)))) by A39, SETFAM_1:def 1;

hence x in Sigma by A40; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tailSigmaField (F,I) or x in Sigma )

assume A39: x in tailSigmaField (F,I) ; :: thesis: x in Sigma

Union (F | (I \ ({} I))) c= Sigma

proof

then A40:
sigma (Union (F | (I \ ({} I)))) c= Sigma
by PROB_1:def 9;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Union (F | (I \ ({} I))) or y in Sigma )

assume y in Union (F | (I \ ({} I))) ; :: thesis: y in Sigma

then ex S being set st

( y in S & S in rng (F | (I \ ({} I))) ) by TARSKI:def 4;

hence y in Sigma ; :: thesis: verum

end;assume y in Union (F | (I \ ({} I))) ; :: thesis: y in Sigma

then ex S being set st

( y in S & S in rng (F | (I \ ({} I))) ) by TARSKI:def 4;

hence y in Sigma ; :: thesis: verum

sigUn (F,(I \ ({} I))) in futSigmaFields (F,I) by Def7;

then x in sigma (Union (F | (I \ ({} I)))) by A39, SETFAM_1:def 1;

hence x in Sigma by A40; :: thesis: verum

proof

assume
( u in sigUn (F,(I \ ({} I))) & v in tailSigmaField (F,I) )
; :: thesis: u,v are_independent_respect_to P
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in finSigmaFields (F,I) or x in Sigma )

assume x in finSigmaFields (F,I) ; :: thesis: x in Sigma

then consider E being finite Subset of I such that

A42: x in sigUn (F,E) by Def10;

Union (F | E) c= Sigma

hence x in Sigma by A42; :: thesis: verum

end;assume x in finSigmaFields (F,I) ; :: thesis: x in Sigma

then consider E being finite Subset of I such that

A42: x in sigUn (F,E) by Def10;

Union (F | E) c= Sigma

proof

then
sigma (Union (F | E)) c= Sigma
by PROB_1:def 9;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Union (F | E) or y in Sigma )

assume y in Union (F | E) ; :: thesis: y in Sigma

then ex S being set st

( y in S & S in rng (F | E) ) by TARSKI:def 4;

hence y in Sigma ; :: thesis: verum

end;assume y in Union (F | E) ; :: thesis: y in Sigma

then ex S being set st

( y in S & S in rng (F | E) ) by TARSKI:def 4;

hence y in Sigma ; :: thesis: verum

hence x in Sigma by A42; :: thesis: verum

hence u,v are_independent_respect_to P by A13, A24, A37, A41, A36, A38, Th10; :: thesis: verum

then a,a are_independent_respect_to P by A1, A25;

then P . (a /\ a) = (P . a) * (P . a) by PROB_2:def 4;

hence ( P . a = 0 or P . a = 1 ) by Th2; :: thesis: verum