let M be V3() Conditional_Probability Matrix of REAL; :: thesis: for p being FinSequence of REAL holds
( p = Entropy_of_Cond_Prob M iff ( len p = len M & ( for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) ) )
let p be FinSequence of REAL ; :: thesis: ( p = Entropy_of_Cond_Prob M iff ( len p = len M & ( for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) ) )
A1: len (Infor_FinSeq_of M) = len M by Def8;
hereby :: thesis: ( len p = len M & ( for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) implies p = Entropy_of_Cond_Prob M )
assume A2: p = Entropy_of_Cond_Prob M ; :: thesis: ( len p = len M & ( for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) )
then A3: len p = len M by Def11;
then A4: dom p = dom M by FINSEQ_3:29;
now :: thesis: for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k))
let k be Nat; :: thesis: ( k in dom p implies p . k = - (Sum ((Infor_FinSeq_of M) . k)) )
assume A5: k in dom p ; :: thesis: p . k = - (Sum ((Infor_FinSeq_of M) . k))
A6: k in dom (Infor_FinSeq_of M) by A1, A3, A5, FINSEQ_3:29;
thus p . k = Entropy (Line (M,k)) by A2, A5, Def11
.= - (Sum (Line ((Infor_FinSeq_of M),k))) by A4, A5, Th53
.= - (Sum ((Infor_FinSeq_of M) . k)) by A6, MATRIX_0:60 ; :: thesis: verum
end;
hence ( len p = len M & ( for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) ) by A2, Def11; :: thesis: verum
end;
assume that
A7: len p = len M and
A8: for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ; :: thesis: p = Entropy_of_Cond_Prob M
A9: dom p = dom M by A7, FINSEQ_3:29;
A10: dom (Infor_FinSeq_of M) = dom M by A1, FINSEQ_3:29;
now :: thesis: for k being Nat st k in dom p holds
p . k = Entropy (Line (M,k))
let k be Nat; :: thesis: ( k in dom p implies p . k = Entropy (Line (M,k)) )
assume A11: k in dom p ; :: thesis: p . k = Entropy (Line (M,k))
thus p . k = - (Sum ((Infor_FinSeq_of M) . k)) by A8, A11
.= - (Sum (Line ((Infor_FinSeq_of M),k))) by A10, A9, A11, MATRIX_0:60
.= Entropy (Line (M,k)) by A9, A11, Th53 ; :: thesis: verum
end;
hence p = Entropy_of_Cond_Prob M by A7, Def11; :: thesis: verum