let M be non empty-yielding 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 Element of 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 Element of NAT st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) ) )
A1:
( len (Infor_FinSeq_of M) = len M & width (Infor_FinSeq_of M) = width M )
by Def8;
then A2:
( dom (Infor_FinSeq_of M) = dom M & Seg (width (Infor_FinSeq_of M)) = Seg (width M) )
by FINSEQ_3:31;
hereby :: thesis: ( len p = len M & ( for k being Element of NAT st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) implies p = Entropy_of_Cond_Prob M )
assume A3:
p = Entropy_of_Cond_Prob M
;
:: thesis: ( len p = len M & ( for k being Element of NAT st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) )then A4:
(
len p = len M & ( for
k being
Element of
NAT st
k in dom p holds
p . k = Entropy (Line M,k) ) )
by Def11;
then A5:
dom p = dom M
by FINSEQ_3:31;
now let k be
Element of
NAT ;
:: thesis: ( k in dom p implies p . k = - (Sum ((Infor_FinSeq_of M) . k)) )assume A6:
k in dom p
;
:: thesis: p . k = - (Sum ((Infor_FinSeq_of M) . k))A7:
k in dom (Infor_FinSeq_of M)
by A1, A4, A6, FINSEQ_3:31;
thus p . k =
Entropy (Line M,k)
by A3, A6, Def11
.=
- (Sum (Line (Infor_FinSeq_of M),k))
by A5, A6, Th53
.=
- (Sum ((Infor_FinSeq_of M) . k))
by A7, MATRIX_2:18
;
:: thesis: verum end; hence
(
len p = len M & ( for
k being
Element of
NAT st
k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) )
by A3, Def11;
:: thesis: verum
end;
assume A8:
( len p = len M & ( for k being Element of NAT st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) )
; :: thesis: p = Entropy_of_Cond_Prob M
then A9:
dom p = dom M
by FINSEQ_3:31;
now let k be
Element of
NAT ;
:: thesis: ( k in dom p implies p . k = Entropy (Line M,k) )assume A10:
k in dom p
;
:: thesis: p . k = Entropy (Line M,k)thus p . k =
- (Sum ((Infor_FinSeq_of M) . k))
by A8, A10
.=
- (Sum (Line (Infor_FinSeq_of M),k))
by A2, A9, A10, MATRIX_2:18
.=
Entropy (Line M,k)
by A9, A10, Th53
;
:: thesis: verum end;
hence
p = Entropy_of_Cond_Prob M
by A8, Def11; :: thesis: verum