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))) )
set M1 = (Vec2DiagMx p) * M;
assume A2: len p = len M ; :: thesis: Entropy_of_Joint_Prob ((Vec2DiagMx p) * M) = (Entropy p) + (Sum (mlt p,(Entropy_of_Cond_Prob M)))
then reconsider M1 = (Vec2DiagMx p) * M as Joint_Probability Matrix of REAL by Th28;
A4: (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 RVSUM_1:94
.= (- (Sum (Infor_FinSeq_of p))) + (- (Sum (mlt p,(LineSum (Infor_FinSeq_of M))))) by RVSUM_1:118 ;
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 A2, Th64
.= (- (Sum (Infor_FinSeq_of p))) - (Sum (mlt p,(LineSum (Infor_FinSeq_of M)))) ;
hence Entropy_of_Joint_Prob ((Vec2DiagMx p) * M) = (Entropy p) + (Sum (mlt p,(Entropy_of_Cond_Prob M))) by A4; :: thesis: verum