let p be ProbFinS FinSequence of REAL ; :: thesis: for M being non empty-yielding Conditional_Probability Matrix of REAL st len p = len M holds
Entropy_of_Joint_Prob ((Vec2DiagMx p) * M) = (Entropy p) + (Sum (mlt p,(Entropy_of_Cond_Prob M)))
let M be non empty-yielding Conditional_Probability Matrix of REAL ; :: thesis: ( len p = len M implies Entropy_of_Joint_Prob ((Vec2DiagMx p) * M) = (Entropy p) + (Sum (mlt p,(Entropy_of_Cond_Prob M))) )
assume A1: len p = len M ; :: thesis: Entropy_of_Joint_Prob ((Vec2DiagMx p) * M) = (Entropy p) + (Sum (mlt p,(Entropy_of_Cond_Prob M)))
set M1 = (Vec2DiagMx p) * M;
len (LineSum (Infor_FinSeq_of M)) = len (Infor_FinSeq_of M) by MATRPROB:def 1
.= len p by A1, Def8 ;
then A2: ( p is Element of (len p) -tuples_on REAL & LineSum (Infor_FinSeq_of M) is Element of (len p) -tuples_on REAL ) by FINSEQ_2:110;
reconsider M1 = (Vec2DiagMx p) * M as Joint_Probability Matrix of REAL by A1, Th28;
A3: Entropy_of_Joint_Prob M1 = - (Sum (Mx2FinS (Infor_FinSeq_of M1))) by Th59
.= - (SumAll (Infor_FinSeq_of M1)) by Th42
.= - ((Sum (Infor_FinSeq_of p)) + (Sum (mlt p,(LineSum (Infor_FinSeq_of M))))) by A1, Th64
.= (- (Sum (Infor_FinSeq_of p))) - (Sum (mlt p,(LineSum (Infor_FinSeq_of M)))) ;
(Entropy p) + (Sum (mlt p,(Entropy_of_Cond_Prob M))) = (- (Sum (Infor_FinSeq_of p))) + (Sum (mlt p,(- (LineSum (Infor_FinSeq_of M))))) by Th63
.= (- (Sum (Infor_FinSeq_of p))) + (Sum (- (mlt p,(LineSum (Infor_FinSeq_of M))))) by A2, RVSUM_1:94
.= (- (Sum (Infor_FinSeq_of p))) + (- (Sum (mlt p,(LineSum (Infor_FinSeq_of M))))) by RVSUM_1:118 ;
hence Entropy_of_Joint_Prob ((Vec2DiagMx p) * M) = (Entropy p) + (Sum (mlt p,(Entropy_of_Cond_Prob M))) by A3; :: thesis: verum