let Omega be non empty set ; for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma st 0 < P . B & P . B < 1 & (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A holds
A,B are_independent_respect_to P
let Sigma be SigmaField of Omega; for P being Probability of Sigma
for A, B being Event of Sigma st 0 < P . B & P . B < 1 & (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A holds
A,B are_independent_respect_to P
let P be Probability of Sigma; for A, B being Event of Sigma st 0 < P . B & P . B < 1 & (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A holds
A,B are_independent_respect_to P
let A, B be Event of Sigma; ( 0 < P . B & P . B < 1 & (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A implies A,B are_independent_respect_to P )
assume that
A1:
0 < P . B
and
A2:
P . B < 1
and
A3:
(P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A
; A,B are_independent_respect_to P
( 0 < P . (([#] Sigma) \ B) & (P . (A /\ B)) / (P . B) = (P .|. (([#] Sigma) \ B)) . A )
by A1, A2, A3, Def6, Th17;
then A4:
(P . (A /\ B)) / (P . B) = (P . (A /\ (([#] Sigma) \ B))) / (P . (([#] Sigma) \ B))
by Def6;
A5:
B ` = ([#] Sigma) \ B
;
P . (([#] Sigma) \ B) <> 0
by A2, Th17;
then
(P . (A /\ B)) * (P . (([#] Sigma) \ B)) = (P . (A /\ (([#] Sigma) \ B))) * (P . B)
by A1, A4, Th1;
then
(P . (A /\ B)) * (1 - (P . B)) = (P . (A /\ (([#] Sigma) \ B))) * (P . B)
by PROB_1:32;
then P . (A /\ B) =
((P . (A /\ (([#] Sigma) \ B))) + (P . (A /\ B))) * (P . B)
.=
(P . A) * (P . B)
by A5, Th14
;
hence
A,B are_independent_respect_to P
; verum