let p be ProbFinS FinSequence of REAL ; :: thesis: for M being 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 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 A1: 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;
A2: (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:65
.= (- (Sum (Infor_FinSeq_of p))) + (- (Sum (mlt (p,(LineSum (Infor_FinSeq_of M)))))) by RVSUM_1:88 ;
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))))) ;
hence Entropy_of_Joint_Prob ((Vec2DiagMx p) * M) = (Entropy p) + (Sum (mlt (p,(Entropy_of_Cond_Prob M)))) by A2; :: thesis: verum