let Omega be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum